Search for blocks/addresses/...

Proofgold Asset

asset id
2a5d6848fdcff5bd7eb8fb8dfcdb3c4a38333b0f81ddc9a6fb41b4d4f3bb06cf
asset hash
8dfc66449791a3773cc09b50a583ae0ebc89eb69f2bce95a84eb4dabd752b444
bday / block
27893
tx
be867..
preasset
doc published by PrQUS..
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param realreal : ι
Param famunionfamunion : ι(ιι) → ι
Param ReplSepReplSep : ι(ιο) → (ιι) → ι
Param SNoLtSNoLt : ιιο
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param recip_SNorecip_SNo : ιι
Definition div_SNodiv_SNo := λ x0 x1 . mul_SNo x0 (recip_SNo x1)
Definition SNo_sqrtauxsetSNo_sqrtauxset := λ x0 x1 x2 . famunion x0 (λ x3 . {div_SNo (add_SNo x2 (mul_SNo x3 x4)) (add_SNo x3 x4)|x4 ∈ x1,SNoLt 0 (add_SNo x3 x4)})
Known famunionE_impredfamunionE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . x4x0x2x1 x4x3)x3
Known ReplSepE_impredReplSepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3ReplSep x0 x1 x2∀ x4 : ο . (∀ x5 . x5x0x1 x5x3 = x2 x5x4)x4
Known real_div_SNoreal_div_SNo : ∀ x0 . x0real∀ x1 . x1realdiv_SNo x0 x1real
Known real_add_SNoreal_add_SNo : ∀ x0 . x0real∀ x1 . x1realadd_SNo x0 x1real
Known real_mul_SNoreal_mul_SNo : ∀ x0 . x0real∀ x1 . x1realmul_SNo x0 x1real
Theorem SNo_sqrtauxset_realSNo_sqrtauxset_real : ∀ x0 x1 x2 . x0realx1realx2realSNo_sqrtauxset x0 x1 x2real (proof)
Param SepSep : ι(ιο) → ι
Param SNoLeSNoLe : ιιο
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Param SNoSNo : ιο
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known SNoLeESNoLeE : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1or (SNoLt x0 x1) (x0 = x1)
Known SNo_0SNo_0 : SNo 0
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known real_SNoreal_SNo : ∀ x0 . x0realSNo x0
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known add_SNo_Le3add_SNo_Le3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe x0 x2SNoLe x1 x3SNoLe (add_SNo x0 x1) (add_SNo x2 x3)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known SNoLe_refSNoLe_ref : ∀ x0 . SNoLe x0 x0
Known mul_SNo_zeroLmul_SNo_zeroL : ∀ x0 . SNo x0mul_SNo 0 x0 = 0
Known div_SNo_pos_posdiv_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (div_SNo x0 x1)
Known div_SNo_0_numdiv_SNo_0_num : ∀ x0 . SNo x0div_SNo 0 x0 = 0
Theorem SNo_sqrtauxset_real_nonnegSNo_sqrtauxset_real_nonneg : ∀ x0 x1 x2 . x0Sep real (SNoLe 0)x1Sep real (SNoLe 0)x2realSNoLe 0 x2SNo_sqrtauxset x0 x1 x2Sep real (SNoLe 0) (proof)
Param SNoS_SNoS_ : ιι
Param omegaomega : ι
Param sqrt_SNo_nonnegsqrt_SNo_nonneg : ιι
Param ordinalordinal : ιο
Param SNoLevSNoLev : ιι
Param SNo_SNo_ : ιιο
Known SNoS_E2SNoS_E2 : ∀ x0 . ordinal x0∀ x1 . x1SNoS_ x0∀ x2 : ο . (SNoLev x1x0ordinal (SNoLev x1)SNo x1SNo_ (SNoLev x1) x1x2)x2
Known omega_ordinalomega_ordinal : ordinal omega
Known SNoLev_indSNoLev_ind : ∀ x0 : ι → ο . (∀ x1 . SNo x1(∀ x2 . x2SNoS_ (SNoLev x1)x0 x2)x0 x1)∀ x1 . SNo x1x0 x1
Known ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0)
Known ordinal_Emptyordinal_Empty : ordinal 0
Known SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Param ordsuccordsucc : ιι
Known ordinal_1ordinal_1 : ordinal 1
Param SNoCutSNoCut : ιιι
Param apap : ιιι
Param SNo_sqrtauxSNo_sqrtaux : ι(ιι) → ιι
Known sqrt_SNo_nonneg_eqsqrt_SNo_nonneg_eq : ∀ x0 . SNo x0sqrt_SNo_nonneg x0 = SNoCut (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0)) (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1))
Param nat_pnat_p : ιο
Definition SNoCutPSNoCutP := λ x0 x1 . and (and (∀ x2 . x2x0SNo x2) (∀ x2 . x2x1SNo x2)) (∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3)
Known SNo_sqrt_SNo_SNoCutPSNo_sqrt_SNo_SNoCutP : ∀ x0 . SNo x0SNoLe 0 x0SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))
Known real_SNoCutreal_SNoCut : ∀ x0 . x0real∀ x1 . x1realSNoCutP x0 x1(x0 = 0∀ x2 : ο . x2)(x1 = 0∀ x2 : ο . x2)(∀ x2 . x2x0∀ x3 : ο . (∀ x4 . and (x4x0) (SNoLt x2 x4)x3)x3)(∀ x2 . x2x1∀ x3 : ο . (∀ x4 . and (x4x1) (SNoLt x4 x2)x3)x3)SNoCut x0 x1real
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known sqrt_SNo_nonneg_Lnonemptysqrt_SNo_nonneg_Lnonempty : ∀ x0 . SNo x0SNoLe 0 x00SNoLev x0famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0) = 0∀ x1 : ο . x1
Known sqrt_SNo_nonneg_Rnonemptysqrt_SNo_nonneg_Rnonempty : ∀ x0 . SNo x0SNoLe 0 x01SNoLev x0famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1) = 0∀ x1 : ο . x1
Known SNo_sqrtaux_0_propSNo_sqrtaux_0_prop : ∀ x0 . SNo x0SNoLe 0 x0∀ x1 . nat_p x1∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0)
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known SNo_1SNo_1 : SNo 1
Known SNo_sqrtaux_monSNo_sqrtaux_mon : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2∀ x3 . nat_p x3x2x3and (ap (SNo_sqrtaux x0 x1 x2) 0ap (SNo_sqrtaux x0 x1 x3) 0) (ap (SNo_sqrtaux x0 x1 x2) 1ap (SNo_sqrtaux x0 x1 x3) 1)
Known nat_0nat_0 : nat_p 0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known Subq_EmptySubq_Empty : ∀ x0 . 0x0
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Definition SNoLSNoL := λ x0 . {x1 ∈ SNoS_ (SNoLev x0)|SNoLt x1 x0}
Definition SNoL_nonnegSNoL_nonneg := λ x0 . Sep (SNoL x0) (SNoLe 0)
Definition SNoRSNoR := λ x0 . Sep (SNoS_ (SNoLev x0)) (SNoLt x0)
Known SNo_sqrtaux_0SNo_sqrtaux_0 : ∀ x0 . ∀ x1 : ι → ι . SNo_sqrtaux x0 x1 0 = lam 2 (λ x3 . If_i (x3 = 0) (prim5 (SNoL_nonneg x0) x1) (prim5 (SNoR x0) x1))
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known sqrt_SNo_nonneg_1sqrt_SNo_nonneg_1 : sqrt_SNo_nonneg 1 = 1
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known SNoS_I2SNoS_I2 : ∀ x0 x1 . SNo x0SNo x1SNoLev x0SNoLev x1x0SNoS_ (SNoLev x1)
Known ordinal_SNoLevordinal_SNoLev : ∀ x0 . ordinal x0SNoLev x0 = x0
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
Param binunionbinunion : ιιι
Known SNo_sqrtaux_SSNo_sqrtaux_S : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2SNo_sqrtaux x0 x1 (ordsucc x2) = lam 2 (λ x4 . If_i (x4 = 0) (binunion (ap (SNo_sqrtaux x0 x1 x2) 0) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 x1 x2) 0) (ap (SNo_sqrtaux x0 x1 x2) 1) x0)) (binunion (binunion (ap (SNo_sqrtaux x0 x1 x2) 1) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 x1 x2) 0) (ap (SNo_sqrtaux x0 x1 x2) 0) x0)) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 x1 x2) 1) (ap (SNo_sqrtaux x0 x1 x2) 1) x0)))
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SNo_sqrtauxset_ISNo_sqrtauxset_I : ∀ x0 x1 x2 x3 . x3x0∀ x4 . x4x1SNoLt 0 (add_SNo x3 x4)div_SNo (add_SNo x2 (mul_SNo x3 x4)) (add_SNo x3 x4)SNo_sqrtauxset x0 x1 x2
Known add_SNo_1_1_2add_SNo_1_1_2 : add_SNo 1 1 = 2
Known SNoLt_0_2SNoLt_0_2 : SNoLt 0 2
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known SNoLt_0_1SNoLt_0_1 : SNoLt 0 1
Known famunionIfamunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2x0x3x1 x2x3famunion x0 x1
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known div_mul_SNo_invLdiv_mul_SNo_invL : ∀ x0 x1 . SNo x0SNo x1(x1 = 0∀ x2 : ο . x2)div_SNo (mul_SNo x0 x1) x1 = x0
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known pos_mul_SNo_Lt'pos_mul_SNo_Lt : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt 0 x2SNoLt x0 x1SNoLt (mul_SNo x0 x2) (mul_SNo x1 x2)
Known SNo_recip_SNoSNo_recip_SNo : ∀ x0 . SNo x0SNo (recip_SNo x0)
Known recip_SNo_of_pos_is_posrecip_SNo_of_pos_is_pos : ∀ x0 . SNo x0SNoLt 0 x0SNoLt 0 (recip_SNo x0)
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 add_SNo_Lt1add_SNo_Lt1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x2SNoLt (add_SNo x0 x1) (add_SNo x2 x1)
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known add_SNo_Le1add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x2SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Known add_SNo_Lt3add_SNo_Lt3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt x0 x2SNoLt x1 x3SNoLt (add_SNo x0 x1) (add_SNo x2 x3)
Known SNo_sqrtaux_1_propSNo_sqrtaux_1_prop : ∀ x0 . SNo x0SNoLe 0 x0∀ x1 . nat_p x1∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2))
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known SNoL_ESNoL_E : ∀ x0 . SNo x0∀ x1 . x1SNoL x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x2)x2
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Known omega_TransSetomega_TransSet : TransSet omega
Known SNoR_ESNoR_E : ∀ x0 . SNo x0∀ x1 . x1SNoR x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x2)x2
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Param iffiff : οοο
Definition PNoEq_PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . x3x0iff (x1 x3) (x2 x3)
Definition SNoEq_SNoEq_ := λ x0 x1 x2 . PNoEq_ x0 (λ x3 . x3x1) (λ x3 . x3x2)
Known SNo_eqSNo_eq : ∀ x0 x1 . SNo x0SNo x1SNoLev x0 = SNoLev x1SNoEq_ (SNoLev x0) x0 x1x0 = x1
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Known iffIiffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known SNoLtI3SNoLtI3 : ∀ x0 x1 . SNoLev x1SNoLev x0SNoEq_ (SNoLev x1) x0 x1nIn (SNoLev x1) x0SNoLt x0 x1
Known SNoLev_0SNoLev_0 : SNoLev 0 = 0
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known real_1real_1 : 1real
Known SNoLev_0_eq_0SNoLev_0_eq_0 : ∀ x0 . SNo x0SNoLev x0 = 0x0 = 0
Known Empty_Subq_eqEmpty_Subq_eq : ∀ x0 . x00x0 = 0
Known sqrt_SNo_nonneg_0sqrt_SNo_nonneg_0 : sqrt_SNo_nonneg 0 = 0
Known real_0real_0 : 0real
Known SNoS_omega_realSNoS_omega_real : SNoS_ omegareal
Known SNoS_ISNoS_I : ∀ x0 . ordinal x0∀ x1 x2 . x2x0SNo_ x2 x1x1SNoS_ x0
Known SNoLev_SNoLev_ : ∀ x0 . SNo x0SNo_ (SNoLev x0) x0
Theorem sqrt_SNo_nonneg_SNoS_omegasqrt_SNo_nonneg_SNoS_omega : ∀ x0 . x0SNoS_ omegaSNoLe 0 x0sqrt_SNo_nonneg x0real (proof)
Param minus_SNominus_SNo : ιι
Param abs_SNoabs_SNo : ιι
Param eps_eps_ : ιι
Known real_Ereal_E : ∀ x0 . x0real∀ x1 : ο . (SNo x0SNoLev x0ordsucc omegax0SNoS_ (ordsucc omega)SNoLt (minus_SNo omega) x0SNoLt x0 omega(∀ x2 . x2SNoS_ omega(∀ x3 . x3omegaSNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3))x2 = x0)(∀ x2 . x2omega∀ x3 : ο . (∀ x4 . and (x4SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 (eps_ x2))))x3)x3)x1)x1
Known sqrt_SNo_nonneg_prop1sqrt_SNo_nonneg_prop1 : ∀ x0 . SNo x0SNoLe 0 x0and (and (SNo (sqrt_SNo_nonneg x0)) (SNoLe 0 (sqrt_SNo_nonneg x0))) (mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0)
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known SNoCutP_SNoCut_impredSNoCutP_SNoCut_impred : ∀ x0 x1 . SNoCutP x0 x1∀ x2 : ο . (SNo (SNoCut x0 x1)SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x3 . ordsucc (SNoLev x3))) (famunion x1 (λ x3 . ordsucc (SNoLev x3))))(∀ x3 . x3x0SNoLt x3 (SNoCut x0 x1))(∀ x3 . x3x1SNoLt (SNoCut x0 x1) x3)(∀ x3 . SNo x3(∀ x4 . x4x0SNoLt x4 x3)(∀ x4 . x4x1SNoLt x3 x4)and (SNoLev (SNoCut x0 x1)SNoLev x3) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x3))x2)x2
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known div_SNo_pos_LtRdiv_SNo_pos_LtR : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt 0 x1SNoLt (mul_SNo x2 x1) x0SNoLt x2 (div_SNo x0 x1)
Known pos_mul_SNo_Lt2pos_mul_SNo_Lt2 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt 0 x0SNoLt 0 x1SNoLt x0 x2SNoLt x1 x3SNoLt (mul_SNo x0 x1) (mul_SNo x2 x3)
Known add_SNo_Lt3badd_SNo_Lt3b : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe x0 x2SNoLt x1 x3SNoLt (add_SNo x0 x1) (add_SNo x2 x3)
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Known div_SNo_pos_LtLdiv_SNo_pos_LtL : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt 0 x1SNoLt x0 (mul_SNo x2 x1)SNoLt (div_SNo x0 x1) x2
Known nat_1nat_1 : nat_p 1
Known sqrt_SNo_nonneg_nonnegsqrt_SNo_nonneg_nonneg : ∀ x0 . SNo x0SNoLe 0 x0SNoLe 0 (sqrt_SNo_nonneg x0)
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Theorem sqrt_SNo_nonneg_realsqrt_SNo_nonneg_real : ∀ x0 . x0realSNoLe 0 x0sqrt_SNo_nonneg x0real (proof)
Param intint : ι
Param setminussetminus : ιιι
Param SingSing : ιι
Definition rationalrational := {x0 ∈ real|∀ x1 : ο . (∀ x2 . and (x2int) (∀ x3 : ο . (∀ x4 . and (x4setminus omega (Sing 0)) (x0 = div_SNo x2 x4)x3)x3)x1)x1}
Param mul_natmul_nat : ιιι
Known form100_1_v1form100_1_v1 : ∀ x0 . x0setminus omega 1∀ x1 . x1setminus omega 1mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)∀ x2 : ο . x2
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known omega_SNoS_omegaomega_SNoS_omega : omegaSNoS_ omega
Known nat_2nat_2 : nat_p 2
Known int_3_casesint_3_cases : ∀ x0 . x0int∀ x1 : ο . (∀ x2 . x2omegax0 = minus_SNo (ordsucc x2)x1)(x0 = 0x1)(∀ x2 . x2omegax0 = ordsucc x2x1)x1
Known SNo_2SNo_2 : SNo 2
Known div_SNo_neg_posdiv_SNo_neg_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 0SNoLt 0 x1SNoLt (div_SNo x0 x1) 0
Known int_SNoint_SNo : ∀ x0 . x0intSNo x0
Known minus_SNo_Lt_contra1minus_SNo_Lt_contra1 : ∀ x0 x1 . SNo x0SNo x1SNoLt (minus_SNo x0) x1SNoLt (minus_SNo x1) x0
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Known ordinal_ordsucc_SNo_eqordinal_ordsucc_SNo_eq : ∀ x0 . ordinal x0ordsucc x0 = add_SNo 1 x0
Known add_SNo_Le2add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x1 x2SNoLe (add_SNo x0 x1) (add_SNo x0 x2)
Known omega_nonnegomega_nonneg : ∀ x0 . x0omegaSNoLe 0 x0
Known neq_ordsucc_0neq_ordsucc_0 : ∀ x0 . ordsucc x0 = 0∀ x1 : ο . x1
Known eq_1_Sing0eq_1_Sing0 : 1 = Sing 0
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known mul_SNo_com_4_inner_midmul_SNo_com_4_inner_mid : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo (mul_SNo x0 x1) (mul_SNo x2 x3) = mul_SNo (mul_SNo x0 x2) (mul_SNo x1 x3)
Known sqrt_SNo_nonneg_sqrsqrt_SNo_nonneg_sqr : ∀ x0 . SNo x0SNoLe 0 x0mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known SingISingI : ∀ x0 . x0Sing x0
Known mul_div_SNo_invLmul_div_SNo_invL : ∀ x0 x1 . SNo x0SNo x1(x1 = 0∀ x2 : ο . x2)mul_SNo (div_SNo x0 x1) x1 = x0
Known SNo_sqrt_SNo_nonnegSNo_sqrt_SNo_nonneg : ∀ x0 . SNo x0SNoLe 0 x0SNo (sqrt_SNo_nonneg x0)
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Theorem sqrt_2_irrationalsqrt_2_irrational : sqrt_SNo_nonneg 2setminus real rational (proof)