Logipedia

// This prints the left floatting menu

Dedukti

Matita

Coq

Lean

PVS

OpenTheory

Theorem
gcd.eq_minus_gcd_aux

Statement

∀ p m n, O < n ⇒ n ≤ m ⇒ n ≤ p ⇒ ex (λa. ex (λb. (((a × n) - (b × m)) = (gcd_aux p m n)) ∨ (((b × m) - (a × n)) = (gcd_aux p m n))))

Main Dependencies

axiom

connectives.ex_intro connectives.match_ex_prop

theorem

gcd.divides_to_gcd_aux gcd.let_clause_1544 gcd.let_clause_15441 gcd.not_divides_to_gcd_aux nat.le_S_S_to_le nat.le_to_not_lt nat.minus_plus nat.times_times primes.decidable_divides

Theory

axiom

bool.axiom_match_bool_type_false bool.axiom_match_bool_type_true bool.match_bool_prop connectives.I connectives.Not_ind connectives.equal_leibniz connectives.ex_intro connectives.falsity connectives.match_Or_prop connectives.match_ex_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_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 eq_minus_gcd_aux : forall (p:nat.nat), forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> (nat.le n m) -> (nat.le n p) -> 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 p m n)) (logic.eq (nat.nat) (nat.minus (nat.times b m) (nat.times a n)) (gcd_aux p m n)))).

Statement

theorem eq_minus_gcd_aux : \forall (p:nat). \forall (m:nat). \forall (n:nat). ((lt) (O) n) -> ((le) n m) -> ((le) n p) -> (ex) (nat) (\lambda a : nat. (ex) (nat) (\lambda b : nat. (Or) ((eq) (nat) ((minus) ((times) a n) ((times) b m)) ((gcd_aux) p m n)) ((eq) (nat) ((minus) ((times) b m) ((times) a n)) ((gcd_aux) p m n)))).

Statement

theorem eq_minus_gcd_aux : forall (p:nat.nat) , forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((nat.le_) ) (n)) (m)) -> ((((nat.le_) ) (n)) (p)) -> ((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) ) (p)) (m)) (n)))) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (b)) (m))) ((((nat.times) ) (a)) (n)))) (((((gcd.gcd_aux) ) (p)) (m)) (n))))).

Statement

eq_minus_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) => (nat_sttfa_th.le(n)(m) => (nat_sttfa_th.le(n)(p) => 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(p)(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(p)(m)(n)))))))))))))

Printing for OpenTheory is not working at the moment.

Theoremgcd.eq_minus_gcd_aux

Theorem
gcd.eq_minus_gcd_aux