Search for blocks/addresses/...

Proofgold Address

address
PUVXTmzmbmMwooLhhu4Az9s3GaoBKA4wKe5
total
0
mg
-
conjpub
-
current assets
aba16../71878.. bday: 29757 doc published by PrQUS..
Param setminussetminus : ιιι
Param omegaomega : ι
Param SingSing : ιι
Param nat_pnat_p : ιο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param add_natadd_nat : ιιι
Param mul_natmul_nat : ιιι
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Param ordinalordinal : ιο
Param ordsuccordsucc : ιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_0nat_0 : nat_p 0
Known mul_nat_0Lmul_nat_0L : ∀ x0 . nat_p x0mul_nat 0 x0 = 0
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
Known ordinal_ordsuccordinal_ordsucc : ∀ x0 . ordinal x0ordinal (ordsucc x0)
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Known mul_nat_SLmul_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordinal_ordsucc_In_Subqordinal_ordsucc_In_Subq : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1x0
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0)
Known ordinal_Emptyordinal_Empty : ordinal 0
Known Empty_Subq_eqEmpty_Subq_eq : ∀ x0 . x00x0 = 0
Known SingISingI : ∀ x0 . x0Sing x0
Theorem quotient_remainder_natquotient_remainder_nat : ∀ x0 . x0setminus omega (Sing 0)∀ x1 . nat_p x1∀ x2 : ο . (∀ x3 . and (x3omega) (∀ x4 : ο . (∀ x5 . and (x5x0) (x1 = add_nat (mul_nat x3 x0) x5)x4)x4)x2)x2 (proof)
Param SNoSNo : ιο
Param SNoLeSNoLe : ιιο
Param mul_SNomul_SNo : ιιι
Param SNoLtSNoLt : ιιο
Known SNoLeESNoLeE : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1or (SNoLt x0 x1) (x0 = x1)
Known SNo_0SNo_0 : SNo 0
Known mul_SNo_nonpos_posmul_SNo_nonpos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 0SNoLt 0 x1SNoLe (mul_SNo x0 x1) 0
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known SNoLe_refSNoLe_ref : ∀ x0 . SNoLe x0 x0
Theorem mul_SNo_nonpos_nonnegmul_SNo_nonpos_nonneg : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 0SNoLe 0 x1SNoLe (mul_SNo x0 x1) 0 (proof)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Theorem ordinal_0_In_ordsuccordinal_0_In_ordsucc : ∀ x0 . ordinal x00ordsucc x0 (proof)
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Theorem ordinal_ordsucc_posordinal_ordsucc_pos : ∀ x0 . ordinal x0SNoLt 0 (ordsucc x0) (proof)
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param minus_SNominus_SNo : ιι
Known int_SNo_casesint_SNo_cases : ∀ x0 : ι → ο . (∀ x1 . x1omegax0 x1)(∀ x1 . x1omegax0 (minus_SNo x1))∀ x1 . x1intx0 x1
Known Subq_omega_intSubq_omega_int : omegaint
Known add_nat_add_SNoadd_nat_add_SNo : ∀ x0 . x0omega∀ x1 . x1omegaadd_nat x0 x1 = add_SNo x0 x1
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Known omega_nonnegomega_nonneg : ∀ x0 . x0omegaSNoLe 0 x0
Known int_add_SNoint_add_SNo : ∀ x0 . x0int∀ x1 . x1intadd_SNo x0 x1int
Known int_minus_SNo_omegaint_minus_SNo_omega : ∀ x0 . x0omegaminus_SNo x0int
Known nat_1nat_1 : nat_p 1
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Known aa7e8..nonneg_int_nat_p : ∀ x0 . x0intSNoLe 0 x0nat_p x0
Known int_minus_SNoint_minus_SNo : ∀ x0 . x0intminus_SNo x0int
Known add_SNo_minus_Le2badd_SNo_minus_Le2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe (add_SNo x2 x1) x0SNoLe x2 (add_SNo x0 (minus_SNo x1))
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known add_SNo_minus_Lt1badd_SNo_minus_Lt1b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 (add_SNo x2 x1)SNoLt (add_SNo x0 (minus_SNo x1)) x2
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known add_SNo_Lt2add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x1 x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Known mul_SNo_distrRmul_SNo_distrR : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2)
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known SNo_1SNo_1 : SNo 1
Known mul_SNo_minus_distrLmul_SNo_minus_distrL : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Known mul_SNo_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Known add_SNo_assocadd_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known add_SNo_minus_L2add_SNo_minus_L2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Known minus_add_SNo_distrminus_add_SNo_distr : ∀ x0 x1 . SNo x0SNo x1minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known nat_p_SNonat_p_SNo : ∀ x0 . nat_p x0SNo x0
Theorem quotient_remainder_intquotient_remainder_int : ∀ x0 . x0setminus omega (Sing 0)∀ x1 . x1int∀ x2 : ο . (∀ x3 . and (x3int) (∀ x4 : ο . (∀ x5 . and (x5x0) (x1 = add_SNo (mul_SNo x3 x0) x5)x4)x4)x2)x2 (proof)
Definition divides_intdivides_int := λ x0 x1 . and (and (x0int) (x1int)) (∀ x2 : ο . (∀ x3 . and (x3int) (mul_SNo x0 x3 = x1)x2)x2)
Known divides_int_refdivides_int_ref : ∀ x0 . x0intdivides_int x0 x0
Known divides_int_0divides_int_0 : ∀ x0 . x0intdivides_int x0 0
Known divides_int_add_SNodivides_int_add_SNo : ∀ x0 x1 x2 . divides_int x0 x1divides_int x0 x2divides_int x0 (add_SNo x1 x2)
Known divides_int_add_SNo_3 : ∀ x0 x1 x2 x3 . divides_int x0 x1divides_int x0 x2divides_int x0 x3divides_int x0 (add_SNo x1 (add_SNo x2 x3))
Known divides_int_add_SNo_4 : ∀ x0 x1 x2 x3 x4 . divides_int x0 x1divides_int x0 x2divides_int x0 x3divides_int x0 x4divides_int x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 x4)))
Known divides_int_mul_SNodivides_int_mul_SNo : ∀ x0 x1 x2 x3 . divides_int x0 x2divides_int x1 x3divides_int (mul_SNo x0 x1) (mul_SNo x2 x3)
Param divides_natdivides_nat : ιιο
Known divides_nat_divides_intdivides_nat_divides_int : ∀ x0 x1 . divides_nat x0 x1divides_int x0 x1
Known divides_int_divides_natdivides_int_divides_nat : ∀ x0 . x0omega∀ x1 . x1omegadivides_int x0 x1divides_nat x0 x1
Known divides_int_minus_SNodivides_int_minus_SNo : ∀ x0 x1 . divides_int x0 x1divides_int x0 (minus_SNo x1)
Known divides_int_minus_SNo_conv : ∀ x0 x1 . SNo x1divides_int x0 (minus_SNo x1)divides_int x0 x1
Known divides_int_diff_SNo_rev : ∀ x0 x1 . x1int∀ x2 . x2intdivides_int x0 (add_SNo x1 (minus_SNo x2))divides_int x0 (add_SNo x2 (minus_SNo x1))
Known divides_int_mul_SNo_Ldivides_int_mul_SNo_L : ∀ x0 x1 x2 . x2intdivides_int x0 x1divides_int x0 (mul_SNo x1 x2)
Known divides_int_mul_SNo_Rdivides_int_mul_SNo_R : ∀ x0 x1 x2 . x2intdivides_int x0 x1divides_int x0 (mul_SNo x2 x1)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known int_SNoint_SNo : ∀ x0 . x0intSNo x0
Theorem divides_int_1divides_int_1 : ∀ x0 . x0intdivides_int 1 x0 (proof)
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known nonneg_mul_SNo_Lenonneg_mul_SNo_Le : ∀ x0 x1 x2 . SNo x0SNoLe 0 x0SNo x1SNo x2SNoLe x1 x2SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Known ordinal_Subq_SNoLeordinal_Subq_SNoLe : ∀ x0 x1 . ordinal x0ordinal x1x0x1SNoLe x0 x1
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Known SNoLe_traSNoLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLe x1 x2SNoLe x0 x2
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Known minus_SNo_Le_contraminus_SNo_Le_contra : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1SNoLe (minus_SNo x1) (minus_SNo x0)
Theorem divides_int_pos_Ledivides_int_pos_Le : ∀ x0 x1 . divides_int x0 x1SNoLt 0 x1SNoLe x0 x1 (proof)
Definition gcd_relngcd_reln := λ x0 x1 x2 . and (and (divides_int x2 x0) (divides_int x2 x1)) (∀ x3 . divides_int x3 x0divides_int x3 x1SNoLe x3 x2)
Known SNoLe_antisymSNoLe_antisym : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1SNoLe x1 x0x0 = x1
Theorem gcd_reln_uniqgcd_reln_uniq : ∀ x0 x1 x2 x3 . gcd_reln x0 x1 x2gcd_reln x0 x1 x3x2 = x3 (proof)
Definition int_lin_combint_lin_comb := λ x0 x1 x2 . and (and (and (x0int) (x1int)) (x2int)) (∀ x3 : ο . (∀ x4 . and (x4int) (∀ x5 : ο . (∀ x6 . and (x6int) (add_SNo (mul_SNo x4 x0) (mul_SNo x6 x1) = x2)x5)x5)x3)x3)
Known and4Iand4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (and (and x0 x1) x2) x3
Theorem int_lin_comb_Iint_lin_comb_I : ∀ x0 . x0int∀ x1 . x1int∀ x2 . x2int(∀ x3 : ο . (∀ x4 . and (x4int) (∀ x5 : ο . (∀ x6 . and (x6int) (add_SNo (mul_SNo x4 x0) (mul_SNo x6 x1) = x2)x5)x5)x3)x3)int_lin_comb x0 x1 x2 (proof)
Theorem int_lin_comb_Eint_lin_comb_E : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2∀ x3 : ο . (x0intx1intx2int∀ x4 . x4int∀ x5 . x5intadd_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2x3)x3 (proof)
Theorem int_lin_comb_E1int_lin_comb_E1 : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2x0int (proof)
Theorem int_lin_comb_E2int_lin_comb_E2 : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2x1int (proof)
Theorem int_lin_comb_E3int_lin_comb_E3 : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2x2int (proof)
Theorem int_lin_comb_E4int_lin_comb_E4 : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2∀ x3 : ο . (∀ x4 . x4int∀ x5 . x5intadd_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2x3)x3 (proof)
Known least_ordinal_exleast_ordinal_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2)x1)x1)∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3x2not (x0 x3))x1)x1
Known int_3_casesint_3_cases : ∀ x0 . x0int∀ x1 : ο . (∀ x2 . x2omegax0 = minus_SNo (ordsucc x2)x1)(x0 = 0x1)(∀ x2 . x2omegax0 = ordsucc x2x1)x1
Known mul_SNo_zeroLmul_SNo_zeroL : ∀ x0 . SNo x0mul_SNo 0 x0 = 0
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known ordinal_SNoordinal_SNo : ∀ x0 . ordinal x0SNo x0
Theorem least_pos_int_lin_comb_exleast_pos_int_lin_comb_ex : ∀ x0 . x0int∀ x1 . x1intnot (and (x0 = 0) (x1 = 0))∀ x2 : ο . (∀ x3 . and (and (int_lin_comb x0 x1 x3) (SNoLt 0 x3)) (∀ x4 . int_lin_comb x0 x1 x4SNoLt 0 x4SNoLe x3 x4)x2)x2 (proof)
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Theorem int_lin_comb_symint_lin_comb_sym : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2int_lin_comb x1 x0 x2 (proof)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known int_mul_SNoint_mul_SNo : ∀ x0 . x0int∀ x1 . x1intmul_SNo x0 x1int
Known mul_SNo_distrLmul_SNo_distrL : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known mul_SNo_assocmul_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Theorem least_pos_int_lin_comb_divides_intleast_pos_int_lin_comb_divides_int : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2SNoLt 0 x2(∀ x3 . int_lin_comb x0 x1 x3SNoLt 0 x3SNoLe x2 x3)divides_int x2 x0 (proof)
Theorem least_pos_int_lin_comb_gcdleast_pos_int_lin_comb_gcd : ∀ x0 x1 x2 . int_lin_comb x0 x1 x2SNoLt 0 x2(∀ x3 . int_lin_comb x0 x1 x3SNoLt 0 x3SNoLe x2 x3)gcd_reln x0 x1 x2 (proof)
Definition iffiff := λ x0 x1 : ο . and (x0x1) (x1x0)
Known iffIiffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Theorem BezoutThmBezoutThm : ∀ x0 . x0int∀ x1 . x1intnot (and (x0 = 0) (x1 = 0))∀ x2 . iff (gcd_reln x0 x1 x2) (and (and (int_lin_comb x0 x1 x2) (SNoLt 0 x2)) (∀ x3 . int_lin_comb x0 x1 x3SNoLt 0 x3SNoLe x2 x3)) (proof)
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known mul_SNo_pos_negmul_SNo_pos_neg : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt x1 0SNoLt (mul_SNo x0 x1) 0
Known 2bbf0..mul_nat_0_or_Subq : ∀ x0 . nat_p x0∀ x1 . nat_p x1or (x1 = 0) (x0mul_nat x0 x1)
Theorem gcd_idgcd_id : ∀ x0 . x0setminus omega (Sing 0)gcd_reln x0 x0 x0 (proof)
Theorem gcd_0gcd_0 : ∀ x0 . x0setminus omega (Sing 0)gcd_reln 0 x0 x0 (proof)
Theorem gcd_symgcd_sym : ∀ x0 x1 x2 . gcd_reln x0 x1 x2gcd_reln x1 x0 x2 (proof)
Theorem gcd_minusgcd_minus : ∀ x0 x1 x2 . gcd_reln x0 x1 x2gcd_reln x0 (minus_SNo x1) x2 (proof)
Known add_SNo_minus_R2'add_SNo_minus_R2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (add_SNo x0 (minus_SNo x1)) x1 = x0
Theorem euclidean_algorithm_prop_1euclidean_algorithm_prop_1 : ∀ x0 x1 x2 . x1intgcd_reln x0 (add_SNo x1 (minus_SNo x0)) x2gcd_reln x0 x1 x2 (proof)
Known and7Iand7I : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . x0x1x2x3x4x5x6and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6
Theorem euclidean_algorithmeuclidean_algorithm : and (and (and (and (and (and (∀ x0 . x0setminus omega (Sing 0)gcd_reln x0 x0 x0) (∀ x0 . x0setminus omega (Sing 0)gcd_reln 0 x0 x0)) (∀ x0 . x0setminus omega (Sing 0)gcd_reln x0 0 x0)) (∀ x0 . x0omega∀ x1 . x1omegaSNoLt x0 x1∀ x2 . gcd_reln x0 (add_SNo x1 (minus_SNo x0)) x2gcd_reln x0 x1 x2)) (∀ x0 . x0omega∀ x1 . x1omegaSNoLt x1 x0∀ x2 . gcd_reln x1 x0 x2gcd_reln x0 x1 x2)) (∀ x0 . x0omega∀ x1 . x1intSNoLt x1 0∀ x2 . gcd_reln x0 (minus_SNo x1) x2gcd_reln x0 x1 x2)) (∀ x0 . x0int∀ x1 . x1intSNoLt x0 0∀ x2 . gcd_reln (minus_SNo x0) x1 x2gcd_reln x0 x1 x2) (proof)
Definition prime_natprime_nat := λ x0 . and (and (x0omega) (1x0)) (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known In_0_1In_0_1 : 01
Known SNoLt_0_1SNoLt_0_1 : SNoLt 0 1
Known mul_SNo_rotate_3_1mul_SNo_rotate_3_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo x2 (mul_SNo x0 x1)
Theorem Euclid_lemmaEuclid_lemma : ∀ x0 . prime_nat x0∀ x1 . x1int∀ x2 . x2intdivides_int x0 (mul_SNo x1 x2)or (divides_int x0 x1) (divides_int x0 x2) (proof)
Definition coprime_int := λ x0 x1 . gcd_reln x0 x1 1

previous assets