Logipedia

// This prints the left floatting menu

Load

Dedukti-jumb

Theorem
gcd.prime_to_gcd_1

Statement

∀ n m, prime n ⇒ ¬(n | m) ⇒ (gcd n m) = 1

Main Dependencies

definition

theorem

gcd.divides_gcd_l gcd.divides_gcd_r gcd.lt_O_gcd nat.le_to_le_to_eq nat.not_eq_to_le_to_lt nat.not_lt_to_le

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

Coq-Jumb

Statement

Theorem prime_to_gcd_1 : forall (n:nat.nat), forall (m:nat.nat), (primes.prime n) -> (connectives.Not (primes.divides n m)) -> logic.eq (nat.nat) (gcd n m) (nat.S nat.O).

Matita-Jumb

Statement

theorem prime_to_gcd_1 : \forall (n:nat). \forall (m:nat). ((prime) n) -> ((Not) ((divides) n m)) -> (eq) (nat) ((gcd) n m) ((S) (O) ).

Lean-jumb

Statement

theorem prime_to_gcd_1 : forall (n:nat.nat) , forall (m:nat.nat) , (((primes.prime) ) (n)) -> (((connectives.Not) ) ((((primes.divides) ) (n)) (m))) -> (((logic.eq_) (nat.nat)) ((((gcd.gcd) ) (n)) (m))) (((nat.S) ) ((nat.O) )).

PVS-jumb

Statement

prime_to_gcd_1 : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(primes_sttfa_th.prime(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(n)(m))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))))))

OpenTheory

Printing for OpenTheory is not working at the moment.