// This prints the left floatting menu

Theoremgcd.let_clause_15441

Statement

∀ p q, ∀ m n, O < n ⇒ n ≤ m ⇒ n ≤ q ⇒ ex (λa. ex (λb. (((a × n) - (b × m)) = (gcd_aux q m n)) ∨ (((b × m) - (a × n)) = (gcd_aux q m n)))) ⇒ ∀ m n, O < n ⇒ n ≤ m ⇒ n ≤ (q+1) ⇒ ¬(n | m) ⇒ ∀ a, ex (λb. (((a × (mod m n)) - (b × n)) = (gcd_aux q n (mod m n))) ∨ (((b × n) - (a × (mod m n))) = (gcd_aux q n (mod m n)))) ⇒ ∀ b, (((a × (mod m n)) - (b × n)) = (gcd_aux q n (mod m n))) ∨ (((b × n) - (a × (mod m n))) = (gcd_aux q n (mod m n))) ⇒ ((b × n) - (a × (mod m n))) = (gcd_aux q n (mod m n)) ⇒ ((n × b) - (a × (mod m n))) = (gcd_aux q n (mod m n))

Main Dependencies
Theory

Statement

Theorem let_clause_15441 : forall (p:nat.nat), forall (q:nat.nat), (forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> (nat.le n m) -> (nat.le n q) -> connectives.ex (nat.nat) (fun (a:nat.nat) => connectives.ex (nat.nat) (fun (b:nat.nat) => connectives.Or (logic.eq (nat.nat) (nat.minus (nat.times a n) (nat.times b m)) (gcd_aux q m n)) (logic.eq (nat.nat) (nat.minus (nat.times b m) (nat.times a n)) (gcd_aux q m n))))) -> forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> (nat.le n m) -> (nat.le n (nat.S q)) -> (connectives.Not (primes.divides n m)) -> forall (a:nat.nat), (connectives.ex (nat.nat) (fun (b:nat.nat) => connectives.Or (logic.eq (nat.nat) (nat.minus (nat.times a (div_mod.mod m n)) (nat.times b n)) (gcd_aux q n (div_mod.mod m n))) (logic.eq (nat.nat) (nat.minus (nat.times b n) (nat.times a (div_mod.mod m n))) (gcd_aux q n (div_mod.mod m n))))) -> forall (b:nat.nat), (connectives.Or (logic.eq (nat.nat) (nat.minus (nat.times a (div_mod.mod m n)) (nat.times b n)) (gcd_aux q n (div_mod.mod m n))) (logic.eq (nat.nat) (nat.minus (nat.times b n) (nat.times a (div_mod.mod m n))) (gcd_aux q n (div_mod.mod m n)))) -> (logic.eq (nat.nat) (nat.minus (nat.times b n) (nat.times a (div_mod.mod m n))) (gcd_aux q n (div_mod.mod m n))) -> logic.eq (nat.nat) (nat.minus (nat.times n b) (nat.times a (div_mod.mod m n))) (gcd_aux q n (div_mod.mod m n)).

Statement

theorem let_clause_15441 : \forall (p:nat). \forall (q:nat). (\forall (m:nat). \forall (n:nat). ((lt) (O) n) -> ((le) n m) -> ((le) n q) -> (ex) (nat) (\lambda a : nat. (ex) (nat) (\lambda b : nat. (Or) ((eq) (nat) ((minus) ((times) a n) ((times) b m)) ((gcd_aux) q m n)) ((eq) (nat) ((minus) ((times) b m) ((times) a n)) ((gcd_aux) q m n))))) -> \forall (m:nat). \forall (n:nat). ((lt) (O) n) -> ((le) n m) -> ((le) n ((S) q)) -> ((Not) ((divides) n m)) -> \forall (a:nat). ((ex) (nat) (\lambda b : nat. (Or) ((eq) (nat) ((minus) ((times) a ((mod) m n)) ((times) b n)) ((gcd_aux) q n ((mod) m n))) ((eq) (nat) ((minus) ((times) b n) ((times) a ((mod) m n))) ((gcd_aux) q n ((mod) m n))))) -> \forall (b:nat). ((Or) ((eq) (nat) ((minus) ((times) a ((mod) m n)) ((times) b n)) ((gcd_aux) q n ((mod) m n))) ((eq) (nat) ((minus) ((times) b n) ((times) a ((mod) m n))) ((gcd_aux) q n ((mod) m n)))) -> ((eq) (nat) ((minus) ((times) b n) ((times) a ((mod) m n))) ((gcd_aux) q n ((mod) m n))) -> (eq) (nat) ((minus) ((times) n b) ((times) a ((mod) m n))) ((gcd_aux) q n ((mod) m n)).

Statement

theorem let_clause_15441 : forall (p:nat.nat) , forall (q:nat.nat) , (forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((nat.le_) ) (n)) (m)) -> ((((nat.le_) ) (n)) (q)) -> ((connectives.ex) (nat.nat)) (fun (a : nat.nat) , ((connectives.ex) (nat.nat)) (fun (b : nat.nat) , (((connectives.Or) ) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (a)) (n))) ((((nat.times) ) (b)) (m)))) (((((gcd.gcd_aux) ) (q)) (m)) (n)))) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (b)) (m))) ((((nat.times) ) (a)) (n)))) (((((gcd.gcd_aux) ) (q)) (m)) (n)))))) -> forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((nat.le_) ) (n)) (m)) -> ((((nat.le_) ) (n)) (((nat.S) ) (q))) -> (((connectives.Not) ) ((((primes.divides) ) (n)) (m))) -> forall (a:nat.nat) , (((connectives.ex) (nat.nat)) (fun (b : nat.nat) , (((connectives.Or) ) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (a)) ((((div_mod.mod) ) (m)) (n)))) ((((nat.times) ) (b)) (n)))) (((((gcd.gcd_aux) ) (q)) (n)) ((((div_mod.mod) ) (m)) (n))))) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (b)) (n))) ((((nat.times) ) (a)) ((((div_mod.mod) ) (m)) (n))))) (((((gcd.gcd_aux) ) (q)) (n)) ((((div_mod.mod) ) (m)) (n)))))) -> forall (b:nat.nat) , ((((connectives.Or) ) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (a)) ((((div_mod.mod) ) (m)) (n)))) ((((nat.times) ) (b)) (n)))) (((((gcd.gcd_aux) ) (q)) (n)) ((((div_mod.mod) ) (m)) (n))))) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (b)) (n))) ((((nat.times) ) (a)) ((((div_mod.mod) ) (m)) (n))))) (((((gcd.gcd_aux) ) (q)) (n)) ((((div_mod.mod) ) (m)) (n))))) -> ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (b)) (n))) ((((nat.times) ) (a)) ((((div_mod.mod) ) (m)) (n))))) (((((gcd.gcd_aux) ) (q)) (n)) ((((div_mod.mod) ) (m)) (n)))) -> (((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (n)) (b))) ((((nat.times) ) (a)) ((((div_mod.mod) ) (m)) (n))))) (((((gcd.gcd_aux) ) (q)) (n)) ((((div_mod.mod) ) (m)) (n))).

Statement

let_clause_15441 : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(q: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) => (nat_sttfa_th.le(n)(m) => (nat_sttfa_th.le(n)(q) => connectives_sttfa_th.sttfa_ex[nat_sttfa_th.sttfa_nat]((LAMBDA(a:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_ex[nat_sttfa_th.sttfa_nat]((LAMBDA(b:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_Or(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(a)(n))(nat_sttfa_th.times(b)(m)))(gcd_sttfa.gcd_aux(q)(m)(n)))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(b)(m))(nat_sttfa_th.times(a)(n)))(gcd_sttfa.gcd_aux(q)(m)(n)))))))))))) => (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.le(n)(m) => (nat_sttfa_th.le(n)(nat_sttfa_th.sttfa_S(q)) => (connectives_sttfa_th.sttfa_Not(primes_sttfa_th.sttfa_divides(n)(m)) => (FORALL(a:nat_sttfa_th.sttfa_nat):(connectives_sttfa_th.sttfa_ex[nat_sttfa_th.sttfa_nat]((LAMBDA(b:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_Or(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(a)(div_mod_sttfa_th.mod(m)(n)))(nat_sttfa_th.times(b)(n)))(gcd_sttfa.gcd_aux(q)(n)(div_mod_sttfa_th.mod(m)(n))))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(b)(n))(nat_sttfa_th.times(a)(div_mod_sttfa_th.mod(m)(n))))(gcd_sttfa.gcd_aux(q)(n)(div_mod_sttfa_th.mod(m)(n)))))) => (FORALL(b:nat_sttfa_th.sttfa_nat):(connectives_sttfa_th.sttfa_Or(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(a)(div_mod_sttfa_th.mod(m)(n)))(nat_sttfa_th.times(b)(n)))(gcd_sttfa.gcd_aux(q)(n)(div_mod_sttfa_th.mod(m)(n))))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(b)(n))(nat_sttfa_th.times(a)(div_mod_sttfa_th.mod(m)(n))))(gcd_sttfa.gcd_aux(q)(n)(div_mod_sttfa_th.mod(m)(n)))) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(b)(n))(nat_sttfa_th.times(a)(div_mod_sttfa_th.mod(m)(n))))(gcd_sttfa.gcd_aux(q)(n)(div_mod_sttfa_th.mod(m)(n))) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(n)(b))(nat_sttfa_th.times(a)(div_mod_sttfa_th.mod(m)(n))))(gcd_sttfa.gcd_aux(q)(n)(div_mod_sttfa_th.mod(m)(n)))))))))))))))))

Printing for OpenTheory is not working at the moment.