Search for blocks/addresses/...

Proofgold Asset

asset id
01deda1c3488cb60edda5ff2d77eb1f932ba664ff3790ca553e2ea6a28dc619b
asset hash
a9529ce49ce79142cc701896b00c8558eb4b9f926c7fe07940a2661e889b04d7
bday / block
29757
tx
00571..
preasset
doc published by PrQUS..
Param omegaomega : ι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param mul_natmul_nat : ιιι
Definition divides_natdivides_nat := λ x0 x1 . and (and (x0omega) (x1omega)) (∀ x2 : ο . (∀ x3 . and (x3omega) (mul_nat x0 x3 = x1)x2)x2)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Param nat_pnat_p : ιο
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem divides_nat_mulRdivides_nat_mulR : ∀ x0 . x0omega∀ x1 . x1omegadivides_nat x0 (mul_nat x0 x1) (proof)
Known mul_nat_commul_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = mul_nat x1 x0
Theorem divides_nat_mulLdivides_nat_mulL : ∀ x0 . x0omega∀ x1 . x1omegadivides_nat x1 (mul_nat x0 x1) (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param ordsuccordsucc : ιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known nat_inv_imprednat_inv_impred : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Theorem nat_le1_casesnat_le1_cases : ∀ x0 . nat_p x0x01or (x0 = 0) (x0 = 1) (proof)
Definition composite_natcomposite_nat := λ x0 . and (x0omega) (∀ x1 : ο . (∀ x2 . and (x2omega) (∀ x3 : ο . (∀ x4 . and (x4omega) (and (and (1x2) (1x4)) (mul_nat x2 x4 = x0))x3)x3)x1)x1)
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 dnegdneg : ∀ x0 : ο . not (not x0)x0
Param ordinalordinal : ιο
Known ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0)
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known nat_1nat_1 : nat_p 1
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known In_0_1In_0_1 : 01
Known mul_nat_0Lmul_nat_0L : ∀ x0 . nat_p x0mul_nat 0 x0 = 0
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Theorem prime_nat_or_composite_natprime_nat_or_composite_nat : ∀ x0 . x0omega1x0or (prime_nat x0) (composite_nat x0) (proof)
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known 91381..divides_nat_ref : ∀ x0 . nat_p x0divides_nat x0 x0
Known 58a75.. : ∀ x0 x1 . nat_p x0nat_p x10x01x1x0mul_nat x0 x1
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known e4e38..divides_nat_tra : ∀ x0 x1 x2 . divides_nat x0 x1divides_nat x1 x2divides_nat x0 x2
Theorem prime_nat_divisor_exprime_nat_divisor_ex : ∀ x0 . nat_p x01x0∀ x1 : ο . (∀ x2 . and (prime_nat x2) (divides_nat x2 x0)x1)x1 (proof)
Param add_natadd_nat : ιιι
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known df9cc..mul_nat_Subq_L : ∀ x0 x1 . nat_p x0nat_p x1x0x1∀ x2 . nat_p x2mul_nat x2 x0mul_nat x2 x1
Known ordinal_ordsucc_In_Subqordinal_ordsucc_In_Subq : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known add_nat_SLadd_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known nat_0nat_0 : nat_p 0
Known add_nat_0Ladd_nat_0L : ∀ x0 . nat_p x0add_nat 0 x0 = x0
Known 9cc32.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2x1x2add_nat x1 x0add_nat x2 x0
Theorem nat_1In_not_divides_ordsuccnat_1In_not_divides_ordsucc : ∀ x0 x1 . 1x0divides_nat x0 x1not (divides_nat x0 (ordsucc x1)) (proof)
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Definition finitefinite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2omega) (equip x0 x2)x1)x1
Definition infiniteinfinite := λ x0 . not (finite x0)
Param SepSep : ι(ιο) → ι
Definition primesprimes := Sep omega prime_nat
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition Pi_natPi_nat := λ x0 : ι → ι . nat_primrec 1 (λ x1 x2 . mul_nat x2 (x0 x1))
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem Pi_nat_0Pi_nat_0 : ∀ x0 : ι → ι . Pi_nat x0 0 = 1 (proof)
Known nat_primrec_Snat_primrec_S : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Theorem Pi_nat_SPi_nat_S : ∀ x0 : ι → ι . ∀ x1 . nat_p x1Pi_nat x0 (ordsucc x1) = mul_nat (Pi_nat x0 x1) (x0 x1) (proof)
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem Pi_nat_pPi_nat_p : ∀ x0 : ι → ι . ∀ x1 . nat_p x1(∀ x2 . x2x1nat_p (x0 x2))nat_p (Pi_nat x0 x1) (proof)
Known neq_1_0neq_1_0 : 1 = 0∀ x0 : ο . x0
Known mul_nat_0_invmul_nat_0_inv : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = 0or (x0 = 0) (x1 = 0)
Theorem Pi_nat_0_invPi_nat_0_inv : ∀ x0 : ι → ι . ∀ x1 . nat_p x1(∀ x2 . x2x1nat_p (x0 x2))Pi_nat x0 x1 = 0∀ x2 : ο . (∀ x3 . and (x3x1) (x0 x3 = 0)x2)x2 (proof)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Theorem Pi_nat_dividesPi_nat_divides : ∀ x0 : ι → ι . ∀ x1 . nat_p x1(∀ x2 . x2x1nat_p (x0 x2))∀ x2 . x2x1divides_nat (x0 x2) (Pi_nat x0 x1) (proof)
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known ordinal_Emptyordinal_Empty : ordinal 0
Known Empty_Subq_eqEmpty_Subq_eq : ∀ x0 . x00x0 = 0
Known SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Theorem form100_11_infinite_primesform100_11_infinite_primes : infinite primes (proof)