Logipedia

Theorem
gcd.lt_O_gcd

Statement

∀ m n, O < n ⇒ O < (gcd m n)

Main Dependencies

theorem

gcd.gcd_O_to_eq_O gcd.let_clause_1572

Theory

axiom

bool.axiom_match_bool_type_false bool.axiom_match_bool_type_true bool.match_bool_prop connectives.I connectives.Not_ind connectives.conj connectives.equal_leibniz connectives.falsity connectives.match_And_prop connectives.match_Or_prop connectives.nmk connectives.or_introl connectives.or_intror div_mod.axiom_div_aux div_mod.axiom_div_aux_body_O div_mod.axiom_div_aux_body_S div_mod.axiom_mod_aux div_mod.axiom_mod_aux_body_O div_mod.axiom_mod_aux_body_S div_mod.div_mod_spec_intro div_mod.match_div_mod_spec_prop gcd.axiom_gcd_aux gcd.axiom_gcd_aux_body_O gcd.axiom_gcd_aux_body_S leibniz.sym_leibniz logic.eq_ind logic.refl nat.axiom_eqb nat.axiom_eqb_body_O nat.axiom_eqb_body_S nat.axiom_filter_nat_type_O nat.axiom_filter_nat_type_S nat.axiom_leb nat.axiom_leb_body_O nat.axiom_leb_body_S nat.axiom_match_nat_type_O nat.axiom_match_nat_type_S nat.axiom_minus nat.axiom_minus_body_O nat.axiom_minus_body_S nat.axiom_plus nat.axiom_plus_body_O nat.axiom_plus_body_S nat.axiom_times nat.axiom_times_body_O nat.axiom_times_body_S nat.le_S nat.le_ind nat.le_n nat.match_nat_prop nat.nat_ind primes.match_divides_prop primes.quotient

definition

div_mod.mod leibniz.leibniz nat.lt primes.dividesb

tyop

bool.bool nat.nat

Statement

Theorem lt_O_gcd : forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> nat.lt nat.O (gcd m n).

Statement

theorem lt_O_gcd : \forall (m:nat). \forall (n:nat). ((lt) (O) n) -> (lt) (O) ((gcd) m n).

Statement

theorem lt_O_gcd : forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> (((nat.lt_) ) ((nat.O) )) ((((gcd.gcd) ) (m)) (n)).

Statement

lt_O_gcd : LEMMA (FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(gcd_sttfa.gcd(m)(n)))))

Printing for OpenTheory is not working at the moment.

Theoremgcd.lt_O_gcd

Theorem
gcd.lt_O_gcd