// This prints the left floatting menu

Theoremgcd.let_clause_1545

Statement

∀ m n, (gcd m n) = O ⇒ O | n ⇒ ∀ q1, n = (O × q1) ⇒ O | m ⇒ ∀ q2, m = (O × q2) ⇒ m = O

Main Dependencies
Theory

Statement

Theorem let_clause_1545 : forall (m:nat.nat), forall (n:nat.nat), (logic.eq (nat.nat) (gcd m n) nat.O) -> (primes.divides nat.O n) -> forall (q1:nat.nat), (logic.eq (nat.nat) n (nat.times nat.O q1)) -> (primes.divides nat.O m) -> forall (q2:nat.nat), (logic.eq (nat.nat) m (nat.times nat.O q2)) -> logic.eq (nat.nat) m nat.O.

Statement

theorem let_clause_1545 : \forall (m:nat). \forall (n:nat). ((eq) (nat) ((gcd) m n) (O) ) -> ((divides) (O) n) -> \forall (q1:nat). ((eq) (nat) n ((times) (O) q1)) -> ((divides) (O) m) -> \forall (q2:nat). ((eq) (nat) m ((times) (O) q2)) -> (eq) (nat) m (O) .

Statement

theorem let_clause_1545 : forall (m:nat.nat) , forall (n:nat.nat) , ((((logic.eq_) (nat.nat)) ((((gcd.gcd) ) (m)) (n))) ((nat.O) )) -> ((((primes.divides) ) ((nat.O) )) (n)) -> forall (q1:nat.nat) , ((((logic.eq_) (nat.nat)) (n)) ((((nat.times) ) ((nat.O) )) (q1))) -> ((((primes.divides) ) ((nat.O) )) (m)) -> forall (q2:nat.nat) , ((((logic.eq_) (nat.nat)) (m)) ((((nat.times) ) ((nat.O) )) (q2))) -> (((logic.eq_) (nat.nat)) (m)) ((nat.O) ).

Statement

let_clause_1545 : LEMMA (FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](gcd_sttfa.gcd(m)(n))(nat_sttfa_th.sttfa_O) => (primes_sttfa_th.sttfa_divides(nat_sttfa_th.sttfa_O)(n) => (FORALL(q1:nat_sttfa_th.sttfa_nat):(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.times(nat_sttfa_th.sttfa_O)(q1)) => (primes_sttfa_th.sttfa_divides(nat_sttfa_th.sttfa_O)(m) => (FORALL(q2:nat_sttfa_th.sttfa_nat):(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](m)(nat_sttfa_th.times(nat_sttfa_th.sttfa_O)(q2)) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](m)(nat_sttfa_th.sttfa_O))))))))))

Printing for OpenTheory is not working at the moment.