// This prints the left floatting menu

### Theoremgcd.not_divides_to_gcd_aux

Statement

∀ p m n, O < n ⇒ ¬(n | m) ⇒ (gcd_aux (p+1) m n) = (gcd_aux p n (mod m n))

Main Dependencies

Statement

Theorem not_divides_to_gcd_aux : forall (p:nat.nat), forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> (connectives.Not (primes.divides n m)) -> logic.eq (nat.nat) (gcd_aux (nat.S p) m n) (gcd_aux p n (div_mod.mod m n)).

Statement

theorem not_divides_to_gcd_aux : \forall (p:nat). \forall (m:nat). \forall (n:nat). ((lt) (O) n) -> ((Not) ((divides) n m)) -> (eq) (nat) ((gcd_aux) ((S) p) m n) ((gcd_aux) p n ((mod) m n)).

Statement

theorem not_divides_to_gcd_aux : forall (p:nat.nat) , forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> (((connectives.Not) ) ((((primes.divides) ) (n)) (m))) -> (((logic.eq_) (nat.nat)) (((((gcd.gcd_aux) ) (((nat.S) ) (p))) (m)) (n))) (((((gcd.gcd_aux) ) (p)) (n)) ((((div_mod.mod) ) (m)) (n))).

Statement

not_divides_to_gcd_aux : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => (connectives_sttfa_th.sttfa_Not(primes_sttfa_th.sttfa_divides(n)(m)) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](gcd_sttfa.gcd_aux(nat_sttfa_th.sttfa_S(p))(m)(n))(gcd_sttfa.gcd_aux(p)(n)(div_mod_sttfa_th.mod(m)(n))))))))

Printing for OpenTheory is not working at the moment.