Primitive. The name Eps_i is a term of type (setprop)set.
L2
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : setprop, ∀x : set, P xP (Eps_i P)
L3
Definition. We define True to be ∀p : prop, pp of type prop.
L4
Definition. We define False to be ∀p : prop, p of type prop.
L5
Definition. We define not to be λA : propAFalse of type propprop.
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
L8
Definition. We define and to be λA B : prop∀p : prop, (ABp)p of type proppropprop.
Notation. We use as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
L11
Definition. We define or to be λA B : prop∀p : prop, (Ap)(Bp)p of type proppropprop.
Notation. We use as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
L14
Definition. We define iff to be λA B : propand (AB) (BA) of type proppropprop.
Notation. We use as an infix operator with priority 805 and no associativity corresponding to applying term iff.
Beginning of Section Eq
L18
Variable A : SType
L19
Definition. We define eq to be λx y : A∀Q : AAprop, Q x yQ y x of type AAprop.
L20
Definition. We define neq to be λx y : A¬ eq x y of type AAprop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section FE
L26
Variable A B : SType
L27
Axiom. (func_ext) We take the following as an axiom:
∀f g : AB, (∀x : A, f x = g x)f = g
End of Section FE
Beginning of Section Ex
L30
Variable A : SType
L31
Definition. We define ex to be λQ : Aprop∀P : prop, (∀x : A, Q xP)P of type (Aprop)prop.
End of Section Ex
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
L35
Axiom. (prop_ext) We take the following as an axiom:
∀p q : prop, iff p qp = q
Primitive. The name In is a term of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write xA, B to mean x : set, xAB.
L37
Definition. We define Subq to be λA B ⇒ ∀xA, x B of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write xA, B to mean x : set, xAB.
L38
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X YY XX = Y
L39
Axiom. (In_ind) We take the following as an axiom:
∀P : setprop, (∀X : set, (∀xX, P x)P X)∀X : set, P X
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Primitive. The name Empty is a term of type set.
L42
Axiom. (EmptyAx) We take the following as an axiom:
¬ ∃x : set, x Empty
Primitive. The name is a term of type setset.
L45
Axiom. (UnionEq) We take the following as an axiom:
∀X x, x X ∃Y, x Y Y X
Primitive. The name 𝒫 is a term of type setset.
L48
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y 𝒫 X Y X
Primitive. The name Repl is a term of type set(setset)set.
Notation. {B| xA} is notation for Repl Ax . B).
L51
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA} ∃xA, y = F x
L52
Definition. We define TransSet to be λU : set∀xU, x U of type setprop.
L53
Definition. We define Union_closed to be λU : set∀X : set, X U X U of type setprop.
L54
Definition. We define Power_closed to be λU : set∀X : set, X U𝒫 X U of type setprop.
L55
Definition. We define Repl_closed to be λU : set∀X : set, X U∀F : setset, (∀x : set, x XF x U){F x|xX} U of type setprop.
L57
Definition. We define ZF_closed to be λU : setUnion_closed U Power_closed U Repl_closed U of type setprop.
Primitive. The name UnivOf is a term of type setset.
L62
Axiom. (UnivOf_In) We take the following as an axiom:
∀N : set, N UnivOf N
L63
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet (UnivOf N)
L64
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed (UnivOf N)
L65
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N UTransSet UZF_closed UUnivOf N U
L69
Theorem. (andI)
∀A B : prop, ABA B
Proof:
Proof not loaded.
L73
Theorem. (orIL)
∀A B : prop, AA B
Proof:
Proof not loaded.
L77
Theorem. (orIR)
∀A B : prop, BA B
Proof:
Proof not loaded.
L81
Theorem. (iffI)
∀A B : prop, (AB)(BA)(A B)
Proof:
Proof not loaded.
L85
Theorem. (pred_ext)
∀P Q : setprop, (∀x, P x Q x)P = Q
Proof:
Proof not loaded.
L91
Definition. We define nIn to be λx X ⇒ ¬ In x X of type setsetprop.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
L96
Theorem. (EmptyE)
∀x : set, x Empty
Proof:
Proof not loaded.
L102
Theorem. (PowerI)
∀X Y : set, Y XY 𝒫 X
Proof:
Proof not loaded.
L106
Theorem. (Subq_Empty)
∀X : set, Empty X
Proof:
Proof not loaded.
L110
Theorem. (Empty_In_Power)
∀X : set, Empty 𝒫 X
Proof:
Proof not loaded.
L114
Theorem. (xm)
∀P : prop, P ¬ P
Proof:
Proof not loaded.
L165
Theorem. (FalseE)
False∀p : prop, p
Proof:
Proof not loaded.
L169
Theorem. (andEL)
∀A B : prop, A BA
Proof:
Proof not loaded.
L173
Theorem. (andER)
∀A B : prop, A BB
Proof:
Proof not loaded.
Beginning of Section PropN
L179
Variable P1 P2 P3 : prop
L180
Theorem. (and3I)
P1P2P3P1 P2 P3
Proof:
Proof not loaded.
L184
Theorem. (and3E)
P1 P2 P3(∀p : prop, (P1P2P3p)p)
Proof:
Proof not loaded.
L188
Theorem. (or3I1)
P1P1 P2 P3
Proof:
Proof not loaded.
L192
Theorem. (or3I2)
P2P1 P2 P3
Proof:
Proof not loaded.
L196
Theorem. (or3I3)
P3P1 P2 P3
Proof:
Proof not loaded.
L200
Theorem. (or3E)
P1 P2 P3(∀p : prop, (P1p)(P2p)(P3p)p)
Proof:
Proof not loaded.
L204
Variable P4 : prop
L206
Theorem. (and4I)
P1P2P3P4P1 P2 P3 P4
Proof:
Proof not loaded.
L210
Variable P5 : prop
L212
Theorem. (and5I)
P1P2P3P4P5P1 P2 P3 P4 P5
Proof:
Proof not loaded.
L216
Variable P6 : prop
L218
Theorem. (and6I)
P1P2P3P4P5P6P1 P2 P3 P4 P5 P6
Proof:
Proof not loaded.
L222
Variable P7 : prop
L224
Theorem. (and7I)
P1P2P3P4P5P6P7P1 P2 P3 P4 P5 P6 P7
Proof:
Proof not loaded.
End of Section PropN
L230
Theorem. (not_or_and_demorgan)
∀A B : prop, ¬ (A B)¬ A ¬ B
Proof:
Proof not loaded.
L238
Theorem. (not_ex_all_demorgan_i)
∀P : setprop, (¬ ∃x, P x)∀x, ¬ P x
Proof:
Proof not loaded.
L244
Theorem. (iffEL)
∀A B : prop, (A B)AB
Proof:
Proof not loaded.
L248
Theorem. (iffER)
∀A B : prop, (A B)BA
Proof:
Proof not loaded.
L252
Theorem. (iff_refl)
∀A : prop, A A
Proof:
Proof not loaded.
L256
Theorem. (iff_sym)
∀A B : prop, (A B)(B A)
Proof:
Proof not loaded.
L265
Theorem. (iff_trans)
∀A B C : prop, (A B)(B C)(A C)
Proof:
Proof not loaded.
L278
Theorem. (eq_i_tra)
∀x y z, x = yy = zx = z
Proof:
Proof not loaded.
L282
Theorem. (neq_i_sym)
∀x y, x yy x
Proof:
Proof not loaded.
L286
Theorem. (Eps_i_ex)
∀P : setprop, (∃x, P x)P (Eps_i P)
Proof:
Proof not loaded.
L292
Theorem. (prop_ext_2)
∀p q : prop, (pq)(qp)p = q
Proof:
Proof not loaded.
L298
Theorem. (Subq_ref)
∀X : set, X X
Proof:
Proof not loaded.
L302
Theorem. (Subq_tra)
∀X Y Z : set, X YY ZX Z
Proof:
Proof not loaded.
L306
Theorem. (Empty_Subq_eq)
∀X : set, X EmptyX = Empty
Proof:
Proof not loaded.
L314
Theorem. (Empty_eq)
∀X : set, (∀x, x X)X = Empty
Proof:
Proof not loaded.
L324
Theorem. (UnionI)
∀X x Y : set, x YY Xx X
Proof:
Proof not loaded.
L337
Theorem. (UnionE)
∀X x : set, x X∃Y : set, x Y Y X
Proof:
Proof not loaded.
L341
Theorem. (UnionE_impred)
∀X x : set, x X∀p : prop, (∀Y : set, x YY Xp)p
Proof:
Proof not loaded.
L349
Theorem. (PowerE)
∀X Y : set, Y 𝒫 XY X
Proof:
Proof not loaded.
L353
Theorem. (Self_In_Power)
∀X : set, X 𝒫 X
Proof:
Proof not loaded.
L357
Theorem. (dneg)
∀P : prop, ¬ ¬ PP
Proof:
Proof not loaded.
L366
Theorem. (not_all_ex_demorgan_i)
∀P : setprop, ¬ (∀x, P x)∃x, ¬ P x
Proof:
Proof not loaded.
L376
Theorem. (eq_or_nand)
or = (λx y : prop¬ (¬ x ¬ y))
Proof:
Proof not loaded.
L393
Definition. We define exactly1of2 to be λA B : propA ¬ B ¬ A B of type proppropprop.
L395
Theorem. (exactly1of2_I1)
∀A B : prop, A¬ Bexactly1of2 A B
Proof:
Proof not loaded.
L405
Theorem. (exactly1of2_I2)
∀A B : prop, ¬ ABexactly1of2 A B
Proof:
Proof not loaded.
L415
Theorem. (exactly1of2_E)
∀A B : prop, exactly1of2 A B∀p : prop, (A¬ Bp)(¬ ABp)p
Proof:
Proof not loaded.
L430
Theorem. (exactly1of2_or)
∀A B : prop, exactly1of2 A BA B
Proof:
Proof not loaded.
L438
Theorem. (ReplI)
∀A : set, ∀F : setset, ∀x : set, x AF x {F x|xA}
Proof:
Proof not loaded.
L448
Theorem. (ReplE)
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}∃xA, y = F x
Proof:
Proof not loaded.
L452
Theorem. (ReplE_impred)
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}∀p : prop, (∀x : set, x Ay = F xp)p
Proof:
Proof not loaded.
L461
Theorem. (ReplE')
∀X, ∀f : setset, ∀p : setprop, (∀xX, p (f x))∀y{f x|xX}, p y
Proof:
Proof not loaded.
L468
Theorem. (Repl_Empty)
∀F : setset, {F x|xEmpty} = Empty
Proof:
Proof not loaded.
L479
Theorem. (ReplEq_ext_sub)
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} {G x|xX}
Proof:
Proof not loaded.
L494
Theorem. (ReplEq_ext)
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} = {G x|xX}
Proof:
Proof not loaded.
L503
Theorem. (Repl_inv_eq)
∀P : setprop, ∀f g : setset, (∀x, P xg (f x) = x)∀X, (∀xX, P x){g y|y{f x|xX}} = X
Proof:
Proof not loaded.
L527
Theorem. (Repl_invol_eq)
∀P : setprop, ∀f : setset, (∀x, P xf (f x) = x)∀X, (∀xX, P x){f y|y{f x|xX}} = X
Proof:
Proof not loaded.
L536
Definition. We define If_i to be (λp x y ⇒ Eps_i (λz : setp z = x ¬ p z = y)) of type propsetsetset.
Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.
L538
Theorem. (If_i_correct)
∀p : prop, ∀x y : set, p (if p then x else y) = x ¬ p (if p then x else y) = y
Proof:
Proof not loaded.
L560
Theorem. (If_i_0)
∀p : prop, ∀x y : set, ¬ p(if p then x else y) = y
Proof:
Proof not loaded.
L571
Theorem. (If_i_1)
∀p : prop, ∀x y : set, p(if p then x else y) = x
Proof:
Proof not loaded.
L582
Theorem. (If_i_or)
∀p : prop, ∀x y : set, (if p then x else y) = x (if p then x else y) = y
Proof:
Proof not loaded.
L591
Definition. We define UPair to be λy z ⇒ {if Empty X then y else z|X𝒫 (𝒫 Empty)} of type setsetset.
Notation. {x,y} is notation for UPair x y.
L594
Theorem. (UPairE)
∀x y z : set, x {y,z}x = y x = z
Proof:
Proof not loaded.
L614
Theorem. (UPairI1)
∀y z : set, y {y,z}
Proof:
Proof not loaded.
L625
Theorem. (UPairI2)
∀y z : set, z {y,z}
Proof:
Proof not loaded.
L638
Definition. We define Sing to be λx ⇒ {x,x} of type setset.
Notation. {x} is notation for Sing x.
L640
Theorem. (SingI)
∀x : set, x {x}
Proof:
Proof not loaded.
L644
Theorem. (SingE)
∀x y : set, y {x}y = x
Proof:
Proof not loaded.
L650
Definition. We define binunion to be λX Y ⇒ {X,Y} of type setsetset.
Notation. We use as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
L653
Theorem. (binunionI1)
∀X Y z : set, z Xz X Y
Proof:
Proof not loaded.
L663
Theorem. (binunionI2)
∀X Y z : set, z Yz X Y
Proof:
Proof not loaded.
L673
Theorem. (binunionE)
∀X Y z : set, z X Yz X z Y
Proof:
Proof not loaded.
L696
Theorem. (binunionE')
∀X Y z, ∀p : prop, (z Xp)(z Yp)(z X Yp)
Proof:
Proof not loaded.
L703
Theorem. (binunion_asso)
∀X Y Z : set, X (Y Z) = (X Y) Z
Proof:
Proof not loaded.
L729
Theorem. (binunion_com_Subq)
∀X Y : set, X Y Y X
Proof:
Proof not loaded.
L737
Theorem. (binunion_com)
∀X Y : set, X Y = Y X
Proof:
Proof not loaded.
L743
Theorem. (binunion_idl)
∀X : set, Empty X = X
Proof:
Proof not loaded.
L752
Theorem. (binunion_idr)
∀X : set, X Empty = X
Proof:
Proof not loaded.
L758
Theorem. (binunion_Subq_1)
∀X Y : set, X X Y
Proof:
Proof not loaded.
L762
Theorem. (binunion_Subq_2)
∀X Y : set, Y X Y
Proof:
Proof not loaded.
L766
Theorem. (binunion_Subq_min)
∀X Y Z : set, X ZY ZX Y Z
Proof:
Proof not loaded.
L777
Theorem. (Subq_binunion_eq)
∀X Y, (X Y) = (X Y = Y)
Proof:
Proof not loaded.
L793
Definition. We define SetAdjoin to be λX y ⇒ X {y} of type setsetset.
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.
L797
Definition. We define famunion to be λX F ⇒ {F x|xX} of type set(setset)set.
Notation. We use x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
L802
Theorem. (famunionI)
∀X : set, ∀F : (setset), ∀x y : set, x Xy F xy xXF x
Proof:
Proof not loaded.
L806
Theorem. (famunionE)
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∃xX, y F x
Proof:
Proof not loaded.
L827
Theorem. (famunionE_impred)
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∀p : prop, (∀x, x Xy F xp)p
Proof:
Proof not loaded.
L835
Theorem. (famunion_Empty)
∀F : setset, (xEmptyF x) = Empty
Proof:
Proof not loaded.
L842
Theorem. (famunion_Subq)
∀X, ∀f g : setset, (∀xX, f x g x)famunion X f famunion X g
Proof:
Proof not loaded.
L852
Theorem. (famunion_ext)
∀X, ∀f g : setset, (∀xX, f x = g x)famunion X f = famunion X g
Proof:
Proof not loaded.
Beginning of Section SepSec
L863
Variable X : set
L864
Variable P : setprop
L865
Let z : setEps_i (λz ⇒ z X P z)
L866
Let F : setsetλx ⇒ if P x then x else z
L868
Definition. We define Sep to be if (∃zX, P z) then {F x|xX} else Empty of type set.
End of Section SepSec
Notation. {xA | B} is notation for Sep Ax . B).
L872
Theorem. (SepI)
∀X : set, ∀P : (setprop), ∀x : set, x XP xx {xX|P x}
Proof:
Proof not loaded.
L910
Theorem. (SepE)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X P x
Proof:
Proof not loaded.
L961
Theorem. (SepE1)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X
Proof:
Proof not loaded.
L965
Theorem. (SepE2)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}P x
Proof:
Proof not loaded.
L969
Theorem. (Sep_Empty)
∀P : setprop, {xEmpty|P x} = Empty
Proof:
Proof not loaded.
L975
Theorem. (Sep_Subq)
∀X : set, ∀P : setprop, {xX|P x} X
Proof:
Proof not loaded.
L979
Theorem. (Sep_In_Power)
∀X : set, ∀P : setprop, {xX|P x} 𝒫 X
Proof:
Proof not loaded.
L985
Definition. We define ReplSep to be λX P F ⇒ {F x|x{zX|P z}} of type set(setprop)(setset)set.
Notation. {B| xA, C} is notation for ReplSep Ax . C) (λ x . B).
L987
Theorem. (ReplSepI)
∀X : set, ∀P : setprop, ∀F : setset, ∀x : set, x XP xF x {F x|xX, P x}
Proof:
Proof not loaded.
L991
Theorem. (ReplSepE)
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∃x : set, x X P x y = F x
Proof:
Proof not loaded.
L1010
Theorem. (ReplSepE_impred)
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∀p : prop, (∀xX, P xy = F xp)p
Proof:
Proof not loaded.
L1023
Definition. We define binintersect to be λX Y ⇒ {xX|x Y} of type setsetset.
Notation. We use as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.
L1027
Theorem. (binintersectI)
∀X Y z, z Xz Yz X Y
Proof:
Proof not loaded.
L1031
Theorem. (binintersectE)
∀X Y z, z X Yz X z Y
Proof:
Proof not loaded.
L1035
Theorem. (binintersectE1)
∀X Y z, z X Yz X
Proof:
Proof not loaded.
L1039
Theorem. (binintersectE2)
∀X Y z, z X Yz Y
Proof:
Proof not loaded.
L1043
Theorem. (binintersect_Subq_1)
∀X Y : set, X Y X
Proof:
Proof not loaded.
L1047
Theorem. (binintersect_Subq_2)
∀X Y : set, X Y Y
Proof:
Proof not loaded.
L1051
Theorem. (binintersect_Subq_eq_1)
∀X Y, X YX Y = X
Proof:
Proof not loaded.
L1062
Theorem. (binintersect_Subq_max)
∀X Y Z : set, Z XZ YZ X Y
Proof:
Proof not loaded.
L1073
Theorem. (binintersect_com_Subq)
∀X Y : set, X Y Y X
Proof:
Proof not loaded.
L1079
Theorem. (binintersect_com)
∀X Y : set, X Y = Y X
Proof:
Proof not loaded.
L1087
Definition. We define setminus to be λX Y ⇒ Sep X (λx ⇒ x Y) of type setsetset.
Notation. We use as an infix operator with priority 350 and no associativity corresponding to applying term setminus.
L1091
Theorem. (setminusI)
∀X Y z, (z X)(z Y)z X Y
Proof:
Proof not loaded.
L1095
Theorem. (setminusE)
∀X Y z, (z X Y)z X z Y
Proof:
Proof not loaded.
L1099
Theorem. (setminusE1)
∀X Y z, (z X Y)z X
Proof:
Proof not loaded.
L1103
Theorem. (setminusE2)
∀X Y z, (z X Y)z Y
Proof:
Proof not loaded.
L1107
Theorem. (setminus_Subq)
∀X Y : set, X Y X
Proof:
Proof not loaded.
L1111
Theorem. (setminus_In_Power)
∀A U, A U 𝒫 A
Proof:
Proof not loaded.
L1115
Theorem. (binunion_remove1_eq)
∀X, ∀xX, X = (X {x}) {x}
Proof:
Proof not loaded.
L1140
Theorem. (In_irref)
∀x, x x
Proof:
Proof not loaded.
L1149
Theorem. (In_no2cycle)
∀x y, x yy xFalse
Proof:
Proof not loaded.
L1161
Definition. We define ordsucc to be λx : setx {x} of type setset.
L1162
Theorem. (ordsuccI1)
∀x : set, x ordsucc x
Proof:
Proof not loaded.
L1167
Theorem. (ordsuccI2)
∀x : set, x ordsucc x
Proof:
Proof not loaded.
L1171
Theorem. (ordsuccE)
∀x y : set, y ordsucc xy x y = x
Proof:
Proof not loaded.
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
L1181
Theorem. (neq_0_ordsucc)
∀a : set, 0 ordsucc a
Proof:
Proof not loaded.
L1189
Theorem. (neq_ordsucc_0)
∀a : set, ordsucc a 0
Proof:
Proof not loaded.
L1193
Theorem. (ordsucc_inj)
∀a b : set, ordsucc a = ordsucc ba = b
Proof:
Proof not loaded.
L1214
Theorem. (In_0_1)
Proof:
Proof not loaded.
L1218
Theorem. (In_0_2)
Proof:
Proof not loaded.
L1222
Theorem. (In_1_2)
Proof:
Proof not loaded.
L1226
Definition. We define nat_p to be λn : set∀p : setprop, p 0(∀x : set, p xp (ordsucc x))p n of type setprop.
L1228
Theorem. (nat_0)
Proof:
Proof not loaded.
L1232
Theorem. (nat_ordsucc)
∀n : set, nat_p nnat_p (ordsucc n)
Proof:
Proof not loaded.
L1236
Theorem. (nat_1)
Proof:
Proof not loaded.
L1240
Theorem. (nat_2)
Proof:
Proof not loaded.
L1244
Theorem. (nat_0_in_ordsucc)
∀n, nat_p n0 ordsucc n
Proof:
Proof not loaded.
L1256
Theorem. (nat_ordsucc_in_ordsucc)
∀n, nat_p n∀mn, ordsucc m ordsucc n
Proof:
Proof not loaded.
L1282
Theorem. (nat_ind)
∀p : setprop, p 0(∀n, nat_p np np (ordsucc n))∀n, nat_p np n
Proof:
Proof not loaded.
L1307
Theorem. (nat_complete_ind)
∀p : setprop, (∀n, nat_p n(∀mn, p m)p n)∀n, nat_p np n
Proof:
Proof not loaded.
L1337
Theorem. (nat_inv_impred)
∀p : setprop, p 0(∀n, nat_p np (ordsucc n))∀n, nat_p np n
Proof:
Proof not loaded.
L1341
Theorem. (nat_inv)
∀n, nat_p nn = 0 ∃x, nat_p x n = ordsucc x
Proof:
Proof not loaded.
L1349
Theorem. (nat_p_trans)
∀n, nat_p n∀mn, nat_p m
Proof:
Proof not loaded.
L1370
Theorem. (nat_trans)
∀n, nat_p n∀mn, m n
Proof:
Proof not loaded.
L1396
Theorem. (nat_ordsucc_trans)
∀n, nat_p n∀mordsucc n, m n
Proof:
Proof not loaded.
L1412
Definition. We define surj to be λX Y f ⇒ (∀uX, f u Y) (∀wY, ∃uX, f u = w) of type setset(setset)prop.
L1418
Theorem. (form100_63_surjCantor)
∀A : set, ∀f : setset, ¬ surj A (𝒫 A) f
Proof:
Proof not loaded.
L1444
Definition. We define inj to be λX Y f ⇒ (∀uX, f u Y) (∀u vX, f u = f vu = v) of type setset(setset)prop.
L1450
Theorem. (form100_63_injCantor)
∀A : set, ∀f : setset, ¬ inj (𝒫 A) A f
Proof:
Proof not loaded.
L1481
Theorem. (injI)
∀X Y, ∀f : setset, (∀xX, f x Y)(∀x zX, f x = f zx = z)inj X Y f
Proof:
Proof not loaded.
L1489
Theorem. (inj_comp)
∀X Y Z : set, ∀f g : setset, inj X Y finj Y Z ginj X Z (λx ⇒ g (f x))
Proof:
Proof not loaded.
L1509
Definition. We define bij to be λX Y f ⇒ (∀uX, f u Y) (∀u vX, f u = f vu = v) (∀wY, ∃uX, f u = w) of type setset(setset)prop.
L1517
Theorem. (bijI)
∀X Y, ∀f : setset, (∀uX, f u Y)(∀u vX, f u = f vu = v)(∀wY, ∃uX, f u = w)bij X Y f
Proof:
Proof not loaded.
L1532
Theorem. (bijE)
∀X Y, ∀f : setset, bij X Y f∀p : prop, ((∀uX, f u Y)(∀u vX, f u = f vu = v)(∀wY, ∃uX, f u = w)p)p
Proof:
Proof not loaded.
L1546
Theorem. (bij_inj)
∀X Y, ∀f : setset, bij X Y finj X Y f
Proof:
Proof not loaded.
L1550
Theorem. (bij_id)
∀X, bij X X (λx ⇒ x)
Proof:
Proof not loaded.
L1561
Theorem. (bij_comp)
∀X Y Z : set, ∀f g : setset, bij X Y fbij Y Z gbij X Z (λx ⇒ g (f x))
Proof:
Proof not loaded.
L1593
Theorem. (bij_surj)
∀X Y, ∀f : setset, bij X Y fsurj X Y f
Proof:
Proof not loaded.
L1603
Definition. We define inv to be λX f ⇒ λy : setEps_i (λx ⇒ x X f x = y) of type set(setset)setset.
L1605
Theorem. (surj_rinv)
∀X Y, ∀f : setset, (∀wY, ∃uX, f u = w)∀yY, inv X f y X f (inv X f y) = y
Proof:
Proof not loaded.
L1614
Theorem. (inj_linv)
∀X, ∀f : setset, (∀u vX, f u = f vu = v)∀xX, inv X f (f x) = x
Proof:
Proof not loaded.
L1629
Theorem. (bij_inv)
∀X Y, ∀f : setset, bij X Y fbij Y X (inv X f)
Proof:
Proof not loaded.
L1670
Definition. We define atleastp to be λX Y : set∃f : setset, inj X Y f of type setsetprop.
L1673
Theorem. (atleastp_tra)
∀X Y Z, atleastp X Yatleastp Y Zatleastp X Z
Proof:
Proof not loaded.
L1687
Theorem. (Subq_atleastp)
∀X Y, X Yatleastp X Y
Proof:
Proof not loaded.
L1700
Definition. We define equip to be λX Y : set∃f : setset, bij X Y f of type setsetprop.
L1703
Theorem. (equip_atleastp)
∀X Y, equip X Yatleastp X Y
Proof:
Proof not loaded.
L1713
Theorem. (equip_ref)
∀X, equip X X
Proof:
Proof not loaded.
L1720
Theorem. (equip_sym)
∀X Y, equip X Yequip Y X
Proof:
Proof not loaded.
L1729
Theorem. (equip_tra)
∀X Y Z, equip X Yequip Y Zequip X Z
Proof:
Proof not loaded.
L1740
Theorem. (equip_0_Empty)
∀X, equip X 0X = 0
Proof:
Proof not loaded.
L1753
Theorem. (equip_adjoin_ordsucc)
∀N X y, y Xequip N Xequip (ordsucc N) (X {y})
Proof:
Proof not loaded.
L1843
Theorem. (equip_ordsucc_remove1)
∀X N, ∀xX, equip X (ordsucc N)equip (X {x}) N
Proof:
Proof not loaded.
Beginning of Section SchroederBernstein
L2039
Theorem. (KnasterTarski_set)
∀A, ∀F : setset, (∀U𝒫 A, F U 𝒫 A)(∀U V𝒫 A, U VF U F V)∃Y𝒫 A, F Y = Y
Proof:
Proof not loaded.
L2080
Theorem. (image_In_Power)
∀A B, ∀f : setset, (∀xA, f x B)∀U𝒫 A, {f x|xU} 𝒫 B
Proof:
Proof not loaded.
L2093
Theorem. (image_monotone)
∀f : setset, ∀U V, U V{f x|xU} {f x|xV}
Proof:
Proof not loaded.
L2104
Theorem. (setminus_antimonotone)
∀A U V, U VA V A U
Proof:
Proof not loaded.
L2112
Theorem. (SchroederBernstein)
∀A B, ∀f g : setset, inj A B finj B A gequip A B
Proof:
Proof not loaded.
L2266
Theorem. (atleastp_antisym_equip)
∀A B, atleastp A Batleastp B Aequip A B
Proof:
Proof not loaded.
End of Section SchroederBernstein
Beginning of Section PigeonHole
L2281
Theorem. (PigeonHole_nat)
∀n, nat_p n∀f : setset, (∀iordsucc n, f i n)¬ (∀i jordsucc n, f i = f ji = j)
Proof:
Proof not loaded.
L2428
Proof:
Proof not loaded.
End of Section PigeonHole
L2440
Theorem. (Union_ordsucc_eq)
∀n, nat_p n (ordsucc n) = n
Proof:
Proof not loaded.
L2463
Theorem. (cases_1)
∀i1, ∀p : setprop, p 0p i
Proof:
Proof not loaded.
L2472
Theorem. (cases_2)
∀i2, ∀p : setprop, p 0p 1p i
Proof:
Proof not loaded.
L2481
Theorem. (neq_0_1)
Proof:
Proof not loaded.
L2485
Theorem. (neq_1_0)
Proof:
Proof not loaded.
L2489
Theorem. (neq_0_2)
Proof:
Proof not loaded.
L2493
Theorem. (neq_2_0)
Proof:
Proof not loaded.
L2497
Definition. We define ordinal to be λalpha : setTransSet alpha ∀betaalpha, TransSet beta of type setprop.
L2499
Theorem. (ordinal_TransSet)
∀alpha : set, ordinal alphaTransSet alpha
Proof:
Proof not loaded.
L2503
Proof:
Proof not loaded.
L2516
Theorem. (ordinal_Hered)
∀alpha : set, ordinal alpha∀betaalpha, ordinal beta
Proof:
Proof not loaded.
L2536
Theorem. (TransSet_ordsucc)
∀X : set, TransSet XTransSet (ordsucc X)
Proof:
Proof not loaded.
L2557
Theorem. (ordinal_ordsucc)
∀alpha : set, ordinal alphaordinal (ordsucc alpha)
Proof:
Proof not loaded.
L2577
Theorem. (nat_p_ordinal)
∀n : set, nat_p nordinal n
Proof:
Proof not loaded.
L2588
Theorem. (ordinal_1)
Proof:
Proof not loaded.
L2592
Theorem. (ordinal_2)
Proof:
Proof not loaded.
L2596
Theorem. (TransSet_ordsucc_In_Subq)
∀X : set, TransSet X∀xX, ordsucc x X
Proof:
Proof not loaded.
L2613
Theorem. (ordinal_ordsucc_In_Subq)
∀alpha, ordinal alpha∀betaalpha, ordsucc beta alpha
Proof:
Proof not loaded.
L2619
Theorem. (ordinal_trichotomy_or)
∀alpha beta : set, ordinal alphaordinal betaalpha beta alpha = beta beta alpha
Proof:
Proof not loaded.
L2687
Theorem. (ordinal_trichotomy_or_impred)
∀alpha beta : set, ordinal alphaordinal beta∀p : prop, (alpha betap)(alpha = betap)(beta alphap)p
Proof:
Proof not loaded.
L2692
Theorem. (ordinal_In_Or_Subq)
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Proof:
Proof not loaded.
L2709
Theorem. (ordinal_linear)
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Proof:
Proof not loaded.
L2722
Theorem. (ordinal_ordsucc_In_eq)
∀alpha beta, ordinal alphabeta alphaordsucc beta alpha alpha = ordsucc beta
Proof:
Proof not loaded.
L2739
Theorem. (ordinal_lim_or_succ)
∀alpha, ordinal alpha(∀betaalpha, ordsucc beta alpha) (∃betaalpha, alpha = ordsucc beta)
Proof:
Proof not loaded.
L2754
Theorem. (ordinal_ordsucc_In)
∀alpha, ordinal alpha∀betaalpha, ordsucc beta ordsucc alpha
Proof:
Proof not loaded.
L2769
Theorem. (ordinal_famunion)
∀X, ∀F : setset, (∀xX, ordinal (F x))ordinal (xXF x)
Proof:
Proof not loaded.
L2800
Theorem. (ordinal_binintersect)
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Proof:
Proof not loaded.
L2814
Theorem. (ordinal_binunion)
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Proof:
Proof not loaded.
L2829
Theorem. (ordinal_ind)
∀p : setprop, (∀alpha, ordinal alpha(∀betaalpha, p beta)p alpha)∀alpha, ordinal alphap alpha
Proof:
Proof not loaded.
L2849
Theorem. (least_ordinal_ex)
∀p : setprop, (∃alpha, ordinal alpha p alpha)∃alpha, ordinal alpha p alpha ∀betaalpha, ¬ p beta
Proof:
Proof not loaded.
L2871
Theorem. (equip_Sing_1)
∀x, equip {x} 1
Proof:
Proof not loaded.
L2890
Theorem. (TransSet_In_ordsucc_Subq)
∀x y, TransSet yx ordsucc yx y
Proof:
Proof not loaded.
L2896
Theorem. (exandE_i)
∀P Q : setprop, (∃x, P x Q x)∀r : prop, (∀x, P xQ xr)r
Proof:
Proof not loaded.
L2901
Theorem. (exandE_ii)
∀P Q : (setset)prop, (∃x : setset, P x Q x)∀p : prop, (∀x : setset, P xQ xp)p
Proof:
Proof not loaded.
L2908
Theorem. (exandE_iii)
∀P Q : (setsetset)prop, (∃x : setsetset, P x Q x)∀p : prop, (∀x : setsetset, P xQ xp)p
Proof:
Proof not loaded.
L2915
Theorem. (exandE_iiii)
∀P Q : (setsetsetset)prop, (∃x : setsetsetset, P x Q x)∀p : prop, (∀x : setsetsetset, P xQ xp)p
Proof:
Proof not loaded.
Beginning of Section Descr_ii
L2924
Variable P : (setset)prop
L2926
Definition. We define Descr_ii to be λx : setEps_i (λy ⇒ ∀h : setset, P hh x = y) of type setset.
L2927
Hypothesis Pex : ∃f : setset, P f
L2928
Hypothesis Puniq : ∀f g : setset, P fP gf = g
L2929
Theorem. (Descr_ii_prop)
Proof:
Proof not loaded.
End of Section Descr_ii
Beginning of Section Descr_iii
L2949
Variable P : (setsetset)prop
L2951
Definition. We define Descr_iii to be λx y : setEps_i (λz ⇒ ∀h : setsetset, P hh x y = z) of type setsetset.
L2952
Hypothesis Pex : ∃f : setsetset, P f
L2953
Hypothesis Puniq : ∀f g : setsetset, P fP gf = g
L2954
Proof:
Proof not loaded.
End of Section Descr_iii
Beginning of Section Descr_Vo1
L2976
Variable P : Vo 1prop
L2978
Definition. We define Descr_Vo1 to be λx : set∀h : setprop, P hh x of type Vo 1.
L2979
Hypothesis Pex : ∃f : Vo 1, P f
L2980
Hypothesis Puniq : ∀f g : Vo 1, P fP gf = g
L2981
Proof:
Proof not loaded.
End of Section Descr_Vo1
Beginning of Section If_ii
L3000
Variable p : prop
L3001
Variable f g : setset
L3003
Definition. We define If_ii to be λx ⇒ if p then f x else g x of type setset.
L3004
Theorem. (If_ii_1)
pIf_ii = f
Proof:
Proof not loaded.
L3011
Theorem. (If_ii_0)
¬ pIf_ii = g
Proof:
Proof not loaded.
End of Section If_ii
Beginning of Section If_iii
L3021
Variable p : prop
L3022
Variable f g : setsetset
L3024
Definition. We define If_iii to be λx y ⇒ if p then f x y else g x y of type setsetset.
L3025
Theorem. (If_iii_1)
pIf_iii = f
Proof:
Proof not loaded.
L3035
Theorem. (If_iii_0)
¬ pIf_iii = g
Proof:
Proof not loaded.
End of Section If_iii
Beginning of Section EpsilonRec_i
L3048
Variable F : set(setset)set
L3049
Definition. We define In_rec_i_G to be λX Y ⇒ ∀R : setsetprop, (∀X : set, ∀f : setset, (∀xX, R x (f x))R X (F X f))R X Y of type setsetprop.
L3055
Definition. We define In_rec_i to be λX ⇒ Eps_i (In_rec_i_G X) of type setset.
L3056
Theorem. (In_rec_i_G_c)
∀X : set, ∀f : setset, (∀xX, In_rec_i_G x (f x))In_rec_i_G X (F X f)
Proof:
Proof not loaded.
L3072
Theorem. (In_rec_i_G_inv)
∀X : set, ∀Y : set, In_rec_i_G X Y∃f : setset, (∀xX, In_rec_i_G x (f x)) Y = F X f
Proof:
Proof not loaded.
L3095
Hypothesis Fr : ∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
L3097
Theorem. (In_rec_i_G_f)
∀X : set, ∀Y Z : set, In_rec_i_G X YIn_rec_i_G X ZY = Z
Proof:
Proof not loaded.
L3128
Theorem. (In_rec_i_G_In_rec_i)
∀X : set, In_rec_i_G X (In_rec_i X)
Proof:
Proof not loaded.
L3139
Theorem. (In_rec_i_G_In_rec_i_d)
∀X : set, In_rec_i_G X (F X In_rec_i)
Proof:
Proof not loaded.
L3147
Theorem. (In_rec_i_eq)
∀X : set, In_rec_i X = F X In_rec_i
Proof:
Proof not loaded.
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
L3154
Variable F : set(set(setset))(setset)
L3155
Definition. We define In_rec_G_ii to be λX Y ⇒ ∀R : set(setset)prop, (∀X : set, ∀f : set(setset), (∀xX, R x (f x))R X (F X f))R X Y of type set(setset)prop.
L3161
Definition. We define In_rec_ii to be λX ⇒ Descr_ii (In_rec_G_ii X) of type set(setset).
L3162
Theorem. (In_rec_G_ii_c)
∀X : set, ∀f : set(setset), (∀xX, In_rec_G_ii x (f x))In_rec_G_ii X (F X f)
Proof:
Proof not loaded.
L3178
Theorem. (In_rec_G_ii_inv)
∀X : set, ∀Y : (setset), In_rec_G_ii X Y∃f : set(setset), (∀xX, In_rec_G_ii x (f x)) Y = F X f
Proof:
Proof not loaded.
L3201
Hypothesis Fr : ∀X : set, ∀g h : set(setset), (∀xX, g x = h x)F X g = F X h
L3203
Theorem. (In_rec_G_ii_f)
∀X : set, ∀Y Z : (setset), In_rec_G_ii X YIn_rec_G_ii X ZY = Z
Proof:
Proof not loaded.
L3234
Theorem. (In_rec_G_ii_In_rec_ii)
∀X : set, In_rec_G_ii X (In_rec_ii X)
Proof:
Proof not loaded.
L3247
Theorem. (In_rec_G_ii_In_rec_ii_d)
∀X : set, In_rec_G_ii X (F X In_rec_ii)
Proof:
Proof not loaded.
L3255
Theorem. (In_rec_ii_eq)
∀X : set, In_rec_ii X = F X In_rec_ii
Proof:
Proof not loaded.
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
L3262
Variable F : set(set(setsetset))(setsetset)
L3263
Definition. We define In_rec_G_iii to be λX Y ⇒ ∀R : set(setsetset)prop, (∀X : set, ∀f : set(setsetset), (∀xX, R x (f x))R X (F X f))R X Y of type set(setsetset)prop.
L3269
Definition. We define In_rec_iii to be λX ⇒ Descr_iii (In_rec_G_iii X) of type set(setsetset).
L3270
Theorem. (In_rec_G_iii_c)
∀X : set, ∀f : set(setsetset), (∀xX, In_rec_G_iii x (f x))In_rec_G_iii X (F X f)
Proof:
Proof not loaded.
L3286
Theorem. (In_rec_G_iii_inv)
∀X : set, ∀Y : (setsetset), In_rec_G_iii X Y∃f : set(setsetset), (∀xX, In_rec_G_iii x (f x)) Y = F X f
Proof:
Proof not loaded.
L3309
Hypothesis Fr : ∀X : set, ∀g h : set(setsetset), (∀xX, g x = h x)F X g = F X h
L3311
Theorem. (In_rec_G_iii_f)
∀X : set, ∀Y Z : (setsetset), In_rec_G_iii X YIn_rec_G_iii X ZY = Z
Proof:
Proof not loaded.
L3342
Theorem. (In_rec_G_iii_In_rec_iii)
∀X : set, In_rec_G_iii X (In_rec_iii X)
Proof:
Proof not loaded.
L3355
Theorem. (In_rec_G_iii_In_rec_iii_d)
∀X : set, In_rec_G_iii X (F X In_rec_iii)
Proof:
Proof not loaded.
L3363
Theorem. (In_rec_iii_eq)
∀X : set, In_rec_iii X = F X In_rec_iii
Proof:
Proof not loaded.
End of Section EpsilonRec_iii
Beginning of Section NatRec
L3370
Variable z : set
L3371
Variable f : setsetset
L3372
Let F : set(setset)setλn g ⇒ if n n then f ( n) (g ( n)) else z
L3373
Definition. We define nat_primrec to be In_rec_i F of type setset.
L3374
Theorem. (nat_primrec_r)
∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
Proof:
Proof not loaded.
L3394
Proof:
Proof not loaded.
L3402
Theorem. (nat_primrec_S)
∀n : set, nat_p nnat_primrec (ordsucc n) = f n (nat_primrec n)
Proof:
Proof not loaded.
End of Section NatRec
Beginning of Section NatAdd
L3418
Definition. We define add_nat to be λn m : setnat_primrec n (λ_ r ⇒ ordsucc r) m of type setsetset.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
L3421
Theorem. (add_nat_0R)
∀n : set, n + 0 = n
Proof:
Proof not loaded.
L3426
Theorem. (add_nat_SR)
∀n m : set, nat_p mn + ordsucc m = ordsucc (n + m)
Proof:
Proof not loaded.
L3431
Theorem. (add_nat_p)
∀n : set, nat_p n∀m : set, nat_p mnat_p (n + m)
Proof:
Proof not loaded.
L3450
Theorem. (add_nat_1_1_2)
1 + 1 = 2
Proof:
Proof not loaded.
L3459
Theorem. (add_nat_asso)
∀n : set, nat_p n∀m : set, nat_p m∀k : set, nat_p k(n + m) + k = n + (m + k)
Proof:
Proof not loaded.
L3481
Theorem. (add_nat_0L)
∀m : set, nat_p m0 + m = m
Proof:
Proof not loaded.
L3495
Theorem. (add_nat_SL)
∀n : set, nat_p n∀m : set, nat_p mordsucc n + m = ordsucc (n + m)
Proof:
Proof not loaded.
L3514
Theorem. (add_nat_com)
∀n : set, nat_p n∀m : set, nat_p mn + m = m + n
Proof:
Proof not loaded.
L3532
Theorem. (add_nat_In_R)
∀m, nat_p m∀km, ∀n, nat_p nk + n m + n
Proof:
Proof not loaded.
L3550
Theorem. (add_nat_In_L)
∀n, nat_p n∀m, nat_p m∀km, n + k n + m
Proof:
Proof not loaded.
L3558
Theorem. (add_nat_Subq_R)
∀k, nat_p k∀m, nat_p mk m∀n, nat_p nk + n m + n
Proof:
Proof not loaded.
L3580
Theorem. (add_nat_Subq_L)
∀n, nat_p n∀k, nat_p k∀m, nat_p mk mn + k n + m
Proof:
Proof not loaded.
L3590
Theorem. (add_nat_Subq_R')
∀m, nat_p m∀n, nat_p nm m + n
Proof:
Proof not loaded.
L3604
Theorem. (nat_Subq_add_ex)
∀n, nat_p n∀m, nat_p mn m∃k, nat_p k m = k + n
Proof:
Proof not loaded.
L3642
Theorem. (add_nat_cancel_R)
∀k, nat_p k∀m, nat_p m∀n, nat_p nk + n = m + nk = m
Proof:
Proof not loaded.
End of Section NatAdd
Beginning of Section NatMul
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
L3669
Definition. We define mul_nat to be λn m : setnat_primrec 0 (λ_ r ⇒ n + r) m of type setsetset.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L3672
Theorem. (mul_nat_0R)
∀n : set, n * 0 = 0
Proof:
Proof not loaded.
L3677
Theorem. (mul_nat_SR)
∀n m, nat_p mn * ordsucc m = n + n * m
Proof:
Proof not loaded.
L3682
Theorem. (mul_nat_1R)
∀n, n * 1 = n
Proof:
Proof not loaded.
L3691
Theorem. (mul_nat_p)
∀n : set, nat_p n∀m : set, nat_p mnat_p (n * m)
Proof:
Proof not loaded.
L3708
Theorem. (mul_nat_0L)
∀m : set, nat_p m0 * m = 0
Proof:
Proof not loaded.
L3723
Theorem. (mul_nat_SL)
∀n : set, nat_p n∀m : set, nat_p mordsucc n * m = n * m + m
Proof:
Proof not loaded.
L3755
Theorem. (mul_nat_com)
∀n : set, nat_p n∀m : set, nat_p mn * m = m * n
Proof:
Proof not loaded.
L3775
Theorem. (mul_add_nat_distrL)
∀n : set, nat_p n∀m : set, nat_p m∀k : set, nat_p kn * (m + k) = n * m + n * k
Proof:
Proof not loaded.
L3806
Theorem. (mul_nat_asso)
∀n : set, nat_p n∀m : set, nat_p m∀k : set, nat_p k(n * m) * k = n * (m * k)
Proof:
Proof not loaded.
L3835
Theorem. (mul_nat_Subq_R)
∀m n, nat_p mnat_p nm n∀k, nat_p km * k n * k
Proof:
Proof not loaded.
L3857
Theorem. (mul_nat_Subq_L)
∀m n, nat_p mnat_p nm n∀k, nat_p kk * m k * n
Proof:
Proof not loaded.
L3865
Theorem. (mul_nat_0_or_Subq)
∀m, nat_p m∀n, nat_p nn = 0 m m * n
Proof:
Proof not loaded.
L3880
Theorem. (mul_nat_0_inv)
∀m, nat_p m∀n, nat_p nm * n = 0m = 0 n = 0
Proof:
Proof not loaded.
L3901
Theorem. (mul_nat_0m_1n_In)
∀m, nat_p m∀n, nat_p n0 m1 nm m * n
Proof:
Proof not loaded.
L3937
Theorem. (nat_le1_cases)
∀m, nat_p mm 1m = 0 m = 1
Proof:
Proof not loaded.
L3954
Definition. We define Pi_nat to be λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i) n of type (setset)setset.
L3957
Theorem. (Pi_nat_0)
∀f : setset, Pi_nat f 0 = 1
Proof:
Proof not loaded.
L3962
Theorem. (Pi_nat_S)
∀f : setset, ∀n, nat_p nPi_nat f (ordsucc n) = Pi_nat f n * f n
Proof:
Proof not loaded.
L3968
Theorem. (Pi_nat_p)
∀f : setset, ∀n, nat_p n(∀in, nat_p (f i))nat_p (Pi_nat f n)
Proof:
Proof not loaded.
L3993
Theorem. (Pi_nat_0_inv)
∀f : setset, ∀n, nat_p n(∀in, nat_p (f i))Pi_nat f n = 0(∃in, f i = 0)
Proof:
Proof not loaded.
L4036
Definition. We define exp_nat to be λn m : setnat_primrec 1 (λ_ r ⇒ n * r) m of type setsetset.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_nat.
L4040
Theorem. (exp_nat_0)
∀n, n ^ 0 = 1
Proof:
Proof not loaded.
L4046
Theorem. (exp_nat_S)
∀n m, nat_p mn ^ (ordsucc m) = n * n ^ m
Proof:
Proof not loaded.
L4052
Theorem. (exp_nat_p)
∀n, nat_p n∀m, nat_p mnat_p (n ^ m)
Proof:
Proof not loaded.
L4063
Theorem. (exp_nat_1)
∀n, n ^ 1 = n
Proof:
Proof not loaded.
End of Section NatMul
Beginning of Section form100_52
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_nat.
L4080
Theorem. (Subq_Sing0_1)
Proof:
Proof not loaded.
L4084
Theorem. (Subq_1_Sing0)
Proof:
Proof not loaded.
L4098
Theorem. (eq_1_Sing0)
Proof:
Proof not loaded.
L4102
Proof:
Proof not loaded.
L4123
Theorem. (equip_finite_Power)
∀n, nat_p n∀X, equip X nequip (𝒫 X) (2 ^ n)
Proof:
Proof not loaded.
End of Section form100_52
L4496
Theorem. (ZF_closed_E)
∀U, ZF_closed U∀p : prop, (Union_closed UPower_closed URepl_closed Up)p
Proof:
Proof not loaded.
L4505
Theorem. (ZF_Union_closed)
∀U, ZF_closed U∀XU, X U
Proof:
Proof not loaded.
L4510
Theorem. (ZF_Power_closed)
∀U, ZF_closed U∀XU, 𝒫 X U
Proof:
Proof not loaded.
L4515
Theorem. (ZF_Repl_closed)
∀U, ZF_closed U∀XU, ∀F : setset, (∀xX, F x U){F x|xX} U
Proof:
Proof not loaded.
L4520
Theorem. (ZF_UPair_closed)
∀U, ZF_closed U∀x yU, {x,y} U
Proof:
Proof not loaded.
L4604
Theorem. (ZF_Sing_closed)
∀U, ZF_closed U∀xU, {x} U
Proof:
Proof not loaded.
L4609
Theorem. (ZF_binunion_closed)
∀U, ZF_closed U∀X YU, (X Y) U
Proof:
Proof not loaded.
L4614
Theorem. (ZF_ordsucc_closed)
∀U, ZF_closed U∀xU, ordsucc x U
Proof:
Proof not loaded.
L4619
Theorem. (nat_p_UnivOf_Empty)
∀n : set, nat_p nn UnivOf Empty
Proof:
Proof not loaded.
L4633
Definition. We define ω to be {nUnivOf Empty|nat_p n} of type set.
L4634
Theorem. (omega_nat_p)
∀nω, nat_p n
Proof:
Proof not loaded.
L4638
Theorem. (nat_p_omega)
∀n : set, nat_p nn ω
Proof:
Proof not loaded.
L4647
Theorem. (omega_ordsucc)
Proof:
Proof not loaded.
L4655
Theorem. (form100_22_v2)
∀f : setset, ¬ inj (𝒫 ω) ω f
Proof:
Proof not loaded.
L4659
Theorem. (form100_22_v3)
∀g : setset, ¬ surj ω (𝒫 ω) g
Proof:
Proof not loaded.
L4684
Proof:
Proof not loaded.
L4693
Proof:
Proof not loaded.
L4706
Proof:
Proof not loaded.
L4720
Proof:
Proof not loaded.
L4724
Definition. We define finite to be λX ⇒ ∃nω, equip X n of type setprop.
L4726
Theorem. (nat_finite)
∀n, nat_p nfinite n
Proof:
Proof not loaded.
L4734
Theorem. (finite_ind)
∀p : setprop, p Empty(∀X y, finite Xy Xp Xp (X {y}))∀X, finite Xp X
Proof:
Proof not loaded.
L4826
Theorem. (finite_Empty)
Proof:
Proof not loaded.
L4833
Theorem. (Sing_finite)
∀x, finite {x}
Proof:
Proof not loaded.
L4841
Theorem. (adjoin_finite)
∀X y, finite Xfinite (X {y})
Proof:
Proof not loaded.
L4924
Theorem. (binunion_finite)
∀X, finite X∀Y, finite Yfinite (X Y)
Proof:
Proof not loaded.
L4939
Theorem. (famunion_nat_finite)
∀X : setset, ∀n, nat_p n(∀in, finite (X i))finite (inX i)
Proof:
Proof not loaded.
L4978
Theorem. (Subq_finite)
∀X, finite X∀Y, Y Xfinite Y
Proof:
Proof not loaded.
L5031
Definition. We define infinite to be λA ⇒ ¬ finite A of type setprop.
Beginning of Section InfinitePrimes
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L5038
Definition. We define divides_nat to be λm n ⇒ m ω n ω ∃kω, m * k = n of type setsetprop.
L5041
Theorem. (divides_nat_ref)
∀n, nat_p ndivides_nat n n
Proof:
Proof not loaded.
L5055
Theorem. (divides_nat_tra)
∀k m n, divides_nat k mdivides_nat m ndivides_nat k n
Proof:
Proof not loaded.
L5093
Definition. We define prime_nat to be λn ⇒ n ω 1 n ∀kω, divides_nat k nk = 1 k = n of type setprop.
L5096
Theorem. (divides_nat_mulR)
∀m nω, divides_nat m (m * n)
Proof:
Proof not loaded.
L5109
Theorem. (divides_nat_mulL)
∀m nω, divides_nat n (m * n)
Proof:
Proof not loaded.
L5116
Theorem. (Pi_nat_divides)
∀f : setset, ∀n, nat_p n(∀in, nat_p (f i))(∀in, divides_nat (f i) (Pi_nat f n))
Proof:
Proof not loaded.
L5150
Definition. We define composite_nat to be λn ⇒ n ω ∃k mω, 1 k 1 m k * m = n of type setprop.
L5153
Proof:
Proof not loaded.
L5235
Theorem. (prime_nat_divisor_ex)
∀n, nat_p n1 n∃p, prime_nat p divides_nat p n
Proof:
Proof not loaded.
L5277
Theorem. (nat_1In_not_divides_ordsucc)
∀m n, 1 mdivides_nat m n¬ divides_nat m (ordsucc n)
Proof:
Proof not loaded.
L5344
Definition. We define primes to be {nω|prime_nat n} of type set.
L5346
Proof:
Proof not loaded.
End of Section InfinitePrimes
Beginning of Section InfiniteRamsey
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
L5477
Theorem. (atleastp_omega_infinite)
∀X, atleastp ω Xinfinite X
Proof:
Proof not loaded.
L5503
Theorem. (infinite_remove1)
∀X, infinite X∀y, infinite (X {y})
Proof:
Proof not loaded.
L5536
Theorem. (infinite_Finite_Subq_ex)
∀X, infinite X∀n, nat_p n∃YX, equip Y n
Proof:
Proof not loaded.
L5675
Theorem. (infiniteRamsey_lem)
∀X, ∀f g f' : setset, infinite X(∀ZX, infinite Zf Z Z infinite (f Z))(∀ZX, infinite Zg Z Z g Z f Z)f' 0 = f X(∀m, nat_p mf' (ordsucc m) = f (f' m))(∀m, nat_p mf' m X infinite (f' m)) (∀m m'ω, m m'f' m' f' m) (∀m m'ω, g (f' m) = g (f' m')m = m')
Proof:
Proof not loaded.
L5801
Theorem. (infiniteRamsey)
∀c, nat_p c∀n, nat_p n∀X, infinite X∀C : setset, (∀YX, equip Y nC Y c)∃HX, ∃ic, infinite H ∀YH, equip Y nC Y = i
Proof:
Proof not loaded.
End of Section InfiniteRamsey
L6649
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} {f x|xX}) of type setset.
L6652
Theorem. (Inj1_eq)
∀X : set, Inj1 X = {0} {Inj1 x|xX}
Proof:
Proof not loaded.
(*** Injection of set into itself that will correspond to x |-> (1,x) after pairing is defined. ***)
L6669
Theorem. (Inj1I1)
∀X : set, 0 Inj1 X
Proof:
Proof not loaded.
L6677
Theorem. (Inj1I2)
∀X x : set, x XInj1 x Inj1 X
Proof:
Proof not loaded.
L6686
Theorem. (Inj1E)
∀X y : set, y Inj1 Xy = 0 ∃xX, y = Inj1 x
Proof:
Proof not loaded.
L6701
Theorem. (Inj1NE1)
∀x : set, Inj1 x 0
Proof:
Proof not loaded.
L6711
Theorem. (Inj1NE2)
∀x : set, Inj1 x {0}
Proof:
Proof not loaded.
L6717
Definition. We define Inj0 to be λX ⇒ {Inj1 x|xX} of type setset.
L6720
Theorem. (Inj0I)
∀X x : set, x XInj1 x Inj0 X
Proof:
Proof not loaded.
(*** Injection of set into itself that will correspond to x |-> (0,x) after pairing is defined. ***)
L6724
Theorem. (Inj0E)
∀X y : set, y Inj0 X∃x : set, x X y = Inj1 x
Proof:
Proof not loaded.
L6728
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|xX {0}}) of type setset.
L6731
Theorem. (Unj_eq)
∀X : set, Unj X = {Unj x|xX {0}}
Proof:
Proof not loaded.
(*** Unj : Left inverse of Inj1 and Inj0 ***)
L6748
Theorem. (Unj_Inj1_eq)
∀X : set, Unj (Inj1 X) = X
Proof:
Proof not loaded.
L6800
Theorem. (Inj1_inj)
∀X Y : set, Inj1 X = Inj1 YX = Y
Proof:
Proof not loaded.
L6810
Theorem. (Unj_Inj0_eq)
∀X : set, Unj (Inj0 X) = X
Proof:
Proof not loaded.
L6858
Theorem. (Inj0_inj)
∀X Y : set, Inj0 X = Inj0 YX = Y
Proof:
Proof not loaded.
L6868
Theorem. (Inj0_0)
Proof:
Proof not loaded.
L6872
Theorem. (Inj0_Inj1_neq)
∀X Y : set, Inj0 X Inj1 Y
Proof:
Proof not loaded.
L6887
Definition. We define setsum to be λX Y ⇒ {Inj0 x|xX} {Inj1 y|yY} of type setsetset.
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
(*** setsum ***)
L6892
Theorem. (Inj0_setsum)
∀X Y x : set, x XInj0 x X + Y
Proof:
Proof not loaded.
L6902
Theorem. (Inj1_setsum)
∀X Y y : set, y YInj1 y X + Y
Proof:
Proof not loaded.
L6912
Theorem. (setsum_Inj_inv)
∀X Y z : set, z X + Y(∃xX, z = Inj0 x) (∃yY, z = Inj1 y)
Proof:
Proof not loaded.
L6924
Theorem. (Inj0_setsum_0L)
∀X : set, 0 + X = Inj0 X
Proof:
Proof not loaded.
L6957
Theorem. (Inj1_setsum_1L)
∀X : set, 1 + X = Inj1 X
Proof:
Proof not loaded.
Beginning of Section pair_setsum
L7010
Let pair ≝ setsum
L7011
Definition. We define proj0 to be λZ ⇒ {Unj z|zZ, ∃x : set, Inj0 x = z} of type setset.
L7012
Definition. We define proj1 to be λZ ⇒ {Unj z|zZ, ∃y : set, Inj1 y = z} of type setset.
L7013
Theorem. (Inj0_pair_0_eq)
Inj0 = pair 0
Proof:
Proof not loaded.
L7021
Theorem. (Inj1_pair_1_eq)
Inj1 = pair 1
Proof:
Proof not loaded.
L7029
Theorem. (pairI0)
∀X Y x, x Xpair 0 x pair X Y
Proof:
Proof not loaded.
L7034
Theorem. (pairI1)
∀X Y y, y Ypair 1 y pair X Y
Proof:
Proof not loaded.
L7039
Theorem. (pairE)
∀X Y z, z pair X Y(∃xX, z = pair 0 x) (∃yY, z = pair 1 y)
Proof:
Proof not loaded.
L7045
Theorem. (pairE0)
∀X Y x, pair 0 x pair X Yx X
Proof:
Proof not loaded.
L7071
Theorem. (pairE1)
∀X Y y, pair 1 y pair X Yy Y
Proof:
Proof not loaded.
L7099
Theorem. (proj0I)
∀w u : set, pair 0 u wu proj0 w
Proof:
Proof not loaded.
L7114
Theorem. (proj0E)
∀w u : set, u proj0 wpair 0 u w
Proof:
Proof not loaded.
L7138
Theorem. (proj1I)
∀w u : set, pair 1 u wu proj1 w
Proof:
Proof not loaded.
L7153
Theorem. (proj1E)
∀w u : set, u proj1 wpair 1 u w
Proof:
Proof not loaded.
L7177
Theorem. (proj0_pair_eq)
∀X Y : set, proj0 (pair X Y) = X
Proof:
Proof not loaded.
L7197
Theorem. (proj1_pair_eq)
∀X Y : set, proj1 (pair X Y) = Y
Proof:
Proof not loaded.
L7219
Definition. We define Sigma to be λX Y ⇒ xX{pair x y|yY x} of type set(setset)set.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
(*** Sigma X Y = {(x,y) | x in X, y in Y x} ***)
L7225
Theorem. (Sigma_eta_proj0_proj1)
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (proj0 z) (proj1 z) = z proj0 z X proj1 z Y (proj0 z)
Proof:
Proof not loaded.
L7253
Theorem. (proj0_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj0 z X
Proof:
Proof not loaded.
L7261
Theorem. (proj1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj1 z Y (proj0 z)
Proof:
Proof not loaded.
L7269
Theorem. (pair_Sigma)
∀X : set, ∀Y : setset, ∀xX, ∀yY x, pair x y xX, Y x
Proof:
Proof not loaded.
L7284
Theorem. (pair_Sigma_E1)
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)y Y x
Proof:
Proof not loaded.
L7295
Theorem. (Sigma_E)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)∃xX, ∃yY x, z = pair x y
Proof:
Proof not loaded.
L7313
Definition. We define setprod to be λX Y : setxX, Y of type setsetset.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
L7317
Let lam : set(setset)setSigma
L7319
Definition. We define ap to be λf x ⇒ {proj1 z|zf, ∃y : set, z = pair x y} of type setsetset.
(*** lam X F = {(x,y) | x :e X, y :e F x} = \/_{x :e X} {(x,y) | y :e (F x)} = Sigma X F ***)
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ xAB is notation for the set Sigma Ax : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
(*** ap f x = {proj1 z | z :e f, exists y, z = pair x y}} ***)
L7323
Theorem. (lamI)
∀X : set, ∀F : setset, ∀xX, ∀yF x, pair x y λxXF x
Proof:
Proof not loaded.
L7327
Theorem. (lamE)
∀X : set, ∀F : setset, ∀z : set, z (λxXF x)∃xX, ∃yF x, z = pair x y
Proof:
Proof not loaded.
L7331
Theorem. (apI)
∀f x y, pair x y fy f x
Proof:
Proof not loaded.
L7343
Theorem. (apE)
∀f x y, y f xpair x y f
Proof:
Proof not loaded.
L7371
Theorem. (beta)
∀X : set, ∀F : setset, ∀x : set, x X(λxXF x) x = F x
Proof:
Proof not loaded.
L7391
Theorem. (proj0_ap_0)
∀u, proj0 u = u 0
Proof:
Proof not loaded.
L7411
Theorem. (proj1_ap_1)
∀u, proj1 u = u 1
Proof:
Proof not loaded.
L7431
Theorem. (pair_ap_0)
∀x y : set, (pair x y) 0 = x
Proof:
Proof not loaded.
L7438
Theorem. (pair_ap_1)
∀x y : set, (pair x y) 1 = y
Proof:
Proof not loaded.
L7445
Theorem. (ap0_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 0) X
Proof:
Proof not loaded.
L7451
Theorem. (ap1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 1) (Y (z 0))
Proof:
Proof not loaded.
L7458
Definition. We define pair_p to be λu : setpair (u 0) (u 1) = u of type setprop.
L7461
Theorem. (pair_p_I)
∀x y, pair_p (pair x y)
Proof:
Proof not loaded.
L7469
Proof:
Proof not loaded.
L7487
Theorem. (tuple_pair)
∀x y : set, pair x y = (x,y)
Proof:
Proof not loaded.
L7562
Definition. We define Pi to be λX Y ⇒ {f𝒫 (xX, (Y x))|∀xX, f x Y x} of type set(setset)set.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
L7566
Theorem. (PiI)
∀X : set, ∀Y : setset, ∀f : set, (∀uf, pair_p u u 0 X)(∀xX, f x Y x)f xX, Y x
Proof:
Proof not loaded.
L7600
Theorem. (lam_Pi)
∀X : set, ∀Y : setset, ∀F : setset, (∀xX, F x Y x)(λxXF x) (xX, Y x)
Proof:
Proof not loaded.
L7639
Theorem. (ap_Pi)
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f (xX, Y x)x Xf x Y x
Proof:
Proof not loaded.
L7645
Definition. We define setexp to be λX Y : setyY, X of type setsetset.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
L7649
Theorem. (pair_tuple_fun)
pair = (λx y ⇒ (x,y))
Proof:
Proof not loaded.
Beginning of Section Tuples
L7658
Variable x0 x1 : set
L7659
Theorem. (tuple_2_0_eq)
(x0,x1) 0 = x0
Proof:
Proof not loaded.
L7664
Theorem. (tuple_2_1_eq)
(x0,x1) 1 = x1
Proof:
Proof not loaded.
End of Section Tuples
L7671
Theorem. (ReplEq_setprod_ext)
∀X Y, ∀F G : setsetset, (∀xX, ∀yY, F x y = G x y){F (w 0) (w 1)|wX Y} = {G (w 0) (w 1)|wX Y}
Proof:
Proof not loaded.
L7682
Theorem. (lamI2)
∀X, ∀F : setset, ∀xX, ∀yF x, (x,y) λxXF x
Proof:
Proof not loaded.
L7688
Theorem. (tuple_2_Sigma)
∀X : set, ∀Y : setset, ∀xX, ∀yY x, (x,y) xX, Y x
Proof:
Proof not loaded.
L7692
Theorem. (tuple_2_setprod)
∀X : set, ∀Y : set, ∀xX, ∀yY, (x,y) X Y
Proof:
Proof not loaded.
End of Section pair_setsum
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
L7707
Definition. We define DescrR_i_io_1 to be λR ⇒ Eps_i (λx ⇒ (∃y : setprop, R x y) (∀y z : setprop, R x yR x zy = z)) of type (set(setprop)prop)set.
L7709
Definition. We define DescrR_i_io_2 to be λR ⇒ Descr_Vo1 (λy ⇒ R (DescrR_i_io_1 R) y) of type (set(setprop)prop)setprop.
L7710
Theorem. (DescrR_i_io_12)
∀R : set(setprop)prop, (∃x, (∃y : setprop, R x y) (∀y z : setprop, R x yR x zy = z))R (DescrR_i_io_1 R) (DescrR_i_io_2 R)
Proof:
Proof not loaded.
L7720
Definition. We define PNoEq_ to be λalpha p q ⇒ ∀betaalpha, p beta q beta of type set(setprop)(setprop)prop.
(*** Conway describes this way of formalizing in ZF in an appendix to Part Zero of his book,
but rejects formalization in favor of "Mathematician's Liberation." ***)
L7726
Theorem. (PNoEq_ref_)
∀alpha, ∀p : setprop, PNoEq_ alpha p p
Proof:
Proof not loaded.
L7732
Theorem. (PNoEq_sym_)
∀alpha, ∀p q : setprop, PNoEq_ alpha p qPNoEq_ alpha q p
Proof:
Proof not loaded.
L7740
Theorem. (PNoEq_tra_)
∀alpha, ∀p q r : setprop, PNoEq_ alpha p qPNoEq_ alpha q rPNoEq_ alpha p r
Proof:
Proof not loaded.
L7749
Theorem. (PNoEq_antimon_)
∀p q : setprop, ∀alpha, ordinal alpha∀betaalpha, PNoEq_ alpha p qPNoEq_ beta p q
Proof:
Proof not loaded.
L7759
Definition. We define PNoLt_ to be λalpha p q ⇒ ∃betaalpha, PNoEq_ beta p q ¬ p beta q beta of type set(setprop)(setprop)prop.
L7762
Theorem. (PNoLt_E_)
∀alpha, ∀p q : setprop, PNoLt_ alpha p q∀R : prop, (∀beta, beta alphaPNoEq_ beta p q¬ p betaq betaR)R
Proof:
Proof not loaded.
L7773
Theorem. (PNoLt_irref_)
∀alpha, ∀p : setprop, ¬ PNoLt_ alpha p p
Proof:
Proof not loaded.
L7780
Theorem. (PNoLt_mon_)
∀p q : setprop, ∀alpha, ordinal alpha∀betaalpha, PNoLt_ beta p qPNoLt_ alpha p q
Proof:
Proof not loaded.
L7791
Theorem. (PNoLt_trichotomy_or_)
∀p q : setprop, ∀alpha, ordinal alphaPNoLt_ alpha p q PNoEq_ alpha p q PNoLt_ alpha q p
Proof:
Proof not loaded.
L7866
Definition. We define PNoLt to be λalpha p beta q ⇒ PNoLt_ (alpha beta) p q alpha beta PNoEq_ alpha p q q alpha beta alpha PNoEq_ beta p q ¬ p beta of type set(setprop)set(setprop)prop.
L7871
Theorem. (PNoLtI1)
∀alpha beta, ∀p q : setprop, PNoLt_ (alpha beta) p qPNoLt alpha p beta q
Proof:
Proof not loaded.
L7880
Theorem. (PNoLtI2)
∀alpha beta, ∀p q : setprop, alpha betaPNoEq_ alpha p qq alphaPNoLt alpha p beta q
Proof:
Proof not loaded.
L7892
Theorem. (PNoLtI3)
∀alpha beta, ∀p q : setprop, beta alphaPNoEq_ beta p q¬ p betaPNoLt alpha p beta q
Proof:
Proof not loaded.
L7904
Theorem. (PNoLtE)
∀alpha beta, ∀p q : setprop, PNoLt alpha p beta q∀R : prop, (PNoLt_ (alpha beta) p qR)(alpha betaPNoEq_ alpha p qq alphaR)(beta alphaPNoEq_ beta p q¬ p betaR)R
Proof:
Proof not loaded.
L7919
Theorem. (PNoLt_irref)
∀alpha, ∀p : setprop, ¬ PNoLt alpha p alpha p
Proof:
Proof not loaded.
L7930
Theorem. (PNoLt_trichotomy_or)
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta q alpha = beta PNoEq_ alpha p q PNoLt beta q alpha p
Proof:
Proof not loaded.
L7997
Theorem. (PNoLtEq_tra)
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoLt alpha p beta qPNoEq_ beta q rPNoLt alpha p beta r
Proof:
Proof not loaded.
L8051
Theorem. (PNoEqLt_tra)
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLt alpha q beta rPNoLt alpha p beta r
Proof:
Proof not loaded.
L8109
Theorem. (PNoLt_tra)
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
Proof:
Proof not loaded.
L8424
Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLt alpha p beta q alpha = beta PNoEq_ alpha p q of type set(setprop)set(setprop)prop.
L8427
Theorem. (PNoLeI1)
∀alpha beta, ∀p q : setprop, PNoLt alpha p beta qPNoLe alpha p beta q
Proof:
Proof not loaded.
L8435
Theorem. (PNoLeI2)
∀alpha, ∀p q : setprop, PNoEq_ alpha p qPNoLe alpha p alpha q
Proof:
Proof not loaded.
L8445
Theorem. (PNoLe_ref)
∀alpha, ∀p : setprop, PNoLe alpha p alpha p
Proof:
Proof not loaded.
L8451
Theorem. (PNoLe_antisym)
∀alpha beta, ordinal alphaordinal beta∀p q : setprop, PNoLe alpha p beta qPNoLe beta q alpha palpha = beta PNoEq_ alpha p q
Proof:
Proof not loaded.
L8497
Theorem. (PNoLtLe_tra)
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLe beta q gamma rPNoLt alpha p gamma r
Proof:
Proof not loaded.
L8514
Theorem. (PNoLeLt_tra)
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLe alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
Proof:
Proof not loaded.
L8533
Theorem. (PNoEqLe_tra)
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLe alpha q beta rPNoLe alpha p beta r
Proof:
Proof not loaded.
L8552
Theorem. (PNoLe_tra)
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLe alpha p beta qPNoLe beta q gamma rPNoLe alpha p gamma r
Proof:
Proof not loaded.
L8573
Definition. We define PNo_downc to be λL alpha p ⇒ ∃beta, ordinal beta ∃q : setprop, L beta q PNoLe alpha p beta q of type (set(setprop)prop)set(setprop)prop.
L8576
Definition. We define PNo_upc to be λR alpha p ⇒ ∃beta, ordinal beta ∃q : setprop, R beta q PNoLe beta q alpha p of type (set(setprop)prop)set(setprop)prop.
L8578
Theorem. (PNoLe_downc)
∀L : set(setprop)prop, ∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNo_downc L alpha pPNoLe beta q alpha pPNo_downc L beta q
Proof:
Proof not loaded.
L8598
Theorem. (PNo_downc_ref)
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, L alpha pPNo_downc L alpha p
Proof:
Proof not loaded.
L8609
Theorem. (PNo_upc_ref)
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, R alpha pPNo_upc R alpha p
Proof:
Proof not loaded.
L8620
Theorem. (PNoLe_upc)
∀R : set(setprop)prop, ∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNo_upc R alpha pPNoLe alpha p beta qPNo_upc R beta q
Proof:
Proof not loaded.
L8640
Definition. We define PNoLt_pwise to be λL R ⇒ ∀gamma, ordinal gamma∀p : setprop, L gamma p∀delta, ordinal delta∀q : setprop, R delta qPNoLt gamma p delta q of type (set(setprop)prop)(set(setprop)prop)prop.
L8643
Theorem. (PNoLt_pwise_downc_upc)
∀L R : set(setprop)prop, PNoLt_pwise L RPNoLt_pwise (PNo_downc L) (PNo_upc R)
Proof:
Proof not loaded.
L8684
Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ ∀betaalpha, ∀q : setprop, PNo_downc L beta qPNoLt beta q alpha p of type (set(setprop)prop)set(setprop)prop.
L8688
Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ ∀betaalpha, ∀q : setprop, PNo_upc R beta qPNoLt alpha p beta q of type (set(setprop)prop)set(setprop)prop.
L8691
Definition. We define PNo_rel_strict_imv to be λL R alpha p ⇒ PNo_rel_strict_upperbd L alpha p PNo_rel_strict_lowerbd R alpha p of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
L8693
Theorem. (PNoEq_rel_strict_upperbd)
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_upperbd L alpha pPNo_rel_strict_upperbd L alpha q
Proof:
Proof not loaded.
L8710
Theorem. (PNo_rel_strict_upperbd_antimon)
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, ∀betaalpha, PNo_rel_strict_upperbd L alpha pPNo_rel_strict_upperbd L beta p
Proof:
Proof not loaded.
L8751
Theorem. (PNoEq_rel_strict_lowerbd)
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R alpha q
Proof:
Proof not loaded.
L8768
Theorem. (PNo_rel_strict_lowerbd_antimon)
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, ∀betaalpha, PNo_rel_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R beta p
Proof:
Proof not loaded.
L8809
Theorem. (PNoEq_rel_strict_imv)
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R alpha q
Proof:
Proof not loaded.
L8819
Theorem. (PNo_rel_strict_imv_antimon)
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, ∀betaalpha, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R beta p
Proof:
Proof not loaded.
L8829
Definition. We define PNo_rel_strict_uniq_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R alpha p ∀q : setprop, PNo_rel_strict_imv L R alpha qPNoEq_ alpha p q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
L8832
Definition. We define PNo_rel_strict_split_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta alpha) PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta = alpha) of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
L8836
Theorem. (PNo_extend0_eq)
∀alpha, ∀p : setprop, PNoEq_ alpha p (λdelta ⇒ p delta delta alpha)
Proof:
Proof not loaded.
L8853
Theorem. (PNo_extend1_eq)
∀alpha, ∀p : setprop, PNoEq_ alpha p (λdelta ⇒ p delta delta = alpha)
Proof:
Proof not loaded.
L8870
Theorem. (PNo_rel_imv_ex)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alpha(∃p : setprop, PNo_rel_strict_uniq_imv L R alpha p) (∃taualpha, ∃p : setprop, PNo_rel_strict_split_imv L R tau p)
Proof:
Proof not loaded.
L9947
Definition. We define PNo_lenbdd to be λalpha L ⇒ ∀beta, ∀p : setprop, L beta pbeta alpha of type set(set(setprop)prop)prop.
L9950
Theorem. (PNo_lenbdd_strict_imv_extend0)
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta alpha)
Proof:
Proof not loaded.
L10087
Theorem. (PNo_lenbdd_strict_imv_extend1)
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta = alpha)
Proof:
Proof not loaded.
L10229
Theorem. (PNo_lenbdd_strict_imv_split)
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_split_imv L R alpha p
Proof:
Proof not loaded.
L10245
Theorem. (PNo_rel_imv_bdd_ex)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∃betaordsucc alpha, ∃p : setprop, PNo_rel_strict_split_imv L R beta p
Proof:
Proof not loaded.
L10279
Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinal beta∀q : setprop, L beta qPNoLt beta q alpha p of type (set(setprop)prop)set(setprop)prop.
L10283
Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinal beta∀q : setprop, R beta qPNoLt alpha p beta q of type (set(setprop)prop)set(setprop)prop.
L10286
Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbd L alpha p PNo_strict_lowerbd R alpha p of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
L10288
Theorem. (PNoEq_strict_upperbd)
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_upperbd L alpha pPNo_strict_upperbd L alpha q
Proof:
Proof not loaded.
L10303
Theorem. (PNoEq_strict_lowerbd)
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_lowerbd R alpha pPNo_strict_lowerbd R alpha q
Proof:
Proof not loaded.
L10318
Theorem. (PNoEq_strict_imv)
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_imv L R alpha pPNo_strict_imv L R alpha q
Proof:
Proof not loaded.
L10328
Theorem. (PNo_strict_upperbd_imp_rel_strict_upperbd)
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀betaordsucc alpha, ∀p : setprop, PNo_strict_upperbd L alpha pPNo_rel_strict_upperbd L beta p
Proof:
Proof not loaded.
L10409
Theorem. (PNo_strict_lowerbd_imp_rel_strict_lowerbd)
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀betaordsucc alpha, ∀p : setprop, PNo_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R beta p
Proof:
Proof not loaded.
L10488
Theorem. (PNo_strict_imv_imp_rel_strict_imv)
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀betaordsucc alpha, ∀p : setprop, PNo_strict_imv L R alpha pPNo_rel_strict_imv L R beta p
Proof:
Proof not loaded.
L10507
Theorem. (PNo_rel_split_imv_imp_strict_imv)
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, PNo_rel_strict_split_imv L R alpha pPNo_strict_imv L R alpha p
Proof:
Proof not loaded.
L10753
Theorem. (PNo_lenbdd_strict_imv_ex)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∃betaordsucc alpha, ∃p : setprop, PNo_strict_imv L R beta p
Proof:
Proof not loaded.
L10779
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal beta PNo_strict_imv L R beta p ∀gammabeta, ∀q : setprop, ¬ PNo_strict_imv L R gamma q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
L10785
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p ∀x, x beta¬ p x of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
L10787
Theorem. (PNo_strict_imv_pred_eq)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alpha∀p q : setprop, PNo_least_rep L R alpha pPNo_strict_imv L R alpha q∀betaalpha, p beta q beta
Proof:
Proof not loaded.
L10883
Theorem. (PNo_lenbdd_least_rep2_exuniq2)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∃beta, (∃p : setprop, PNo_least_rep2 L R beta p) (∀p q : setprop, PNo_least_rep2 L R beta pPNo_least_rep2 L R beta qp = q)
Proof:
Proof not loaded.
L10971
Definition. We define PNo_bd to be λL R ⇒ DescrR_i_io_1 (PNo_least_rep2 L R) of type (set(setprop)prop)(set(setprop)prop)set.
L10974
Definition. We define PNo_pred to be λL R ⇒ DescrR_i_io_2 (PNo_least_rep2 L R) of type (set(setprop)prop)(set(setprop)prop)setprop.
L10976
Theorem. (PNo_bd_pred_lem)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)
Proof:
Proof not loaded.
L10988
Theorem. (PNo_bd_pred)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_least_rep L R (PNo_bd L R) (PNo_pred L R)
Proof:
Proof not loaded.
L10999
Theorem. (PNo_bd_In)
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_bd L R ordsucc alpha
Proof:
Proof not loaded.
Beginning of Section TaggedSets
L11033
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
L11035
Proof:
Proof not loaded.
L11043
Proof:
Proof not loaded.
L11047
Theorem. (tagged_not_ordinal)
∀y, ¬ ordinal (y ')
Proof:
Proof not loaded.
L11059
Theorem. (tagged_notin_ordinal)
∀alpha y, ordinal alpha(y ') alpha
Proof:
Proof not loaded.
L11066
Theorem. (tagged_eqE_Subq)
∀alpha beta, ordinal alphaalpha ' = beta 'alpha beta
Proof:
Proof not loaded.
L11087
Theorem. (tagged_eqE_eq)
∀alpha beta, ordinal alphaordinal betaalpha ' = beta 'alpha = beta
Proof:
Proof not loaded.
L11095
Theorem. (tagged_ReplE)
∀alpha beta, ordinal alphaordinal betabeta ' {gamma '|gammaalpha}beta alpha
Proof:
Proof not loaded.
L11108
Theorem. (ordinal_notin_tagged_Repl)
∀alpha Y, ordinal alphaalpha {y '|yY}
Proof:
Proof not loaded.
L11122
Definition. We define SNoElts_ to be λalpha ⇒ alpha {beta '|betaalpha} of type setset.
L11124
Theorem. (SNoElts_mon)
∀alpha beta, alpha betaSNoElts_ alpha SNoElts_ beta
Proof:
Proof not loaded.
L11148
Definition. We define SNo_ to be λalpha x ⇒ x SNoElts_ alpha ∀betaalpha, exactly1of2 (beta ' x) (beta x) of type setsetprop.
L11152
Definition. We define PSNo to be λalpha p ⇒ {betaalpha|p beta} {beta '|betaalpha, ¬ p beta} of type set(setprop)set.
L11154
Theorem. (PNoEq_PSNo)
∀alpha, ordinal alpha∀p : setprop, PNoEq_ alpha (λbeta ⇒ beta PSNo alpha p) p
Proof:
Proof not loaded.
L11181
Theorem. (SNo_PSNo)
∀alpha, ordinal alpha∀p : setprop, SNo_ alpha (PSNo alpha p)
Proof:
Proof not loaded.
L11261
Theorem. (SNo_PSNo_eta_)
∀alpha x, ordinal alphaSNo_ alpha xx = PSNo alpha (λbeta ⇒ beta x)
Proof:
Proof not loaded.
L11328
Definition. We define SNo to be λx ⇒ ∃alpha, ordinal alpha SNo_ alpha x of type setprop.
L11329
Theorem. (SNo_SNo)
∀alpha, ordinal alpha∀z, SNo_ alpha zSNo z
Proof:
Proof not loaded.
L11340
Definition. We define SNoLev to be λx ⇒ Eps_i (λalpha ⇒ ordinal alpha SNo_ alpha x) of type setset.
L11341
Theorem. (SNoLev_uniq_Subq)
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha beta
Proof:
Proof not loaded.
L11374
Theorem. (SNoLev_uniq)
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha = beta
Proof:
Proof not loaded.
L11381
Theorem. (SNoLev_prop)
∀x, SNo xordinal (SNoLev x) SNo_ (SNoLev x) x
Proof:
Proof not loaded.
L11387
Theorem. (SNoLev_ordinal)
∀x, SNo xordinal (SNoLev x)
Proof:
Proof not loaded.
L11391
Theorem. (SNoLev_)
∀x, SNo xSNo_ (SNoLev x) x
Proof:
Proof not loaded.
L11395
Theorem. (SNo_PSNo_eta)
∀x, SNo xx = PSNo (SNoLev x) (λbeta ⇒ beta x)
Proof:
Proof not loaded.
L11405
Theorem. (SNoLev_PSNo)
∀alpha, ordinal alpha∀p : setprop, SNoLev (PSNo alpha p) = alpha
Proof:
Proof not loaded.
L11422
Theorem. (SNo_Subq)
∀x y, SNo xSNo ySNoLev x SNoLev y(∀alphaSNoLev x, alpha x alpha y)x y
Proof:
Proof not loaded.
L11467
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta x) (λbeta ⇒ beta y) of type setsetsetprop.
L11470
Theorem. (SNoEq_I)
∀alpha x y, (∀betaalpha, beta x beta y)SNoEq_ alpha x y
Proof:
Proof not loaded.
L11474
Theorem. (SNo_eq)
∀x y, SNo xSNo ySNoLev x = SNoLev ySNoEq_ (SNoLev x) x yx = y
Proof:
Proof not loaded.
End of Section TaggedSets
L11494
Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y) of type setsetprop.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
L11497
Definition. We define SNoLe to be λx y ⇒ PNoLe (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y) of type setsetprop.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L11501
Theorem. (SNoLtLe)
∀x y, x < yx y
Proof:
Proof not loaded.
L11508
Theorem. (SNoLeE)
∀x y, SNo xSNo yx yx < y x = y
Proof:
Proof not loaded.
L11522
Theorem. (SNoEq_sym_)
∀alpha x y, SNoEq_ alpha x ySNoEq_ alpha y x
Proof:
Proof not loaded.
L11527
Theorem. (SNoEq_tra_)
∀alpha x y z, SNoEq_ alpha x ySNoEq_ alpha y zSNoEq_ alpha x z
Proof:
Proof not loaded.
L11532
Theorem. (SNoLtE)
∀x y, SNo xSNo yx < y∀p : prop, (∀z, SNo zSNoLev z SNoLev x SNoLev ySNoEq_ (SNoLev z) z xSNoEq_ (SNoLev z) z yx < zz < ySNoLev z xSNoLev z yp)(SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yp)(SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xp)p
Proof:
Proof not loaded.
L11635
Theorem. (SNoLtI2)
∀x y, SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yx < y
Proof:
Proof not loaded.
L11650
Theorem. (SNoLtI3)
∀x y, SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xx < y
Proof:
Proof not loaded.
L11664
Theorem. (SNoLt_irref)
∀x, ¬ SNoLt x x
Proof:
Proof not loaded.
L11669
Theorem. (SNoLt_trichotomy_or)
∀x y, SNo xSNo yx < y x = y y < x
Proof:
Proof not loaded.
L11680
Theorem. (SNoLt_trichotomy_or_impred)
∀x y, SNo xSNo y∀p : prop, (x < yp)(x = yp)(y < xp)p
Proof:
Proof not loaded.
L11693
Theorem. (SNoLt_tra)
∀x y z, SNo xSNo ySNo zx < yy < zx < z
Proof:
Proof not loaded.
L11699
Theorem. (SNoLe_ref)
∀x, SNoLe x x
Proof:
Proof not loaded.
L11703
Theorem. (SNoLe_antisym)
∀x y, SNo xSNo yx yy xx = y
Proof:
Proof not loaded.
L11711
Theorem. (SNoLtLe_tra)
∀x y z, SNo xSNo ySNo zx < yy zx < z
Proof:
Proof not loaded.
L11716
Theorem. (SNoLeLt_tra)
∀x y z, SNo xSNo ySNo zx yy < zx < z
Proof:
Proof not loaded.
L11721
Theorem. (SNoLe_tra)
∀x y z, SNo xSNo ySNo zx yy zx z
Proof:
Proof not loaded.
L11726
Theorem. (SNoLtLe_or)
∀x y, SNo xSNo yx < y y x
Proof:
Proof not loaded.
L11735
Theorem. (SNoLt_PSNo_PNoLt)
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPSNo alpha p < PSNo beta qPNoLt alpha p beta q
Proof:
Proof not loaded.
L11758
Theorem. (PNoLt_SNoLt_PSNo)
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta qPSNo alpha p < PSNo beta q
Proof:
Proof not loaded.
L11781
Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λalpha p ⇒ ordinal alpha PSNo alpha p L) (λalpha p ⇒ ordinal alpha PSNo alpha p R)) (PNo_pred (λalpha p ⇒ ordinal alpha PSNo alpha p L) (λalpha p ⇒ ordinal alpha PSNo alpha p R)) of type setsetset.
L11784
Definition. We define SNoCutP to be λL R ⇒ (∀xL, SNo x) (∀yR, SNo y) (∀xL, ∀yR, x < y) of type setsetprop.
L11789
Theorem. (SNoCutP_SNoCut)
∀L R, SNoCutP L RSNo (SNoCut L R) SNoLev (SNoCut L R) ordsucc ((xLordsucc (SNoLev x)) (yRordsucc (SNoLev y))) (∀xL, x < SNoCut L R) (∀yR, SNoCut L R < y) (∀z, SNo z(∀xL, x < z)(∀yR, z < y)SNoLev (SNoCut L R) SNoLev z SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)
Proof:
Proof not loaded.
L12178
Theorem. (SNoCutP_SNoCut_impred)
∀L R, SNoCutP L R∀p : prop, (SNo (SNoCut L R)SNoLev (SNoCut L R) ordsucc ((xLordsucc (SNoLev x)) (yRordsucc (SNoLev y)))(∀xL, x < SNoCut L R)(∀yR, SNoCut L R < y)(∀z, SNo z(∀xL, x < z)(∀yR, z < y)SNoLev (SNoCut L R) SNoLev z SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)p)p
Proof:
Proof not loaded.
L12193
Theorem. (SNoCutP_L_0)
∀L, (∀xL, SNo x)SNoCutP L 0
Proof:
Proof not loaded.
L12204
Theorem. (SNoCutP_0_0)
Proof:
Proof not loaded.
L12208
Definition. We define SNoS_ to be λalpha ⇒ {x𝒫 (SNoElts_ alpha)|∃betaalpha, SNo_ beta x} of type setset.
L12210
Theorem. (SNoS_E)
∀alpha, ordinal alpha∀xSNoS_ alpha, ∃betaalpha, SNo_ beta x
Proof:
Proof not loaded.
Beginning of Section TaggedSets2
L12220
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
L12222
Theorem. (SNoS_I)
∀alpha, ordinal alpha∀x, ∀betaalpha, SNo_ beta xx SNoS_ alpha
Proof:
Proof not loaded.
L12247
Theorem. (SNoS_I2)
∀x y, SNo xSNo ySNoLev x SNoLev yx SNoS_ (SNoLev y)
Proof:
Proof not loaded.
L12253
Theorem. (SNoS_Subq)
∀alpha beta, ordinal alphaordinal betaalpha betaSNoS_ alpha SNoS_ beta
Proof:
Proof not loaded.
L12263
Theorem. (SNoLev_uniq2)
∀alpha, ordinal alpha∀x, SNo_ alpha xSNoLev x = alpha
Proof:
Proof not loaded.
L12276
Theorem. (SNoS_E2)
∀alpha, ordinal alpha∀xSNoS_ alpha, ∀p : prop, (SNoLev x alphaordinal (SNoLev x)SNo xSNo_ (SNoLev x) xp)p
Proof:
Proof not loaded.
L12300
Theorem. (SNoS_In_neq)
∀w, SNo w∀xSNoS_ (SNoLev w), x w
Proof:
Proof not loaded.
L12316
Theorem. (SNoS_SNoLev)
∀z, SNo zz SNoS_ (ordsucc (SNoLev z))
Proof:
Proof not loaded.
L12324
Definition. We define SNoL to be λz ⇒ {xSNoS_ (SNoLev z)|x < z} of type setset.
L12326
Definition. We define SNoR to be λz ⇒ {ySNoS_ (SNoLev z)|z < y} of type setset.
L12327
Theorem. (SNoCutP_SNoL_SNoR)
∀z, SNo zSNoCutP (SNoL z) (SNoR z)
Proof:
Proof not loaded.
L12375
Theorem. (SNoL_E)
∀x, SNo x∀wSNoL x, ∀p : prop, (SNo wSNoLev w SNoLev xw < xp)p
Proof:
Proof not loaded.
L12393
Theorem. (SNoR_E)
∀x, SNo x∀zSNoR x, ∀p : prop, (SNo zSNoLev z SNoLev xx < zp)p
Proof:
Proof not loaded.
L12411
Theorem. (SNoL_SNoS_)
∀z, SNoL z SNoS_ (SNoLev z)
Proof:
Proof not loaded.
L12415
Theorem. (SNoR_SNoS_)
∀z, SNoR z SNoS_ (SNoLev z)
Proof:
Proof not loaded.
L12419
Theorem. (SNoL_SNoS)
∀x, SNo x∀wSNoL x, w SNoS_ (SNoLev x)
Proof:
Proof not loaded.
L12429
Theorem. (SNoR_SNoS)
∀x, SNo x∀zSNoR x, z SNoS_ (SNoLev x)
Proof:
Proof not loaded.
L12439
Theorem. (SNoL_I)
∀z, SNo z∀x, SNo xSNoLev x SNoLev zx < zx SNoL z
Proof:
Proof not loaded.
L12449
Theorem. (SNoR_I)
∀z, SNo z∀y, SNo ySNoLev y SNoLev zz < yy SNoR z
Proof:
Proof not loaded.
L12459
Theorem. (SNo_eta)
∀z, SNo zz = SNoCut (SNoL z) (SNoR z)
Proof:
Proof not loaded.
L12533
Theorem. (SNoCutP_SNo_SNoCut)
∀L R, SNoCutP L RSNo (SNoCut L R)
Proof:
Proof not loaded.
L12542
Theorem. (SNoCutP_SNoCut_L)
∀L R, SNoCutP L R∀xL, x < SNoCut L R
Proof:
Proof not loaded.
L12550
Theorem. (SNoCutP_SNoCut_R)
∀L R, SNoCutP L R∀yR, SNoCut L R < y
Proof:
Proof not loaded.
L12557
Theorem. (SNoCutP_SNoCut_fst)
∀L R, SNoCutP L R∀z, SNo z(∀xL, x < z)(∀yR, z < y)SNoLev (SNoCut L R) SNoLev z SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z
Proof:
Proof not loaded.
L12569
Theorem. (SNoCut_Le)
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(∀wL1, w < SNoCut L2 R2)(∀zR2, SNoCut L1 R1 < z)SNoCut L1 R1 SNoCut L2 R2
Proof:
Proof not loaded.
L12672
Theorem. (SNoCut_ext)
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(∀wL1, w < SNoCut L2 R2)(∀zR1, SNoCut L2 R2 < z)(∀wL2, w < SNoCut L1 R1)(∀zR2, SNoCut L1 R1 < z)SNoCut L1 R1 = SNoCut L2 R2
Proof:
Proof not loaded.
L12695
Theorem. (SNoLt_SNoL_or_SNoR_impred)
∀x y, SNo xSNo yx < y∀p : prop, (∀zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)p
Proof:
Proof not loaded.
L12717
Theorem. (SNoL_or_SNoR_impred)
∀x y, SNo xSNo y∀p : prop, (x = yp)(∀zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)(∀zSNoR y, z SNoL xp)(x SNoR yp)(y SNoL xp)p
Proof:
Proof not loaded.
L12743
Theorem. (SNoL_SNoCutP_ex)
∀L R, SNoCutP L R∀wSNoL (SNoCut L R), ∃w'L, w w'
Proof:
Proof not loaded.
L12783
Theorem. (SNoR_SNoCutP_ex)
∀L R, SNoCutP L R∀zSNoR (SNoCut L R), ∃z'R, z' z
Proof:
Proof not loaded.
L12823
Theorem. (ordinal_SNo_)
∀alpha, ordinal alphaSNo_ alpha alpha
Proof:
Proof not loaded.
L12846
Theorem. (ordinal_SNo)
∀alpha, ordinal alphaSNo alpha
Proof:
Proof not loaded.
L12855
Theorem. (ordinal_SNoLev)
∀alpha, ordinal alphaSNoLev alpha = alpha
Proof:
Proof not loaded.
L12864
Theorem. (ordinal_SNoLev_max)
∀alpha, ordinal alpha∀z, SNo zSNoLev z alphaz < alpha
Proof:
Proof not loaded.
L12911
Theorem. (ordinal_SNoL)
∀alpha, ordinal alphaSNoL alpha = SNoS_ alpha
Proof:
Proof not loaded.
L12943
Theorem. (ordinal_SNoR)
∀alpha, ordinal alphaSNoR alpha = Empty
Proof:
Proof not loaded.
L12965
Theorem. (nat_p_SNo)
∀n, nat_p nSNo n
Proof:
Proof not loaded.
L12973
Theorem. (omega_SNo)
∀nω, SNo n
Proof:
Proof not loaded.
L12980
Proof:
Proof not loaded.
L12988
Theorem. (ordinal_In_SNoLt)
∀alpha, ordinal alpha∀betaalpha, beta < alpha
Proof:
Proof not loaded.
L13004
Theorem. (ordinal_SNoLev_max_2)
∀alpha, ordinal alpha∀z, SNo zSNoLev z ordsucc alphaz alpha
Proof:
Proof not loaded.
L13083
Theorem. (ordinal_Subq_SNoLe)
∀alpha beta, ordinal alphaordinal betaalpha betaalpha beta
Proof:
Proof not loaded.
L13105
Theorem. (ordinal_SNoLt_In)
∀alpha beta, ordinal alphaordinal betaalpha < betaalpha beta
Proof:
Proof not loaded.
L13118
Theorem. (omega_nonneg)
∀mω, 0 m
Proof:
Proof not loaded.
L13124
Theorem. (SNo_0)
Proof:
Proof not loaded.
L13128
Theorem. (SNo_1)
Proof:
Proof not loaded.
L13132
Theorem. (SNo_2)
Proof:
Proof not loaded.
L13136
Theorem. (SNoLev_0)
Proof:
Proof not loaded.
L13140
Theorem. (SNoCut_0_0)
Proof:
Proof not loaded.
L13165
Theorem. (SNoL_0)
Proof:
Proof not loaded.
L13180
Theorem. (SNoR_0)
Proof:
Proof not loaded.
L13195
Theorem. (SNoL_1)
Proof:
Proof not loaded.
L13231
Theorem. (SNoR_1)
Proof:
Proof not loaded.
L13235
Theorem. (SNo_max_SNoLev)
∀x, SNo x(∀ySNoS_ (SNoLev x), y < x)SNoLev x = x
Proof:
Proof not loaded.
L13282
Theorem. (SNo_max_ordinal)
∀x, SNo x(∀ySNoS_ (SNoLev x), y < x)ordinal x
Proof:
Proof not loaded.
L13291
Theorem. (pos_low_eq_one)
∀x, SNo x0 < xSNoLev x 1x = 1
Proof:
Proof not loaded.
L13338
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta x delta SNoLev x) of type setset.
L13340
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta x delta = SNoLev x) of type setset.
L13341
Theorem. (SNo_extend0_SNo_)
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
Proof:
Proof not loaded.
L13349
Theorem. (SNo_extend1_SNo_)
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
Proof:
Proof not loaded.
L13357
Theorem. (SNo_extend0_SNo)
∀x, SNo xSNo (SNo_extend0 x)
Proof:
Proof not loaded.
L13364
Theorem. (SNo_extend1_SNo)
∀x, SNo xSNo (SNo_extend1 x)
Proof:
Proof not loaded.
L13371
Theorem. (SNo_extend0_SNoLev)
∀x, SNo xSNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
Proof:
Proof not loaded.
L13378
Theorem. (SNo_extend1_SNoLev)
∀x, SNo xSNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
Proof:
Proof not loaded.
L13385
Theorem. (SNo_extend0_nIn)
∀x, SNo xSNoLev x SNo_extend0 x
Proof:
Proof not loaded.
L13408
Theorem. (SNo_extend1_In)
∀x, SNo xSNoLev x SNo_extend1 x
Proof:
Proof not loaded.
L13420
Theorem. (SNo_extend0_SNoEq)
∀x, SNo xSNoEq_ (SNoLev x) (SNo_extend0 x) x
Proof:
Proof not loaded.
L13444
Theorem. (SNo_extend1_SNoEq)
∀x, SNo xSNoEq_ (SNoLev x) (SNo_extend1 x) x
Proof:
Proof not loaded.
L13468
Theorem. (SNoLev_0_eq_0)
∀x, SNo xSNoLev x = 0x = 0
Proof:
Proof not loaded.
L13478
Definition. We define eps_ to be λn ⇒ {0} {(ordsucc m) '|mn} of type setset.
L13481
Theorem. (eps_ordinal_In_eq_0)
∀n alpha, ordinal alphaalpha eps_ nalpha = 0
Proof:
Proof not loaded.
(*** eps_ n is the Surreal Number 1/2^n, without needing to define division or exponents first ***)
L13496
Theorem. (eps_0_1)
Proof:
Proof not loaded.
L13511
Theorem. (SNo__eps_)
∀nω, SNo_ (ordsucc n) (eps_ n)
Proof:
Proof not loaded.
L13609
Theorem. (SNo_eps_)
∀nω, SNo (eps_ n)
Proof:
Proof not loaded.
L13616
Theorem. (SNo_eps_1)
Proof:
Proof not loaded.
L13620
Theorem. (SNoLev_eps_)
Proof:
Proof not loaded.
L13627
Proof:
Proof not loaded.
L13634
Theorem. (SNo_eps_decr)
∀nω, ∀mn, eps_ n < eps_ m
Proof:
Proof not loaded.
L13672
Theorem. (SNo_eps_pos)
∀nω, 0 < eps_ n
Proof:
Proof not loaded.
L13689
Theorem. (SNo_pos_eps_Lt)
∀n, nat_p n∀xSNoS_ (ordsucc n), 0 < xeps_ n < x
Proof:
Proof not loaded.
L13736
Theorem. (SNo_pos_eps_Le)
∀n, nat_p n∀xSNoS_ (ordsucc (ordsucc n)), 0 < xeps_ n x
Proof:
Proof not loaded.
L13782
Theorem. (eps_SNo_eq)
∀n, nat_p n∀xSNoS_ (ordsucc n), 0 < xSNoEq_ (SNoLev x) (eps_ n) x∃mn, x = eps_ m
Proof:
Proof not loaded.
L13840
Proof:
Proof not loaded.
L13867
Proof:
Proof not loaded.
End of Section TaggedSets2
L14047
Theorem. (SNo_etaE)
∀z, SNo z∀p : prop, (∀L R, SNoCutP L R(∀xL, SNoLev x SNoLev z)(∀yR, SNoLev y SNoLev z)z = SNoCut L Rp)p
Proof:
Proof not loaded.
L14158
Theorem. (SNo_ind)
∀P : setprop, (∀L R, SNoCutP L R(∀xL, P x)(∀yR, P y)P (SNoCut L R))∀z, SNo zP z
Proof:
Proof not loaded.
Beginning of Section SurrealRecI
L14211
Variable F : set(setset)set
(*** surreal recursion ***)
L14212
Let default : setEps_i (λ_ ⇒ True)
L14213
Let G : set(setsetset)setsetλalpha g ⇒ If_ii (ordinal alpha) (λz : setif z SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : setdefault)
L14223
Definition. We define SNo_rec_i to be λz ⇒ In_rec_ii G (SNoLev z) z of type setset.
L14225
Hypothesis Fr : ∀z, SNo z∀g h : setset, (∀wSNoS_ (SNoLev z), g w = h w)F z g = F z h
L14228
Theorem. (SNo_rec_i_eq)
∀z, SNo zSNo_rec_i z = F z SNo_rec_i
Proof:
Proof not loaded.
End of Section SurrealRecI
Beginning of Section SurrealRecII
L14305
Variable F : set(set(setset))(setset)
L14306
Let default : (setset)Descr_ii (λ_ ⇒ True)
L14307
Let G : set(setset(setset))set(setset)λalpha g ⇒ If_iii (ordinal alpha) (λz : setIf_ii (z SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : setdefault)
L14316
Definition. We define SNo_rec_ii to be λz ⇒ In_rec_iii G (SNoLev z) z of type set(setset).
L14318
Hypothesis Fr : ∀z, SNo z∀g h : set(setset), (∀wSNoS_ (SNoLev z), g w = h w)F z g = F z h
L14321
Theorem. (SNo_rec_ii_eq)
∀z, SNo zSNo_rec_ii z = F z SNo_rec_ii
Proof:
Proof not loaded.
End of Section SurrealRecII
Beginning of Section SurrealRec2
L14398
Variable F : setset(setsetset)set
L14399
Let G : set(setsetset)set(setset)setλw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)
L14401
Let H : set(setsetset)setsetλw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty
L14404
Definition. We define SNo_rec2 to be SNo_rec_ii H of type setsetset.
L14406
Hypothesis Fr : ∀w, SNo w∀z, SNo z∀g h : setsetset, (∀xSNoS_ (SNoLev w), ∀y, SNo yg x y = h x y)(∀ySNoS_ (SNoLev z), g w y = h w y)F w z g = F w z h
L14411
Theorem. (SNo_rec2_G_prop)
∀w, SNo w∀f k : setsetset, (∀xSNoS_ (SNoLev w), f x = k x)∀z, SNo z∀g h : setset, (∀uSNoS_ (SNoLev z), g u = h u)G w f z g = G w k z h
Proof:
Proof not loaded.
L14448
Theorem. (SNo_rec2_eq_1)
∀w, SNo w∀f : setsetset, ∀z, SNo zSNo_rec_i (G w f) z = G w f z (SNo_rec_i (G w f))
Proof:
Proof not loaded.
L14462
Theorem. (SNo_rec2_eq)
∀w, SNo w∀z, SNo zSNo_rec2 w z = F w z SNo_rec2
Proof:
Proof not loaded.
End of Section SurrealRec2
L14559
Theorem. (SNo_ordinal_ind)
∀P : setprop, (∀alpha, ordinal alpha∀xSNoS_ alpha, P x)(∀x, SNo xP x)
Proof:
Proof not loaded.
L14575
Theorem. (SNo_ordinal_ind2)
∀P : setsetprop, (∀alpha, ordinal alpha∀beta, ordinal beta∀xSNoS_ alpha, ∀ySNoS_ beta, P x y)(∀x y, SNo xSNo yP x y)
Proof:
Proof not loaded.
L14603
Theorem. (SNo_ordinal_ind3)
∀P : setsetsetprop, (∀alpha, ordinal alpha∀beta, ordinal beta∀gamma, ordinal gamma∀xSNoS_ alpha, ∀ySNoS_ beta, ∀zSNoS_ gamma, P x y z)(∀x y z, SNo xSNo ySNo zP x y z)
Proof:
Proof not loaded.
L14640
Theorem. (SNoLev_ind)
∀P : setprop, (∀x, SNo x(∀wSNoS_ (SNoLev x), P w)P x)(∀x, SNo xP x)
Proof:
Proof not loaded.
L14663
Theorem. (SNoLev_ind2)
∀P : setsetprop, (∀x y, SNo xSNo y(∀wSNoS_ (SNoLev x), P w y)(∀zSNoS_ (SNoLev y), P x z)(∀wSNoS_ (SNoLev x), ∀zSNoS_ (SNoLev y), P w z)P x y)∀x y, SNo xSNo yP x y
Proof:
Proof not loaded.
L14709
Theorem. (SNoLev_ind3)
∀P : setsetsetprop, (∀x y z, SNo xSNo ySNo z(∀uSNoS_ (SNoLev x), P u y z)(∀vSNoS_ (SNoLev y), P x v z)(∀wSNoS_ (SNoLev z), P x y w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), P u v z)(∀uSNoS_ (SNoLev x), ∀wSNoS_ (SNoLev z), P u y w)(∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), P x v w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), P u v w)P x y z)∀x y z, SNo xSNo ySNo zP x y z
Proof:
Proof not loaded.
L14788
Theorem. (SNo_omega)
Proof:
Proof not loaded.
L14792
Theorem. (SNoLt_0_1)
0 < 1
Proof:
Proof not loaded.
L14798
Theorem. (SNoLt_0_2)
0 < 2
Proof:
Proof not loaded.
L14804
Theorem. (SNoLt_1_2)
1 < 2
Proof:
Proof not loaded.
L14810
Theorem. (restr_SNo_)
∀x, SNo x∀alphaSNoLev x, SNo_ alpha (x SNoElts_ alpha)
Proof:
Proof not loaded.
L14850
Theorem. (restr_SNo)
∀x, SNo x∀alphaSNoLev x, SNo (x SNoElts_ alpha)
Proof:
Proof not loaded.
L14859
Theorem. (restr_SNoLev)
∀x, SNo x∀alphaSNoLev x, SNoLev (x SNoElts_ alpha) = alpha
Proof:
Proof not loaded.
L14868
Theorem. (restr_SNoEq)
∀x, SNo x∀alphaSNoLev x, SNoEq_ alpha (x SNoElts_ alpha) x
Proof:
Proof not loaded.
L14884
Theorem. (SNo_extend0_restr_eq)
∀x, SNo xx = SNo_extend0 x SNoElts_ (SNoLev x)
Proof:
Proof not loaded.
L14909
Theorem. (SNo_extend1_restr_eq)
∀x, SNo xx = SNo_extend1 x SNoElts_ (SNoLev x)
Proof:
Proof not loaded.
Beginning of Section SurrealMinus
L14939
Definition. We define minus_SNo to be SNo_rec_i (λx m ⇒ SNoCut {m z|zSNoR x} {m w|wSNoL x}) of type setset.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L14944
Theorem. (minus_SNo_eq)
∀x, SNo x- x = SNoCut {- z|zSNoR x} {- w|wSNoL x}
Proof:
Proof not loaded.
L14975
Theorem. (minus_SNo_prop1)
∀x, SNo xSNo (- x) (∀uSNoL x, - x < - u) (∀uSNoR x, - u < - x) SNoCutP {- z|zSNoR x} {- w|wSNoL x}
Proof:
Proof not loaded.
L15166
Theorem. (SNo_minus_SNo)
∀x, SNo xSNo (- x)
Proof:
Proof not loaded.
L15173
Theorem. (minus_SNo_Lt_contra)
∀x y, SNo xSNo yx < y- y < - x
Proof:
Proof not loaded.
L15242
Theorem. (minus_SNo_Le_contra)
∀x y, SNo xSNo yx y- y - x
Proof:
Proof not loaded.
L15260
Theorem. (minus_SNo_SNoCutP)
∀x, SNo xSNoCutP {- z|zSNoR x} {- w|wSNoL x}
Proof:
Proof not loaded.
L15268
Theorem. (minus_SNo_SNoCutP_gen)
∀L R, SNoCutP L RSNoCutP {- z|zR} {- w|wL}
Proof:
Proof not loaded.
L15319
Theorem. (minus_SNo_Lev_lem1)
∀alpha, ordinal alpha∀xSNoS_ alpha, SNoLev (- x) SNoLev x
Proof:
Proof not loaded.
L15490
Theorem. (minus_SNo_Lev_lem2)
∀x, SNo xSNoLev (- x) SNoLev x
Proof:
Proof not loaded.
L15501
Theorem. (minus_SNo_invol)
∀x, SNo x- - x = x
Proof:
Proof not loaded.
L15569
Theorem. (minus_SNo_Lev)
∀x, SNo xSNoLev (- x) = SNoLev x
Proof:
Proof not loaded.
L15580
Theorem. (minus_SNo_SNo_)
∀alpha, ordinal alpha∀x, SNo_ alpha xSNo_ alpha (- x)
Proof:
Proof not loaded.
L15597
Theorem. (minus_SNo_SNoS_)
∀alpha, ordinal alpha∀x, x SNoS_ alpha- x SNoS_ alpha
Proof:
Proof not loaded.
L15610
Theorem. (minus_SNoCut_eq_lem)
∀v, SNo v∀L R, SNoCutP L Rv = SNoCut L R- v = SNoCut {- z|zR} {- w|wL}
Proof:
Proof not loaded.
L15720
Theorem. (minus_SNoCut_eq)
∀L R, SNoCutP L R- SNoCut L R = SNoCut {- z|zR} {- w|wL}
Proof:
Proof not loaded.
L15725
Theorem. (minus_SNo_Lt_contra1)
∀x y, SNo xSNo y- x < y- y < x
Proof:
Proof not loaded.
L15738
Theorem. (minus_SNo_Lt_contra2)
∀x y, SNo xSNo yx < - yy < - x
Proof:
Proof not loaded.
L15751
Theorem. (mordinal_SNoLev_min_2)
∀alpha, ordinal alpha∀z, SNo zSNoLev z ordsucc alpha- alpha z
Proof:
Proof not loaded.
L15767
Proof:
Proof not loaded.
L15783
Theorem. (SNoL_minus_SNoR)
∀x, SNo xSNoL (- x) = {- w|wSNoR x}
Proof:
Proof not loaded.
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
L15831
Definition. We define add_SNo to be SNo_rec2 (λx y a ⇒ SNoCut ({a w y|wSNoL x} {a x w|wSNoL y}) ({a z y|zSNoR x} {a x z|zSNoR y})) of type setsetset.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
L15834
Theorem. (add_SNo_eq)
∀x, SNo x∀y, SNo yx + y = SNoCut ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Proof:
Proof not loaded.
L15890
Theorem. (add_SNo_prop1)
∀x y, SNo xSNo ySNo (x + y) (∀uSNoL x, u + y < x + y) (∀uSNoR x, x + y < u + y) (∀uSNoL y, x + u < x + y) (∀uSNoR y, x + y < x + u) SNoCutP ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Proof:
Proof not loaded.
L16351
Theorem. (SNo_add_SNo)
∀x y, SNo xSNo ySNo (x + y)
Proof:
Proof not loaded.
L16361
Theorem. (SNo_add_SNo_3)
∀x y z, SNo xSNo ySNo zSNo (x + y + z)
Proof:
Proof not loaded.
L16370
Theorem. (SNo_add_SNo_3c)
∀x y z, SNo xSNo ySNo zSNo (x + y + - z)
Proof:
Proof not loaded.
L16378
Theorem. (SNo_add_SNo_4)
∀x y z w, SNo xSNo ySNo zSNo wSNo (x + y + z + w)
Proof:
Proof not loaded.
L16383
Theorem. (add_SNo_Lt1)
∀x y z, SNo xSNo ySNo zx < zx + y < z + y
Proof:
Proof not loaded.
L16448
Theorem. (add_SNo_Le1)
∀x y z, SNo xSNo ySNo zx zx + y z + y
Proof:
Proof not loaded.
L16460
Theorem. (add_SNo_Lt2)
∀x y z, SNo xSNo ySNo zy < zx + y < x + z
Proof:
Proof not loaded.
L16526
Theorem. (add_SNo_Le2)
∀x y z, SNo xSNo ySNo zy zx + y x + z
Proof:
Proof not loaded.
L16538
Theorem. (add_SNo_Lt3a)
∀x y z w, SNo xSNo ySNo zSNo wx < zy wx + y < z + w
Proof:
Proof not loaded.
L16551
Theorem. (add_SNo_Lt3b)
∀x y z w, SNo xSNo ySNo zSNo wx zy < wx + y < z + w
Proof:
Proof not loaded.
L16564
Theorem. (add_SNo_Lt3)
∀x y z w, SNo xSNo ySNo zSNo wx < zy < wx + y < z + w
Proof:
Proof not loaded.
L16579
Theorem. (add_SNo_Le3)
∀x y z w, SNo xSNo ySNo zSNo wx zy wx + y z + w
Proof:
Proof not loaded.
L16592
Theorem. (add_SNo_SNoCutP)
∀x y, SNo xSNo ySNoCutP ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Proof:
Proof not loaded.
L16600
Theorem. (add_SNo_com)
∀x y, SNo xSNo yx + y = y + x
Proof:
Proof not loaded.
L16701
Theorem. (add_SNo_0L)
∀x, SNo x0 + x = x
Proof:
Proof not loaded.
L16764
Theorem. (add_SNo_0R)
∀x, SNo xx + 0 = x
Proof:
Proof not loaded.
L16770
Theorem. (add_SNo_minus_SNo_linv)
∀x, SNo x- x + x = 0
Proof:
Proof not loaded.
L16945
Theorem. (add_SNo_minus_SNo_rinv)
∀x, SNo xx + - x = 0
Proof:
Proof not loaded.
L16955
Theorem. (add_SNo_ordinal_SNoCutP)
∀alpha, ordinal alpha∀beta, ordinal betaSNoCutP ({x + beta|xSNoS_ alpha} {alpha + x|xSNoS_ beta}) Empty
Proof:
Proof not loaded.
L16995
Theorem. (add_SNo_ordinal_eq)
∀alpha, ordinal alpha∀beta, ordinal betaalpha + beta = SNoCut ({x + beta|xSNoS_ alpha} {alpha + x|xSNoS_ beta}) Empty
Proof:
Proof not loaded.
L17027
Theorem. (add_SNo_ordinal_ordinal)
∀alpha, ordinal alpha∀beta, ordinal betaordinal (alpha + beta)
Proof:
Proof not loaded.
L17092
Theorem. (add_SNo_ordinal_SL)
∀alpha, ordinal alpha∀beta, ordinal betaordsucc alpha + beta = ordsucc (alpha + beta)
Proof:
Proof not loaded.
L17244
Theorem. (add_SNo_ordinal_SR)
∀alpha, ordinal alpha∀beta, ordinal betaalpha + ordsucc beta = ordsucc (alpha + beta)
Proof:
Proof not loaded.
L17265
Theorem. (add_SNo_ordinal_InL)
∀alpha, ordinal alpha∀beta, ordinal beta∀gammaalpha, gamma + beta alpha + beta
Proof:
Proof not loaded.
L17289
Theorem. (add_SNo_ordinal_InR)
∀alpha, ordinal alpha∀beta, ordinal beta∀gammabeta, alpha + gamma alpha + beta
Proof:
Proof not loaded.
L17306
Theorem. (add_nat_add_SNo)
∀n mω, add_nat n m = n + m
Proof:
Proof not loaded.
L17335
Theorem. (add_SNo_In_omega)
∀n mω, n + m ω
Proof:
Proof not loaded.
L17344
Theorem. (add_SNo_1_1_2)
1 + 1 = 2
Proof:
Proof not loaded.
L17349
Theorem. (add_SNo_SNoL_interpolate)
∀x y, SNo xSNo y∀uSNoL (x + y), (∃vSNoL x, u v + y) (∃vSNoL y, u x + v)
Proof:
Proof not loaded.
L17506
Theorem. (add_SNo_SNoR_interpolate)
∀x y, SNo xSNo y∀uSNoR (x + y), (∃vSNoR x, v + y u) (∃vSNoR y, x + v u)
Proof:
Proof not loaded.
L17663
Theorem. (add_SNo_assoc)
∀x y z, SNo xSNo ySNo zx + (y + z) = (x + y) + z
Proof:
Proof not loaded.
L18079
Theorem. (add_SNo_minus_R2)
∀x y, SNo xSNo y(x + y) + - y = x
Proof:
Proof not loaded.
L18088
Theorem. (add_SNo_minus_R2')
∀x y, SNo xSNo y(x + - y) + y = x
Proof:
Proof not loaded.
L18094
Theorem. (add_SNo_minus_L2)
∀x y, SNo xSNo y- x + (x + y) = y
Proof:
Proof not loaded.
L18103
Theorem. (add_SNo_minus_L2')
∀x y, SNo xSNo yx + (- x + y) = y
Proof:
Proof not loaded.
L18109
Theorem. (add_SNo_cancel_L)
∀x y z, SNo xSNo ySNo zx + y = x + zy = z
Proof:
Proof not loaded.
L18122
Theorem. (add_SNo_cancel_R)
∀x y z, SNo xSNo ySNo zx + y = z + yx = z
Proof:
Proof not loaded.
L18136
Theorem. (minus_SNo_0)
- 0 = 0
Proof:
Proof not loaded.
L18144
Theorem. (minus_add_SNo_distr)
∀x y, SNo xSNo y- (x + y) = (- x) + (- y)
Proof:
Proof not loaded.
L18174
Theorem. (minus_add_SNo_distr_3)
∀x y z, SNo xSNo ySNo z- (x + y + z) = - x + - y + - z
Proof:
Proof not loaded.
L18182
Theorem. (add_SNo_Lev_bd)
∀x y, SNo xSNo ySNoLev (x + y) SNoLev x + SNoLev y
Proof:
Proof not loaded.
L18546
Theorem. (add_SNo_SNoS_omega)
∀x ySNoS_ ω, x + y SNoS_ ω
Proof:
Proof not loaded.
L18576
Theorem. (add_SNo_Lt1_cancel)
∀x y z, SNo xSNo ySNo zx + y < z + yx < z
Proof:
Proof not loaded.
L18592
Theorem. (add_SNo_Lt2_cancel)
∀x y z, SNo xSNo ySNo zx + y < x + zy < z
Proof:
Proof not loaded.
L18599
Theorem. (add_SNo_Le1_cancel)
∀x y z, SNo xSNo ySNo zx + y z + yx z
Proof:
Proof not loaded.
L18615
Theorem. (add_SNo_assoc_4)
∀x y z w, SNo xSNo ySNo zSNo wx + y + z + w = (x + y + z) + w
Proof:
Proof not loaded.
L18625
Theorem. (add_SNo_com_3_0_1)
∀x y z, SNo xSNo ySNo zx + y + z = y + x + z
Proof:
Proof not loaded.
L18635
Theorem. (add_SNo_com_3b_1_2)
∀x y z, SNo xSNo ySNo z(x + y) + z = (x + z) + y
Proof:
Proof not loaded.
L18645
Theorem. (add_SNo_com_4_inner_mid)
∀x y z w, SNo xSNo ySNo zSNo w(x + y) + (z + w) = (x + z) + (y + w)
Proof:
Proof not loaded.
L18657
Theorem. (add_SNo_rotate_3_1)
∀x y z, SNo xSNo ySNo zx + y + z = z + x + y
Proof:
Proof not loaded.
L18671
Theorem. (add_SNo_rotate_4_1)
∀x y z w, SNo xSNo ySNo zSNo wx + y + z + w = w + x + y + z
Proof:
Proof not loaded.
L18679
Theorem. (add_SNo_rotate_5_1)
∀x y z w v, SNo xSNo ySNo zSNo wSNo vx + y + z + w + v = v + x + y + z + w
Proof:
Proof not loaded.
L18687
Theorem. (add_SNo_rotate_5_2)
∀x y z w v, SNo xSNo ySNo zSNo wSNo vx + y + z + w + v = w + v + x + y + z
Proof:
Proof not loaded.
L18695
Theorem. (add_SNo_minus_SNo_prop2)
∀x y, SNo xSNo yx + - x + y = y
Proof:
Proof not loaded.
L18704
Theorem. (add_SNo_minus_SNo_prop3)
∀x y z w, SNo xSNo ySNo zSNo w(x + y + z) + (- z + w) = x + y + w
Proof:
Proof not loaded.
L18715
Theorem. (add_SNo_minus_SNo_prop5)
∀x y z w, SNo xSNo ySNo zSNo w(x + y + - z) + (z + w) = x + y + w
Proof:
Proof not loaded.
L18723
Theorem. (add_SNo_minus_Lt1)
∀x y z, SNo xSNo ySNo zx + - y < zx < z + y
Proof:
Proof not loaded.
L18733
Theorem. (add_SNo_minus_Lt2)
∀x y z, SNo xSNo ySNo zz < x + - yz + y < x
Proof:
Proof not loaded.
L18744
Theorem. (add_SNo_minus_Lt1b)
∀x y z, SNo xSNo ySNo zx < z + yx + - y < z
Proof:
Proof not loaded.
L18754
Theorem. (add_SNo_minus_Lt2b)
∀x y z, SNo xSNo ySNo zz + y < xz < x + - y
Proof:
Proof not loaded.
L18764
Theorem. (add_SNo_minus_Lt1b3)
∀x y z w, SNo xSNo ySNo zSNo wx + y < w + zx + y + - z < w
Proof:
Proof not loaded.
L18773
Theorem. (add_SNo_minus_Lt2b3)
∀x y z w, SNo xSNo ySNo zSNo ww + z < x + yw < x + y + - z
Proof:
Proof not loaded.
L18782
Theorem. (add_SNo_minus_Lt_lem)
∀x y z u v w, SNo xSNo ySNo zSNo uSNo vSNo wx + y + w < u + v + zx + y + - z < u + v + - w
Proof:
Proof not loaded.
L18812
Theorem. (add_SNo_minus_Le2)
∀x y z, SNo xSNo ySNo zz x + - yz + y x
Proof:
Proof not loaded.
L18825
Theorem. (add_SNo_minus_Le2b)
∀x y z, SNo xSNo ySNo zz + y xz x + - y
Proof:
Proof not loaded.
L18838
Theorem. (add_SNo_Lt_subprop2)
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx + u < z + vy + v < w + ux + y < z + w
Proof:
Proof not loaded.
L18869
Theorem. (add_SNo_Lt_subprop3a)
∀x y z w u a, SNo xSNo ySNo zSNo wSNo uSNo ax + z < w + ay + a < ux + y + z < w + u
Proof:
Proof not loaded.
L18892
Theorem. (add_SNo_Lt_subprop3b)
∀x y w u v a, SNo xSNo ySNo wSNo uSNo vSNo ax + a < w + vy < a + ux + y < w + u + v
Proof:
Proof not loaded.
L18909
Theorem. (add_SNo_Lt_subprop3c)
∀x y z w u a b c, SNo xSNo ySNo zSNo wSNo uSNo aSNo bSNo cx + a < b + cy + c < ub + z < w + ax + y + z < w + u
Proof:
Proof not loaded.
L18943
Theorem. (add_SNo_Lt_subprop3d)
∀x y w u v a b c, SNo xSNo ySNo wSNo uSNo vSNo aSNo bSNo cx + a < b + vy < c + ub + c < w + ax + y < w + u + v
Proof:
Proof not loaded.
L19003
Theorem. (ordinal_ordsucc_SNo_eq)
∀alpha, ordinal alphaordsucc alpha = 1 + alpha
Proof:
Proof not loaded.
L19011
Theorem. (add_SNo_3a_2b)
∀x y z w u, SNo xSNo ySNo zSNo wSNo u(x + y + z) + (w + u) = (u + y + z) + (w + x)
Proof:
Proof not loaded.
L19024
Theorem. (add_SNo_1_ordsucc)
∀nω, n + 1 = ordsucc n
Proof:
Proof not loaded.
L19034
Theorem. (add_SNo_eps_Lt)
∀x, SNo x∀nω, x < x + eps_ n
Proof:
Proof not loaded.
L19042
Theorem. (add_SNo_eps_Lt')
∀x y, SNo xSNo y∀nω, x < yx < y + eps_ n
Proof:
Proof not loaded.
L19050
Theorem. (SNoLt_minus_pos)
∀x y, SNo xSNo yx < y0 < y + - x
Proof:
Proof not loaded.
L19057
Theorem. (add_SNo_omega_In_cases)
∀m, ∀nω, ∀k, nat_p km n + km n m + - n k
Proof:
Proof not loaded.
L19083
Theorem. (add_SNo_Lt4)
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx < wy < uz < vx + y + z < w + u + v
Proof:
Proof not loaded.
L19092
Theorem. (add_SNo_3_3_3_Lt1)
∀x y z w u, SNo xSNo ySNo zSNo wSNo ux + y < z + wx + y + u < z + w + u
Proof:
Proof not loaded.
L19101
Theorem. (add_SNo_3_2_3_Lt1)
∀x y z w u, SNo xSNo ySNo zSNo wSNo uy + x < z + wx + u + y < z + w + u
Proof:
Proof not loaded.
L19109
Theorem. (add_SNo_minus_Lt12b3)
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx + y + v < w + u + zx + y + - z < w + u + - v
Proof:
Proof not loaded.
L19132
Theorem. (add_SNo_minus_Le1b)
∀x y z, SNo xSNo ySNo zx z + yx + - y z
Proof:
Proof not loaded.
L19142
Theorem. (add_SNo_minus_Le1b3)
∀x y z w, SNo xSNo ySNo zSNo wx + y w + zx + y + - z w
Proof:
Proof not loaded.
L19151
Theorem. (add_SNo_minus_Le12b3)
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx + y + v w + u + zx + y + - z w + u + - v
Proof:
Proof not loaded.
End of Section SurrealAdd
Beginning of Section SurrealAbs
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L19184
Definition. We define abs_SNo to be λx ⇒ if 0 x then x else - x of type setset.
L19185
Theorem. (nonneg_abs_SNo)
∀x, 0 xabs_SNo x = x
Proof:
Proof not loaded.
L19190
Theorem. (not_nonneg_abs_SNo)
∀x, ¬ (0 x)abs_SNo x = - x
Proof:
Proof not loaded.
L19195
Theorem. (pos_abs_SNo)
∀x, 0 < xabs_SNo x = x
Proof:
Proof not loaded.
L19201
Theorem. (neg_abs_SNo)
∀x, SNo xx < 0abs_SNo x = - x
Proof:
Proof not loaded.
L19211
Theorem. (SNo_abs_SNo)
∀x, SNo xSNo (abs_SNo x)
Proof:
Proof not loaded.
L19219
Theorem. (abs_SNo_minus)
∀x, SNo xabs_SNo (- x) = abs_SNo x
Proof:
Proof not loaded.
L19251
Theorem. (abs_SNo_dist_swap)
∀x y, SNo xSNo yabs_SNo (x + - y) = abs_SNo (y + - x)
Proof:
Proof not loaded.
End of Section SurrealAbs
Beginning of Section SurrealMul
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
L19278
Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|wSNoL x SNoL y} {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|zSNoR x SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|wSNoL x SNoR y} {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|zSNoR x SNoL y})) of type setsetset.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L19289
Theorem. (mul_SNo_eq)
∀x, SNo x∀y, SNo yx * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|wSNoL x SNoL y} {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|zSNoR x SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|wSNoL x SNoR y} {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|zSNoR x SNoL y})
Proof:
Proof not loaded.
L19449
Theorem. (mul_SNo_eq_2)
∀x y, SNo xSNo y∀p : prop, (∀L R, (∀u, u L(∀q : prop, (∀w0SNoL x, ∀w1SNoL y, u = w0 * y + x * w1 + - w0 * w1q)(∀z0SNoR x, ∀z1SNoR y, u = z0 * y + x * z1 + - z0 * z1q)q))(∀w0SNoL x, ∀w1SNoL y, w0 * y + x * w1 + - w0 * w1 L)(∀z0SNoR x, ∀z1SNoR y, z0 * y + x * z1 + - z0 * z1 L)(∀u, u R(∀q : prop, (∀w0SNoL x, ∀z1SNoR y, u = w0 * y + x * z1 + - w0 * z1q)(∀z0SNoR x, ∀w1SNoL y, u = z0 * y + x * w1 + - z0 * w1q)q))(∀w0SNoL x, ∀z1SNoR y, w0 * y + x * z1 + - w0 * z1 R)(∀z0SNoR x, ∀w1SNoL y, z0 * y + x * w1 + - z0 * w1 R)x * y = SNoCut L Rp)p
Proof:
Proof not loaded.
L19565
Theorem. (mul_SNo_prop_1)
∀x, SNo x∀y, SNo y∀p : prop, (SNo (x * y)(∀uSNoL x, ∀vSNoL y, u * y + x * v < x * y + u * v)(∀uSNoR x, ∀vSNoR y, u * y + x * v < x * y + u * v)(∀uSNoL x, ∀vSNoR y, x * y + u * v < u * y + x * v)(∀uSNoR x, ∀vSNoL y, x * y + u * v < u * y + x * v)p)p
Proof:
Proof not loaded.
L20606
Theorem. (SNo_mul_SNo)
∀x y, SNo xSNo ySNo (x * y)
Proof:
Proof not loaded.
L20611
Theorem. (SNo_mul_SNo_lem)
∀x y u v, SNo xSNo ySNo uSNo vSNo (u * y + x * v + - (u * v))
Proof:
Proof not loaded.
L20625
Theorem. (SNo_mul_SNo_3)
∀x y z, SNo xSNo ySNo zSNo (x * y * z)
Proof:
Proof not loaded.
L20634
Theorem. (mul_SNo_eq_3)
∀x y, SNo xSNo y∀p : prop, (∀L R, SNoCutP L R(∀u, u L(∀q : prop, (∀w0SNoL x, ∀w1SNoL y, u = w0 * y + x * w1 + - w0 * w1q)(∀z0SNoR x, ∀z1SNoR y, u = z0 * y + x * z1 + - z0 * z1q)q))(∀w0SNoL x, ∀w1SNoL y, w0 * y + x * w1 + - w0 * w1 L)(∀z0SNoR x, ∀z1SNoR y, z0 * y + x * z1 + - z0 * z1 L)(∀u, u R(∀q : prop, (∀w0SNoL x, ∀z1SNoR y, u = w0 * y + x * z1 + - w0 * z1q)(∀z0SNoR x, ∀w1SNoL y, u = z0 * y + x * w1 + - z0 * w1q)q))(∀w0SNoL x, ∀z1SNoR y, w0 * y + x * z1 + - w0 * z1 R)(∀z0SNoR x, ∀w1SNoL y, z0 * y + x * w1 + - z0 * w1 R)x * y = SNoCut L Rp)p
Proof:
Proof not loaded.
L20875
Theorem. (mul_SNo_Lt)
∀x y u v, SNo xSNo ySNo uSNo vu < xv < yu * y + x * v < x * y + u * v
Proof:
Proof not loaded.
L21231
Theorem. (mul_SNo_Le)
∀x y u v, SNo xSNo ySNo uSNo vu xv yu * y + x * v x * y + u * v
Proof:
Proof not loaded.
L21250
Theorem. (mul_SNo_SNoL_interpolate)
∀x y, SNo xSNo y∀uSNoL (x * y), (∃vSNoL x, ∃wSNoL y, u + v * w v * y + x * w) (∃vSNoR x, ∃wSNoR y, u + v * w v * y + x * w)
Proof:
Proof not loaded.
L21432
Theorem. (mul_SNo_SNoL_interpolate_impred)
∀x y, SNo xSNo y∀uSNoL (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoL y, u + v * w v * y + x * wp)(∀vSNoR x, ∀wSNoR y, u + v * w v * y + x * wp)p
Proof:
Proof not loaded.
L21454
Theorem. (mul_SNo_SNoR_interpolate)
∀x y, SNo xSNo y∀uSNoR (x * y), (∃vSNoL x, ∃wSNoR y, v * y + x * w u + v * w) (∃vSNoR x, ∃wSNoL y, v * y + x * w u + v * w)
Proof:
Proof not loaded.
L21636
Theorem. (mul_SNo_SNoR_interpolate_impred)
∀x y, SNo xSNo y∀uSNoR (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoR y, v * y + x * w u + v * wp)(∀vSNoR x, ∀wSNoL y, v * y + x * w u + v * wp)p
Proof:
Proof not loaded.
L21658
Theorem. (mul_SNo_Subq_lem)
∀x y X Y Z W, ∀U U', (∀u, u U(∀q : prop, (∀w0X, ∀w1Y, u = w0 * y + x * w1 + - w0 * w1q)(∀z0Z, ∀z1W, u = z0 * y + x * z1 + - z0 * z1q)q))(∀w0X, ∀w1Y, w0 * y + x * w1 + - w0 * w1 U')(∀w0Z, ∀w1W, w0 * y + x * w1 + - w0 * w1 U')U U'
Proof:
Proof not loaded.
L21681
Theorem. (mul_SNo_zeroR)
∀x, SNo xx * 0 = 0
Proof:
Proof not loaded.
L21723
Theorem. (mul_SNo_oneR)
∀x, SNo xx * 1 = x
Proof:
Proof not loaded.
L21851
Theorem. (mul_SNo_com)
∀x y, SNo xSNo yx * y = y * x
Proof:
Proof not loaded.
L22010
Theorem. (mul_SNo_minus_distrL)
∀x y, SNo xSNo y(- x) * y = - x * y
Proof:
Proof not loaded.
L22402
Theorem. (mul_SNo_minus_distrR)
∀x y, SNo xSNo yx * (- y) = - (x * y)
Proof:
Proof not loaded.
L22409
Theorem. (mul_SNo_distrR)
∀x y z, SNo xSNo ySNo z(x + y) * z = x * z + y * z
Proof:
Proof not loaded.
L23722
Theorem. (mul_SNo_distrL)
∀x y z, SNo xSNo ySNo zx * (y + z) = x * y + x * z
Proof:
Proof not loaded.
Beginning of Section mul_SNo_assoc_lems
L23737
Variable M : setsetset
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term M.
L23739
Hypothesis SNo_M : ∀x y, SNo xSNo ySNo (x * y)
L23740
Hypothesis DL : ∀x y z, SNo xSNo ySNo zx * (y + z) = x * y + x * z
L23741
Hypothesis DR : ∀x y z, SNo xSNo ySNo z(x + y) * z = x * z + y * z
L23742
Hypothesis IL : ∀x y, SNo xSNo y∀uSNoL (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoL y, u + v * w v * y + x * wp)(∀vSNoR x, ∀wSNoR y, u + v * w v * y + x * wp)p
L23747
Hypothesis IR : ∀x y, SNo xSNo y∀uSNoR (x * y), ∀p : prop, (∀vSNoL x, ∀wSNoR y, v * y + x * w u + v * wp)(∀vSNoR x, ∀wSNoL y, v * y + x * w u + v * wp)p
L23752
Hypothesis M_Lt : ∀x y u v, SNo xSNo ySNo uSNo vu < xv < yu * y + x * v < x * y + u * v
L23754
Hypothesis M_Le : ∀x y u v, SNo xSNo ySNo uSNo vu xv yu * y + x * v x * y + u * v
L23756
Theorem. (mul_SNo_assoc_lem1)
∀x y z, SNo xSNo ySNo z(∀uSNoS_ (SNoLev x), u * (y * z) = (u * y) * z)(∀vSNoS_ (SNoLev y), x * (v * z) = (x * v) * z)(∀wSNoS_ (SNoLev z), x * (y * w) = (x * y) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), u * (v * z) = (u * v) * z)(∀uSNoS_ (SNoLev x), ∀wSNoS_ (SNoLev z), u * (y * w) = (u * y) * w)(∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), x * (v * w) = (x * v) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), u * (v * w) = (u * v) * w)∀L, (∀uL, ∀q : prop, (∀vSNoL x, ∀wSNoL (y * z), u = v * (y * z) + x * w + - v * wq)(∀vSNoR x, ∀wSNoR (y * z), u = v * (y * z) + x * w + - v * wq)q)∀uL, u < (x * y) * z
Proof:
Proof not loaded.
L24216
Theorem. (mul_SNo_assoc_lem2)
∀x y z, SNo xSNo ySNo z(∀uSNoS_ (SNoLev x), u * (y * z) = (u * y) * z)(∀vSNoS_ (SNoLev y), x * (v * z) = (x * v) * z)(∀wSNoS_ (SNoLev z), x * (y * w) = (x * y) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), u * (v * z) = (u * v) * z)(∀uSNoS_ (SNoLev x), ∀wSNoS_ (SNoLev z), u * (y * w) = (u * y) * w)(∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), x * (v * w) = (x * v) * w)(∀uSNoS_ (SNoLev x), ∀vSNoS_ (SNoLev y), ∀wSNoS_ (SNoLev z), u * (v * w) = (u * v) * w)∀R, (∀uR, ∀q : prop, (∀vSNoL x, ∀wSNoR (y * z), u = v * (y * z) + x * w + - v * wq)(∀vSNoR x, ∀wSNoL (y * z), u = v * (y * z) + x * w + - v * wq)q)∀uR, (x * y) * z < u
Proof:
Proof not loaded.
End of Section mul_SNo_assoc_lems
L24701
Theorem. (mul_SNo_assoc)
∀x y z, SNo xSNo ySNo zx * (y * z) = (x * y) * z
Proof:
Proof not loaded.
L24916
Theorem. (mul_nat_mul_SNo)
∀n mω, mul_nat n m = n * m
Proof:
Proof not loaded.
L24958
Theorem. (mul_SNo_In_omega)
∀n mω, n * m ω
Proof:
Proof not loaded.
L24964
Theorem. (mul_SNo_zeroL)
∀x, SNo x0 * x = 0
Proof:
Proof not loaded.
L24970
Theorem. (mul_SNo_oneL)
∀x, SNo x1 * x = x
Proof:
Proof not loaded.
L24976
Theorem. (mul_SNo_rotate_3_1)
∀x y z, SNo xSNo ySNo zx * y * z = z * x * y
Proof:
Proof not loaded.
L24990
Theorem. (pos_mul_SNo_Lt)
∀x y z, SNo x0 < xSNo ySNo zy < zx * y < x * z
Proof:
Proof not loaded.
L25008
Theorem. (nonneg_mul_SNo_Le)
∀x y z, SNo x0 xSNo ySNo zy zx * y x * z
Proof:
Proof not loaded.
L25026
Theorem. (neg_mul_SNo_Lt)
∀x y z, SNo xx < 0SNo ySNo zz < yx * y < x * z
Proof:
Proof not loaded.
L25044
Theorem. (pos_mul_SNo_Lt')
∀x y z, SNo xSNo ySNo z0 < zx < yx * z < y * z
Proof:
Proof not loaded.
L25051
Theorem. (mul_SNo_Lt1_pos_Lt)
∀x y, SNo xSNo yx < 10 < yx * y < y
Proof:
Proof not loaded.
L25058
Theorem. (nonneg_mul_SNo_Le')
∀x y z, SNo xSNo ySNo z0 zx yx * z y * z
Proof:
Proof not loaded.
L25065
Theorem. (mul_SNo_Le1_nonneg_Le)
∀x y, SNo xSNo yx 10 yx * y y
Proof:
Proof not loaded.
L25072
Theorem. (pos_mul_SNo_Lt2)
∀x y z w, SNo xSNo ySNo zSNo w0 < x0 < yx < zy < wx * y < z * w
Proof:
Proof not loaded.
L25087
Theorem. (nonneg_mul_SNo_Le2)
∀x y z w, SNo xSNo ySNo zSNo w0 x0 yx zy wx * y z * w
Proof:
Proof not loaded.
L25102
Theorem. (mul_SNo_pos_pos)
∀x y, SNo xSNo y0 < x0 < y0 < x * y
Proof:
Proof not loaded.
L25118
Theorem. (mul_SNo_pos_neg)
∀x y, SNo xSNo y0 < xy < 0x * y < 0
Proof:
Proof not loaded.
L25132
Theorem. (mul_SNo_neg_pos)
∀x y, SNo xSNo yx < 00 < yx * y < 0
Proof:
Proof not loaded.
L25146
Theorem. (mul_SNo_neg_neg)
∀x y, SNo xSNo yx < 0y < 00 < x * y
Proof:
Proof not loaded.
L25162
Theorem. (mul_SNo_nonneg_nonneg)
∀x y, SNo xSNo y0 x0 y0 x * y
Proof:
Proof not loaded.
L25178
Theorem. (mul_SNo_nonpos_pos)
∀x y, SNo xSNo yx 00 < yx * y 0
Proof:
Proof not loaded.
L25195
Theorem. (mul_SNo_nonpos_neg)
∀x y, SNo xSNo yx 0y < 00 x * y
Proof:
Proof not loaded.
L25212
Theorem. (nonpos_mul_SNo_Le)
∀x y z, SNo xx 0SNo ySNo zz yx * y x * z
Proof:
Proof not loaded.
L25240
Theorem. (SNo_zero_or_sqr_pos)
∀x, SNo xx = 0 0 < x * x
Proof:
Proof not loaded.
L25258
Theorem. (SNo_pos_sqr_uniq)
∀x y, SNo xSNo y0 < x0 < yx * x = y * yx = y
Proof:
Proof not loaded.
L25277
Theorem. (SNo_nonneg_sqr_uniq)
∀x y, SNo xSNo y0 x0 yx * x = y * yx = y
Proof:
Proof not loaded.
L25302
Theorem. (SNo_foil)
∀x y z w, SNo xSNo ySNo zSNo w(x + y) * (z + w) = x * z + x * w + y * z + y * w
Proof:
Proof not loaded.
L25328
Theorem. (mul_SNo_minus_minus)
∀x y, SNo xSNo y(- x) * (- y) = x * y
Proof:
Proof not loaded.
L25337
Theorem. (mul_SNo_com_3_0_1)
∀x y z, SNo xSNo ySNo zx * y * z = y * x * z
Proof:
Proof not loaded.
L25347
Theorem. (mul_SNo_com_3b_1_2)
∀x y z, SNo xSNo ySNo z(x * y) * z = (x * z) * y
Proof:
Proof not loaded.
L25357
Theorem. (mul_SNo_com_4_inner_mid)
∀x y z w, SNo xSNo ySNo zSNo w(x * y) * (z * w) = (x * z) * (y * w)
Proof:
Proof not loaded.
L25369
Theorem. (SNo_foil_mm)
∀x y z w, SNo xSNo ySNo zSNo w(x + - y) * (z + - w) = x * z + - x * w + - y * z + y * w
Proof:
Proof not loaded.
L25384
Theorem. (mul_SNo_nonzero_cancel)
∀x y z, SNo xx 0SNo ySNo zx * y = x * zy = z
Proof:
Proof not loaded.
L25420
Theorem. (mul_SNoCutP_lem)
∀Lx Rx Ly Ry x y, SNoCutP Lx RxSNoCutP Ly Ryx = SNoCut Lx Rxy = SNoCut Ly RySNoCutP ({w 0 * y + x * w 1 + - w 0 * w 1|wLx Ly} {z 0 * y + x * z 1 + - z 0 * z 1|zRx Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|wLx Ry} {z 0 * y + x * z 1 + - z 0 * z 1|zRx Ly}) x * y = SNoCut ({w 0 * y + x * w 1 + - w 0 * w 1|wLx Ly} {z 0 * y + x * z 1 + - z 0 * z 1|zRx Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|wLx Ry} {z 0 * y + x * z 1 + - z 0 * z 1|zRx Ly}) ∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀uLxLy', ∀p : prop, (∀wLx, ∀w'Ly, SNo wSNo w'w < xw' < yu = w * y + x * w' + - w * w'p)p)(∀wLx, ∀w'Ly, w * y + x * w' + - w * w' LxLy')(∀uRxRy', ∀p : prop, (∀zRx, ∀z'Ry, SNo zSNo z'x < zy < z'u = z * y + x * z' + - z * z'p)p)(∀zRx, ∀z'Ry, z * y + x * z' + - z * z' RxRy')(∀uLxRy', ∀p : prop, (∀wLx, ∀zRy, SNo wSNo zw < xy < zu = w * y + x * z + - w * zp)p)(∀wLx, ∀zRy, w * y + x * z + - w * z LxRy')(∀uRxLy', ∀p : prop, (∀zRx, ∀wLy, SNo zSNo wx < zw < yu = z * y + x * w + - z * wp)p)(∀zRx, ∀wLy, z * y + x * w + - z * w RxLy')SNoCutP (LxLy' RxRy') (LxRy' RxLy')x * y = SNoCut (LxLy' RxRy') (LxRy' RxLy')q)q
Proof:
Proof not loaded.
L26713
Theorem. (mul_SNoCut_abs)
∀Lx Rx Ly Ry x y, SNoCutP Lx RxSNoCutP Ly Ryx = SNoCut Lx Rxy = SNoCut Ly Ry∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀uLxLy', ∀p : prop, (∀wLx, ∀w'Ly, SNo wSNo w'w < xw' < yu = w * y + x * w' + - w * w'p)p)(∀wLx, ∀w'Ly, w * y + x * w' + - w * w' LxLy')(∀uRxRy', ∀p : prop, (∀zRx, ∀z'Ry, SNo zSNo z'x < zy < z'u = z * y + x * z' + - z * z'p)p)(∀zRx, ∀z'Ry, z * y + x * z' + - z * z' RxRy')(∀uLxRy', ∀p : prop, (∀wLx, ∀zRy, SNo wSNo zw < xy < zu = w * y + x * z + - w * zp)p)(∀wLx, ∀zRy, w * y + x * z + - w * z LxRy')(∀uRxLy', ∀p : prop, (∀zRx, ∀wLy, SNo zSNo wx < zw < yu = z * y + x * w + - z * wp)p)(∀zRx, ∀wLy, z * y + x * w + - z * w RxLy')SNoCutP (LxLy' RxRy') (LxRy' RxLy')x * y = SNoCut (LxLy' RxRy') (LxRy' RxLy')q)q
Proof:
Proof not loaded.
L26738
Theorem. (mul_SNo_SNoCut_SNoL_interpolate)
∀Lx Rx Ly Ry, SNoCutP Lx RxSNoCutP Ly Ry∀x y, x = SNoCut Lx Rxy = SNoCut Ly Ry∀uSNoL (x * y), (∃vLx, ∃wLy, u + v * w v * y + x * w) (∃vRx, ∃wRy, u + v * w v * y + x * w)
Proof:
Proof not loaded.
L26978
Theorem. (mul_SNo_SNoCut_SNoL_interpolate_impred)
∀Lx Rx Ly Ry, SNoCutP Lx RxSNoCutP Ly Ry∀x y, x = SNoCut Lx Rxy = SNoCut Ly Ry∀uSNoL (x * y), ∀p : prop, (∀vLx, ∀wLy, u + v * w v * y + x * wp)(∀vRx, ∀wRy, u + v * w v * y + x * wp)p
Proof:
Proof not loaded.
L27004
Theorem. (mul_SNo_SNoCut_SNoR_interpolate)
∀Lx Rx Ly Ry, SNoCutP Lx RxSNoCutP Ly Ry∀x y, x = SNoCut Lx Rxy = SNoCut Ly Ry∀uSNoR (x * y), (∃vLx, ∃wRy, v * y + x * w u + v * w) (∃vRx, ∃wLy, v * y + x * w u + v * w)
Proof:
Proof not loaded.
L27244
Theorem. (mul_SNo_SNoCut_SNoR_interpolate_impred)
∀Lx Rx Ly Ry, SNoCutP Lx RxSNoCutP Ly Ry∀x y, x = SNoCut Lx Rxy = SNoCut Ly Ry∀uSNoR (x * y), ∀p : prop, (∀vLx, ∀wRy, v * y + x * w u + v * wp)(∀vRx, ∀wLy, v * y + x * w u + v * wp)p
Proof:
Proof not loaded.
L27270
Theorem. (nonpos_nonneg_0)
∀m nω, m = - nm = 0 n = 0
Proof:
Proof not loaded.
L27302
Theorem. (mul_minus_SNo_distrR)
∀x y, SNo xSNo yx * (- y) = - (x * y)
Proof:
Proof not loaded.
End of Section SurrealMul
Beginning of Section Int
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L27322
Definition. We define int to be ω {- n|nω} of type set.
L27324
Theorem. (int_SNo_cases)
∀p : setprop, (∀nω, p n)(∀nω, p (- n))∀xint, p x
Proof:
Proof not loaded.
L27338
Theorem. (int_3_cases)
∀nint, ∀p : prop, (∀mω, n = - ordsucc mp)(n = 0p)(∀mω, n = ordsucc mp)p
Proof:
Proof not loaded.
L27367
Theorem. (int_SNo)
∀xint, SNo x
Proof:
Proof not loaded.
L27375
Proof:
Proof not loaded.
L27382
Theorem. (int_minus_SNo_omega)
∀nω, - n int
Proof:
Proof not loaded.
L27390
Theorem. (int_add_SNo_lem)
∀nω, ∀m, nat_p m- n + m int
Proof:
Proof not loaded.
L27446
Theorem. (int_add_SNo)
∀x yint, x + y int
Proof:
Proof not loaded.
L27475
Theorem. (int_minus_SNo)
∀xint, - x int
Proof:
Proof not loaded.
L27484
Theorem. (int_mul_SNo)
∀x yint, x * y int
Proof:
Proof not loaded.
L27553
Theorem. (nonneg_int_nat_p)
∀nint, 0 nnat_p n
Proof:
Proof not loaded.
End of Section Int
Beginning of Section BezoutAndGCD
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L27591
Theorem. (quotient_remainder_nat)
∀nω {0}, ∀m, nat_p m∃qω, ∃rn, m = q * n + r
Proof:
Proof not loaded.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L27672
Theorem. (mul_SNo_nonpos_nonneg)
∀x y, SNo xSNo yx 00 yx * y 0
Proof:
Proof not loaded.
L27683
Theorem. (ordinal_0_In_ordsucc)
∀alpha, ordinal alpha0 ordsucc alpha
Proof:
Proof not loaded.
L27692
Theorem. (ordinal_ordsucc_pos)
∀alpha, ordinal alpha0 < ordsucc alpha
Proof:
Proof not loaded.
L27699
Theorem. (quotient_remainder_int)
∀nω {0}, ∀mint, ∃qint, ∃rn, m = q * n + r
Proof:
Proof not loaded.
L27842
Definition. We define divides_int to be λm n ⇒ m int n int ∃kint, m * k = n of type setsetprop.
L27844
Proof:
Proof not loaded.
L27859
Proof:
Proof not loaded.
L27876
Theorem. (divides_int_add_SNo)
∀m n k, divides_int m ndivides_int m kdivides_int m (n + k)
Proof:
Proof not loaded.
L27913
Theorem. (divides_int_mul_SNo)
∀m n m' n', divides_int m m'divides_int n n'divides_int (m * n) (m' * n')
Proof:
Proof not loaded.
L27951
Theorem. (divides_nat_divides_int)
∀m n, divides_nat m ndivides_int m n
Proof:
Proof not loaded.
L27973
Proof:
Proof not loaded.
L28027
Theorem. (divides_int_minus_SNo)
∀m n, divides_int m ndivides_int m (- n)
Proof:
Proof not loaded.
L28051
Theorem. (divides_int_mul_SNo_L)
∀m n, ∀kint, divides_int m ndivides_int m (n * k)
Proof:
Proof not loaded.
L28081
Theorem. (divides_int_mul_SNo_R)
∀m n, ∀kint, divides_int m ndivides_int m (k * n)
Proof:
Proof not loaded.
L28094
Proof:
Proof not loaded.
L28106
Theorem. (divides_int_pos_Le)
∀m n, divides_int m n0 < nm n
Proof:
Proof not loaded.
L28189
Definition. We define gcd_reln to be λm n d ⇒ divides_int d m divides_int d n ∀d', divides_int d' mdivides_int d' nd' d of type setsetsetprop.
L28191
Theorem. (gcd_reln_uniq)
∀a b c d, gcd_reln a b cgcd_reln a b dc = d
Proof:
Proof not loaded.
L28218
Definition. We define int_lin_comb to be λa b c ⇒ a int b int c int ∃m nint, m * a + n * b = c of type setsetsetprop.
L28220
Theorem. (int_lin_comb_I)
∀a b cint, (∃m nint, m * a + n * b = c)int_lin_comb a b c
Proof:
Proof not loaded.
L28231
Theorem. (int_lin_comb_E)
∀a b c, int_lin_comb a b c∀p : prop, (a intb intc int∀m nint, m * a + n * b = cp)p
Proof:
Proof not loaded.
L28247
Theorem. (int_lin_comb_E1)
∀a b c, int_lin_comb a b ca int
Proof:
Proof not loaded.
L28253
Theorem. (int_lin_comb_E2)
∀a b c, int_lin_comb a b cb int
Proof:
Proof not loaded.
L28259
Theorem. (int_lin_comb_E3)
∀a b c, int_lin_comb a b cc int
Proof:
Proof not loaded.
L28265
Theorem. (int_lin_comb_E4)
∀a b c, int_lin_comb a b c∀p : prop, (∀m nint, m * a + n * b = cp)p
Proof:
Proof not loaded.
L28274
Theorem. (least_pos_int_lin_comb_ex)
∀a bint, ¬ (a = 0 b = 0)∃c, int_lin_comb a b c 0 < c ∀c', int_lin_comb a b c'0 < c'c c'
Proof:
Proof not loaded.
L28474
Theorem. (int_lin_comb_sym)
∀a b d, int_lin_comb a b dint_lin_comb b a d
Proof:
Proof not loaded.
L28495
Theorem. (least_pos_int_lin_comb_divides_int)
∀a b d, int_lin_comb a b d0 < d(∀c, int_lin_comb a b c0 < cd c)divides_int d a
Proof:
Proof not loaded.
L28653
Theorem. (least_pos_int_lin_comb_gcd)
∀a b d, int_lin_comb a b d0 < d(∀c, int_lin_comb a b c0 < cd c)gcd_reln a b d
Proof:
Proof not loaded.
L28733
Theorem. (BezoutThm)
∀a bint, ¬ (a = 0 b = 0)∀d, gcd_reln a b d int_lin_comb a b d 0 < d ∀d', int_lin_comb a b d'0 < d'd d'
Proof:
Proof not loaded.
L28764
Theorem. (gcd_id)
∀mω {0}, gcd_reln m m m
Proof:
Proof not loaded.
L28863
Theorem. (gcd_0)
Proof:
Proof not loaded.
L28890
Theorem. (gcd_sym)
∀m n d, gcd_reln m n dgcd_reln n m d
Proof:
Proof not loaded.
L28905
Theorem. (gcd_minus)
∀m n d, gcd_reln m n dgcd_reln m (- n) d
Proof:
Proof not loaded.
L28928
Theorem. (euclidean_algorithm_prop_1)
∀m n d, n intgcd_reln m (n + - m) dgcd_reln m n d
Proof:
Proof not loaded.
L28964
Theorem. (euclidean_algorithm)
(∀mω {0}, gcd_reln m m m) (∀mω {0}, gcd_reln 0 m m) (∀mω {0}, gcd_reln m 0 m) (∀m nω, m < n∀d, gcd_reln m (n + - m) dgcd_reln m n d) (∀m nω, n < m∀d, gcd_reln n m dgcd_reln m n d) (∀mω, ∀nint, n < 0∀d, gcd_reln m (- n) dgcd_reln m n d) (∀m nint, m < 0∀d, gcd_reln (- m) n dgcd_reln m n d)
Proof:
Proof not loaded.
L29011
Theorem. (Euclid_lemma)
∀p, prime_nat p∀a bint, divides_int p (a * b)divides_int p a divides_int p b
Proof:
Proof not loaded.
End of Section BezoutAndGCD
Beginning of Section PrimeFactorization
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L29133
Proof:
Proof not loaded.
L29157
Definition. We define Pi_SNo to be λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i) n of type (setset)setset.
L29160
Theorem. (Pi_SNo_0)
∀f : setset, Pi_SNo f 0 = 1
Proof:
Proof not loaded.
L29165
Theorem. (Pi_SNo_S)
∀f : setset, ∀n, nat_p nPi_SNo f (ordsucc n) = Pi_SNo f n * f n
Proof:
Proof not loaded.
L29171
Theorem. (Pi_SNo_In_omega)
∀f : setset, ∀n, nat_p n(∀in, f i ω)Pi_SNo f n ω
Proof:
Proof not loaded.
L29196
Theorem. (Pi_SNo_In_int)
∀f : setset, ∀n, nat_p n(∀in, f i int)Pi_SNo f n int
Proof:
Proof not loaded.
L29221
Theorem. (divides_int_prime_nat_eq)
∀p q, prime_nat pprime_nat qdivides_int p qp = q
Proof:
Proof not loaded.
L29246
Theorem. (Euclid_lemma_Pi_SNo)
∀f : setset, ∀p, prime_nat p∀n, nat_p n(∀in, f i int)divides_int p (Pi_SNo f n)∃in, divides_int p (f i)
Proof:
Proof not loaded.
L29287
Theorem. (divides_nat_mul_SNo_R)
∀m nω, divides_nat m (m * n)
Proof:
Proof not loaded.
L29301
Theorem. (divides_nat_mul_SNo_L)
∀m nω, divides_nat n (m * n)
Proof:
Proof not loaded.
L29308
Theorem. (Pi_SNo_divides)
∀f : setset, ∀n, nat_p n(∀in, f i ω)(∀in, divides_nat (f i) (Pi_SNo f n))
Proof:
Proof not loaded.
L29340
Definition. We define nonincrfinseq to be λA n f ⇒ ∀in, A (f i) ∀ji, f i f j of type (setprop)set(setset)prop.
L29342
Theorem. (Pi_SNo_eq)
∀f g : setset, ∀m, nat_p m(∀im, f i = g i)Pi_SNo f m = Pi_SNo g m
Proof:
Proof not loaded.
L29365
Theorem. (prime_factorization_ex_uniq)
∀n, nat_p n0 n∃kω, ∃f : setset, nonincrfinseq prime_nat k f Pi_SNo f k = n ∀k'ω, ∀f' : setset, nonincrfinseq prime_nat k' f'Pi_SNo f' k' = nk' = k ∀ik, f' i = f i
Proof:
Proof not loaded.
End of Section PrimeFactorization
Beginning of Section SurrealExp
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L29865
Definition. We define exp_SNo_nat to be λn m : setnat_primrec 1 (λ_ r ⇒ n * r) m of type setsetset.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L29867
Theorem. (exp_SNo_nat_0)
∀x, SNo xx ^ 0 = 1
Proof:
Proof not loaded.
L29872
Theorem. (exp_SNo_nat_S)
∀x, SNo x∀n, nat_p nx ^ (ordsucc n) = x * x ^ n
Proof:
Proof not loaded.
L29877
Theorem. (exp_SNo_nat_1)
∀x, SNo xx ^ 1 = x
Proof:
Proof not loaded.
L29886
Theorem. (SNo_exp_SNo_nat)
∀x, SNo x∀n, nat_p nSNo (x ^ n)
Proof:
Proof not loaded.
L29896
Theorem. (nat_exp_SNo_nat)
∀x, nat_p x∀n, nat_p nnat_p (x ^ n)
Proof:
Proof not loaded.
L29911
Theorem. (eps_ordsucc_half_add)
∀n, nat_p neps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n
Proof:
Proof not loaded.
L30071
Theorem. (eps_1_half_eq1)
Proof:
Proof not loaded.
L30077
Theorem. (eps_1_half_eq2)
Proof:
Proof not loaded.
L30086
Theorem. (double_eps_1)
∀x y z, SNo xSNo ySNo zx + x = y + zx = eps_ 1 * (y + z)
Proof:
Proof not loaded.
L30107
Theorem. (exp_SNo_1_bd)
∀x, SNo x1 x∀n, nat_p n1 x ^ n
Proof:
Proof not loaded.
L30127
Theorem. (exp_SNo_2_bd)
∀n, nat_p nn < 2 ^ n
Proof:
Proof not loaded.
L30161
Theorem. (mul_SNo_eps_power_2)
∀n, nat_p neps_ n * 2 ^ n = 1
Proof:
Proof not loaded.
L30186
Theorem. (eps_bd_1)
∀nω, eps_ n 1
Proof:
Proof not loaded.
L30204
Theorem. (mul_SNo_eps_power_2')
∀n, nat_p n2 ^ n * eps_ n = 1
Proof:
Proof not loaded.
L30213
Theorem. (exp_SNo_nat_mul_add)
∀x, SNo x∀m, nat_p m∀n, nat_p nx ^ m * x ^ n = x ^ (m + n)
Proof:
Proof not loaded.
L30245
Theorem. (exp_SNo_nat_mul_add')
∀x, SNo x∀m nω, x ^ m * x ^ n = x ^ (m + n)
Proof:
Proof not loaded.
L30250
Theorem. (exp_SNo_nat_pos)
∀x, SNo x0 < x∀n, nat_p n0 < x ^ n
Proof:
Proof not loaded.
L30264
Theorem. (mul_SNo_eps_eps_add_SNo)
∀m nω, eps_ m * eps_ n = eps_ (m + n)
Proof:
Proof not loaded.
L30314
Theorem. (SNoS_omega_Lev_equip)
∀n, nat_p nequip {xSNoS_ ω|SNoLev x = n} (2 ^ n)
Proof:
Proof not loaded.
L30711
Theorem. (SNoS_finite)
Proof:
Proof not loaded.
L30763
Proof:
Proof not loaded.
L30783
Proof:
Proof not loaded.
End of Section SurrealExp
Beginning of Section SNoMaxMin
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L30816
Definition. We define SNo_max_of to be λX x ⇒ x X SNo x ∀yX, SNo yy x of type setsetprop.
L30817
Definition. We define SNo_min_of to be λX x ⇒ x X SNo x ∀yX, SNo yx y of type setsetprop.
L30818
Theorem. (minus_SNo_max_min)
∀X y, (∀xX, SNo x)SNo_max_of X ySNo_min_of {- x|xX} (- y)
Proof:
Proof not loaded.
L30839
Theorem. (minus_SNo_max_min')
∀X y, (∀xX, SNo x)SNo_max_of {- x|xX} ySNo_min_of X (- y)
Proof:
Proof not loaded.
L30858
Theorem. (minus_SNo_min_max)
∀X y, (∀xX, SNo x)SNo_min_of X ySNo_max_of {- x|xX} (- y)
Proof:
Proof not loaded.
L30879
Theorem. (double_SNo_max_1)
∀x y, SNo xSNo_max_of (SNoL x) y∀z, SNo zx < zy + z < x + x∃wSNoR z, y + w = x + x
Proof:
Proof not loaded.
L31071
Theorem. (double_SNo_min_1)
∀x y, SNo xSNo_min_of (SNoR x) y∀z, SNo zz < xx + x < y + z∃wSNoL z, y + w = x + x
Proof:
Proof not loaded.
L31141
Theorem. (finite_max_exists)
∀X, (∀xX, SNo x)finite XX 0∃x, SNo_max_of X x
Proof:
Proof not loaded.
L31287
Theorem. (finite_min_exists)
∀X, (∀xX, SNo x)finite XX 0∃x, SNo_min_of X x
Proof:
Proof not loaded.
L31355
Proof:
Proof not loaded.
L31370
Proof:
Proof not loaded.
End of Section SNoMaxMin
Beginning of Section DiadicRationals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L31396
Proof:
Proof not loaded.
L31420
Definition. We define diadic_rational_p to be λx ⇒ ∃kω, ∃mint, x = eps_ k * m of type setprop.
L31422
Proof:
Proof not loaded.
L31447
Proof:
Proof not loaded.
L31458
Proof:
Proof not loaded.
L31463
Proof:
Proof not loaded.
L31475
Proof:
Proof not loaded.
L31501
Proof:
Proof not loaded.
L31543
Proof:
Proof not loaded.
L31621
Theorem. (SNoS_omega_diadic_rational_p_lem)
∀n, nat_p n∀x, SNo xSNoLev x = ndiadic_rational_p x
Proof:
Proof not loaded.
L31826
Proof:
Proof not loaded.
L31839
Theorem. (mul_SNo_SNoS_omega)
∀x ySNoS_ ω, x * y SNoS_ ω
Proof:
Proof not loaded.
End of Section DiadicRationals
Beginning of Section SurrealDiv
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L31860
Definition. We define SNoL_pos to be λx ⇒ {wSNoL x|0 < w} of type setset.
L31861
Theorem. (SNo_recip_pos_pos)
∀x xi, SNo xSNo xi0 < xx * xi = 10 < xi
Proof:
Proof not loaded.
L31883
Theorem. (SNo_recip_lem1)
∀x x' x'i y y', SNo x0 < xx' SNoL_pos xSNo x'ix' * x'i = 1SNo yx * y < 1SNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i1 < x * y'
Proof:
Proof not loaded.
L31929
Theorem. (SNo_recip_lem2)
∀x x' x'i y y', SNo x0 < xx' SNoL_pos xSNo x'ix' * x'i = 1SNo y1 < x * ySNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'ix * y' < 1
Proof:
Proof not loaded.
L31975
Theorem. (SNo_recip_lem3)
∀x x' x'i y y', SNo x0 < xx' SNoR xSNo x'ix' * x'i = 1SNo yx * y < 1SNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'ix * y' < 1
Proof:
Proof not loaded.
L32020
Theorem. (SNo_recip_lem4)
∀x x' x'i y y', SNo x0 < xx' SNoR xSNo x'ix' * x'i = 1SNo y1 < x * ySNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i1 < x * y'
Proof:
Proof not loaded.
L32065
Definition. We define SNo_recipauxset to be λY x X g ⇒ yY{(1 + (x' + - x) * y) * g x'|x'X} of type setsetset(setset)set.
L32067
Theorem. (SNo_recipauxset_I)
∀Y x X, ∀g : setset, ∀yY, ∀x'X, (1 + (x' + - x) * y) * g x' SNo_recipauxset Y x X g
Proof:
Proof not loaded.
L32076
Theorem. (SNo_recipauxset_E)
∀Y x X, ∀g : setset, ∀zSNo_recipauxset Y x X g, ∀p : prop, (∀yY, ∀x'X, z = (1 + (x' + - x) * y) * g x'p)p
Proof:
Proof not loaded.
L32088
Theorem. (SNo_recipauxset_ext)
∀Y x X, ∀g h : setset, (∀x'X, g x' = h x')SNo_recipauxset Y x X g = SNo_recipauxset Y x X h
Proof:
Proof not loaded.
L32102
Definition. We define SNo_recipaux to be λx g ⇒ nat_primrec ({0},0) (λk p ⇒ (p 0 SNo_recipauxset (p 0) x (SNoR x) g SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 SNo_recipauxset (p 0) x (SNoL_pos x) g SNo_recipauxset (p 1) x (SNoR x) g)) of type set(setset)setset.
L32110
Theorem. (SNo_recipaux_0)
∀x, ∀g : setset, SNo_recipaux x g 0 = ({0},0)
Proof:
Proof not loaded.
L32119
Theorem. (SNo_recipaux_S)
∀x, ∀g : setset, ∀n, nat_p nSNo_recipaux x g (ordsucc n) = (SNo_recipaux x g n 0 SNo_recipauxset (SNo_recipaux x g n 0) x (SNoR x) g SNo_recipauxset (SNo_recipaux x g n 1) x (SNoL_pos x) g,SNo_recipaux x g n 1 SNo_recipauxset (SNo_recipaux x g n 0) x (SNoL_pos x) g SNo_recipauxset (SNo_recipaux x g n 1) x (SNoR x) g)
Proof:
Proof not loaded.
L32133
Theorem. (SNo_recipaux_lem1)
∀x, SNo x0 < x∀g : setset, (∀x'SNoS_ (SNoLev x), 0 < x'SNo (g x') x' * g x' = 1)∀k, nat_p k(∀ySNo_recipaux x g k 0, SNo y x * y < 1) (∀ySNo_recipaux x g k 1, SNo y 1 < x * y)
Proof:
Proof not loaded.
L32376
Theorem. (SNo_recipaux_lem2)
∀x, SNo x0 < x∀g : setset, (∀x'SNoS_ (SNoLev x), 0 < x'SNo (g x') x' * g x' = 1)SNoCutP (kωSNo_recipaux x g k 0) (kωSNo_recipaux x g k 1)
Proof:
Proof not loaded.
L32437
Theorem. (SNo_recipaux_ext)
∀x, SNo x∀g h : setset, (∀x'SNoS_ (SNoLev x), g x' = h x')∀k, nat_p kSNo_recipaux x g k = SNo_recipaux x h k
Proof:
Proof not loaded.
Beginning of Section recip_SNo_pos
L32527
Let G : set(setset)setλx g ⇒ SNoCut (kωSNo_recipaux x g k 0) (kωSNo_recipaux x g k 1)
L32528
Definition. We define recip_SNo_pos to be SNo_rec_i G of type setset.
L32529
Theorem. (recip_SNo_pos_eq)
∀x, SNo xrecip_SNo_pos x = G x recip_SNo_pos
Proof:
Proof not loaded.
L32554
Theorem. (recip_SNo_pos_prop1)
∀x, SNo x0 < xSNo (recip_SNo_pos x) x * recip_SNo_pos x = 1
Proof:
Proof not loaded.
L33177
Theorem. (SNo_recip_SNo_pos)
∀x, SNo x0 < xSNo (recip_SNo_pos x)
Proof:
Proof not loaded.
L33182
Theorem. (recip_SNo_pos_invR)
∀x, SNo x0 < xx * recip_SNo_pos x = 1
Proof:
Proof not loaded.
L33187
Theorem. (recip_SNo_pos_is_pos)
∀x, SNo x0 < x0 < recip_SNo_pos x
Proof:
Proof not loaded.
L33212
Theorem. (recip_SNo_pos_invol)
∀x, SNo x0 < xrecip_SNo_pos (recip_SNo_pos x) = x
Proof:
Proof not loaded.
L33235
Theorem. (recip_SNo_pos_eps_)
∀n, nat_p nrecip_SNo_pos (eps_ n) = 2 ^ n
Proof:
Proof not loaded.
L33256
Theorem. (recip_SNo_pos_pow_2)
∀n, nat_p nrecip_SNo_pos (2 ^ n) = eps_ n
Proof:
Proof not loaded.
L33262
Proof:
Proof not loaded.
End of Section recip_SNo_pos
L33269
Definition. We define recip_SNo to be λx ⇒ if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0 of type setset.
L33270
Theorem. (recip_SNo_poscase)
∀x, 0 < xrecip_SNo x = recip_SNo_pos x
Proof:
Proof not loaded.
L33275
Theorem. (recip_SNo_negcase)
∀x, SNo xx < 0recip_SNo x = - recip_SNo_pos (- x)
Proof:
Proof not loaded.
L33287
Proof:
Proof not loaded.
L33294
Theorem. (SNo_recip_SNo)
∀x, SNo xSNo (recip_SNo x)
Proof:
Proof not loaded.
L33314
Theorem. (recip_SNo_invR)
∀x, SNo xx 0x * recip_SNo x = 1
Proof:
Proof not loaded.
L33336
Theorem. (recip_SNo_invL)
∀x, SNo xx 0recip_SNo x * x = 1
Proof:
Proof not loaded.
L33343
Theorem. (mul_SNo_nonzero_cancel_L)
∀x y z, SNo xx 0SNo ySNo zx * y = x * zy = z
Proof:
Proof not loaded.
L33359
Theorem. (recip_SNo_pow_2)
∀n, nat_p nrecip_SNo (2 ^ n) = eps_ n
Proof:
Proof not loaded.
L33367
Theorem. (recip_SNo_of_pos_is_pos)
∀x, SNo x0 < x0 < recip_SNo x
Proof:
Proof not loaded.
L33373
Definition. We define div_SNo to be λx y ⇒ x * recip_SNo y of type setsetset.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
L33377
Theorem. (SNo_div_SNo)
∀x y, SNo xSNo ySNo (x :/: y)
Proof:
Proof not loaded.
L33383
Theorem. (div_SNo_0_num)
∀x, SNo x0 :/: x = 0
Proof:
Proof not loaded.
L33388
Theorem. (div_SNo_0_denum)
∀x, SNo xx :/: 0 = 0
Proof:
Proof not loaded.
L33395
Theorem. (mul_div_SNo_invL)
∀x y, SNo xSNo yy 0(x :/: y) * y = x
Proof:
Proof not loaded.
L33405
Theorem. (mul_div_SNo_invR)
∀x y, SNo xSNo yy 0y * (x :/: y) = x
Proof:
Proof not loaded.
L33411
Theorem. (mul_div_SNo_R)
∀x y z, SNo xSNo ySNo z(x :/: y) * z = (x * z) :/: y
Proof:
Proof not loaded.
L33432
Theorem. (mul_div_SNo_L)
∀x y z, SNo xSNo ySNo zz * (x :/: y) = (z * x) :/: y
Proof:
Proof not loaded.
L33440
Theorem. (div_mul_SNo_invL)
∀x y, SNo xSNo yy 0(x * y) :/: y = x
Proof:
Proof not loaded.
L33447
Theorem. (div_div_SNo)
∀x y z, SNo xSNo ySNo z(x :/: y) :/: z = x :/: (y * z)
Proof:
Proof not loaded.
L33497
Theorem. (mul_div_SNo_both)
∀x y z w, SNo xSNo ySNo zSNo w(x :/: y) * (z :/: w) = (x * z) :/: (y * w)
Proof:
Proof not loaded.
L33506
Theorem. (recip_SNo_pos_pos)
∀x, SNo x0 < x0 < recip_SNo_pos x
Proof:
Proof not loaded.
L33522
Theorem. (div_SNo_pos_pos)
∀x y, SNo xSNo y0 < x0 < y0 < x :/: y
Proof:
Proof not loaded.
L33530
Theorem. (div_SNo_neg_pos)
∀x y, SNo xSNo yx < 00 < yx :/: y < 0
Proof:
Proof not loaded.
L33538
Theorem. (div_SNo_pos_LtL)
∀x y z, SNo xSNo ySNo z0 < yx < z * yx :/: y < z
Proof:
Proof not loaded.
L33559
Theorem. (div_SNo_pos_LtR)
∀x y z, SNo xSNo ySNo z0 < yz * y < xz < x :/: y
Proof:
Proof not loaded.
L33580
Theorem. (div_SNo_pos_LtL')
∀x y z, SNo xSNo ySNo z0 < yx :/: y < zx < z * y
Proof:
Proof not loaded.
L33599
Theorem. (div_SNo_pos_LtR')
∀x y z, SNo xSNo ySNo z0 < yz < x :/: yz * y < x
Proof:
Proof not loaded.
L33618
Theorem. (mul_div_SNo_nonzero_eq)
∀x y z, SNo xSNo ySNo zy 0x = y * zx :/: y = z
Proof:
Proof not loaded.
End of Section SurrealDiv
Beginning of Section Reals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L33641
Theorem. (SNoS_omega_drat_intvl)
∀xSNoS_ ω, ∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k
Proof:
Proof not loaded.
L33669
Theorem. (SNoS_ordsucc_omega_bdd_above)
∀xSNoS_ (ordsucc ω), x < ω∃Nω, x < N
Proof:
Proof not loaded.
L33716
Theorem. (SNoS_ordsucc_omega_bdd_below)
∀xSNoS_ (ordsucc ω), - ω < x∃Nω, - N < x
Proof:
Proof not loaded.
L33737
Theorem. (SNoS_ordsucc_omega_bdd_drat_intvl)
∀xSNoS_ (ordsucc ω), - ω < xx < ω∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k
Proof:
Proof not loaded.
L33875
Definition. We define real to be {xSNoS_ (ordsucc ω)|x ω x - ω (∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)} of type set.
L33877
Theorem. (real_I)
∀xSNoS_ (ordsucc ω), x ωx - ω(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)x real
Proof:
Proof not loaded.
L33893
Theorem. (real_E)
∀xreal, ∀p : prop, (SNo xSNoLev x ordsucc ωx SNoS_ (ordsucc ω)- ω < xx < ω(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)p)p
Proof:
Proof not loaded.
L33936
Theorem. (real_SNo)
∀xreal, SNo x
Proof:
Proof not loaded.
L33941
Theorem. (real_SNoS_omega_prop)
∀xreal, ∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x
Proof:
Proof not loaded.
L33946
Proof:
Proof not loaded.
L34037
Theorem. (real_0)
Proof:
Proof not loaded.
L34041
Theorem. (real_1)
Proof:
Proof not loaded.
L34045
Theorem. (SNoLev_In_real_SNoS_omega)
∀xreal, ∀w, SNo wSNoLev w SNoLev xw SNoS_ ω
Proof:
Proof not loaded.
L34062
Theorem. (real_SNoCut_SNoS_omega)
∀L RSNoS_ ω, SNoCutP L RL 0R 0(∀wL, ∃w'L, w < w')(∀zR, ∃z'R, z' < z)SNoCut L R real
Proof:
Proof not loaded.
L34311
Theorem. (real_SNoCut)
∀L Rreal, SNoCutP L RL 0R 0(∀wL, ∃w'L, w < w')(∀zR, ∃z'R, z' < z)SNoCut L R real
Proof:
Proof not loaded.
L34708
Theorem. (minus_SNo_prereal_1)
∀x, SNo x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀qSNoS_ ω, (∀kω, abs_SNo (q + - - x) < eps_ k)q = - x)
Proof:
Proof not loaded.
L34734
Theorem. (minus_SNo_prereal_2)
∀x, SNo x(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)(∀kω, ∃qSNoS_ ω, q < - x - x < q + eps_ k)
Proof:
Proof not loaded.
L34764
Theorem. (SNo_prereal_incr_lower_pos)
∀x, SNo x0 < x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)∀kω, ∀p : prop, (∀qSNoS_ ω, 0 < qq < xx < q + eps_ kp)p
Proof:
Proof not loaded.
L34850
Theorem. (real_minus_SNo)
Proof:
Proof not loaded.
L34877
Theorem. (SNo_prereal_incr_lower_approx)
∀x, SNo x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)∃fSNoS_ ωω, ∀nω, f n < x x < f n + eps_ n ∀in, f i < f n
Proof:
Proof not loaded.
L35093
Theorem. (SNo_prereal_decr_upper_approx)
∀x, SNo x(∀qSNoS_ ω, (∀kω, abs_SNo (q + - x) < eps_ k)q = x)(∀kω, ∃qSNoS_ ω, q < x x < q + eps_ k)∃gSNoS_ ωω, ∀nω, g n + - eps_ n < x x < g n ∀in, g n < g i
Proof:
Proof not loaded.
L35156
Theorem. (SNoCutP_SNoCut_lim)
∀lambda, ordinal lambda(∀alphalambda, ordsucc alpha lambda)∀L RSNoS_ lambda, SNoCutP L RSNoLev (SNoCut L R) ordsucc lambda
Proof:
Proof not loaded.
L35222
Proof:
Proof not loaded.
L35227
Theorem. (SNo_approx_real_lem)
∀f gSNoS_ ωω, (∀n mω, f n < g m)∀p : prop, (SNoCutP {f n|nω} {g n|nω}SNo (SNoCut {f n|nω} {g n|nω})SNoLev (SNoCut {f n|nω} {g n|nω}) ordsucc ωSNoCut {f n|nω} {g n|nω} SNoS_ (ordsucc ω)(∀nω, f n < SNoCut {f n|nω} {g n|nω})(∀nω, SNoCut {f n|nω} {g n|nω} < g n)p)p
Proof:
Proof not loaded.
L35328
Theorem. (SNo_approx_real)
∀x, SNo x∀f gSNoS_ ωω, (∀nω, f n < x)(∀nω, x < f n + eps_ n)(∀nω, ∀in, f i < f n)(∀nω, x < g n)(∀nω, ∀in, g n < g i)x = SNoCut {f n|nω} {g n|nω}x real
Proof:
Proof not loaded.
L35545
Theorem. (SNo_approx_real_rep)
∀xreal, ∀p : prop, (∀f gSNoS_ ωω, (∀nω, f n < x)(∀nω, x < f n + eps_ n)(∀nω, ∀in, f i < f n)(∀nω, g n + - eps_ n < x)(∀nω, x < g n)(∀nω, ∀in, g n < g i)SNoCutP {f n|nω} {g n|nω}x = SNoCut {f n|nω} {g n|nω}p)p
Proof:
Proof not loaded.
L35728
Theorem. (real_add_SNo)
∀x yreal, x + y real
Proof:
Proof not loaded.
L36204
Theorem. (SNoS_ordsucc_omega_bdd_eps_pos)
∀xSNoS_ (ordsucc ω), 0 < xx < ω∃Nω, eps_ N * x < 1
Proof:
Proof not loaded.
L36255
Theorem. (real_mul_SNo_pos)
∀x yreal, 0 < x0 < yx * y real
Proof:
Proof not loaded.
L37620
Theorem. (real_mul_SNo)
∀x yreal, x * y real
Proof:
Proof not loaded.
L37678
Theorem. (nonneg_real_nat_interval)
∀xreal, 0 x∃nω, n x x < ordsucc n
Proof:
Proof not loaded.
L37757
Theorem. (pos_real_left_approx_double)
∀xreal, 0 < xx 2(∀mω, x eps_ m)∃wSNoL_pos x, x < 2 * w
Proof:
Proof not loaded.
L38122
Proof:
Proof not loaded.
L38866
Proof:
Proof not loaded.
L38872
Proof:
Proof not loaded.
L38898
Theorem. (real_div_SNo)
∀x yreal, x :/: y real
Proof:
Proof not loaded.
End of Section Reals
Beginning of Section even_odd
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L38915
Theorem. (nat_le2_cases)
∀m, nat_p mm 2m = 0 m = 1 m = 2
Proof:
Proof not loaded.
L38936
Theorem. (prime_nat_2_lem)
∀m, nat_p m∀n, nat_p nm * n = 2m = 1 m = 2
Proof:
Proof not loaded.
L38967
Proof:
Proof not loaded.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L38987
Theorem. (not_eq_2m_2n1)
∀m nint, 2 * m 2 * n + 1
Proof:
Proof not loaded.
End of Section even_odd
Beginning of Section form100_22b
L39029
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L39036
Proof:
Proof not loaded.
L39203
Theorem. (Repl_finite)
∀f : setset, ∀X, finite Xfinite {f x|xX}
Proof:
Proof not loaded.
L39256
Theorem. (infinite_bigger)
∀Xω, infinite X∀mω, ∃nX, m n
Proof:
Proof not loaded.
L39285
Proof:
Proof not loaded.
L41035
Proof:
Proof not loaded.
L41048
Proof:
Proof not loaded.
L41056
Proof:
Proof not loaded.
End of Section form100_22b
Beginning of Section rational
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L41082
Definition. We define rational to be {xreal|∃mint, ∃nω {0}, x = m :/: n} of type set.
End of Section rational
Beginning of Section form100_3
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
(*** The Denumerability of the Rational Numbers ***)
L41096
Proof:
Proof not loaded.
L41105
Proof:
Proof not loaded.
L41153
Proof:
Proof not loaded.
L41157
Proof:
Proof not loaded.
L41216
Definition. We define nat_pair to be λm n ⇒ 2 ^ m * (2 * n + 1) of type setsetset.
L41218
Theorem. (nat_pair_In_omega)
∀m nω, nat_pair m n ω
Proof:
Proof not loaded.
L41230
Theorem. (nat_pair_0)
∀m n m' n'ω, nat_pair m n = nat_pair m' n'm = m'
Proof:
Proof not loaded.
L41439
Theorem. (nat_pair_1)
∀m n m' n'ω, nat_pair m n = nat_pair m' n'n = n'
Proof:
Proof not loaded.
L41476
Proof:
Proof not loaded.
End of Section form100_3
Beginning of Section SurrealSqrt
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L41810
Definition. We define SNoL_nonneg to be λx ⇒ {wSNoL x|0 w} of type setset.
L41811
Proof:
Proof not loaded.
L41817
Proof:
Proof not loaded.
L41831
Definition. We define SNo_sqrtauxset to be λY Z x ⇒ yY{(x + y * z) :/: (y + z)|zZ, 0 < y + z} of type setsetsetset.
L41833
Theorem. (SNo_sqrtauxset_I)
∀Y Z x, ∀yY, ∀zZ, 0 < y + z(x + y * z) :/: (y + z) SNo_sqrtauxset Y Z x
Proof:
Proof not loaded.
L41843
Theorem. (SNo_sqrtauxset_E)
∀Y Z x, ∀uSNo_sqrtauxset Y Z x, ∀p : prop, (∀yY, ∀zZ, 0 < y + zu = (x + y * z) :/: (y + z)p)p
Proof:
Proof not loaded.
L41857
Theorem. (SNo_sqrtauxset_0)
∀Z x, SNo_sqrtauxset 0 Z x = 0
Proof:
Proof not loaded.
L41865
Theorem. (SNo_sqrtauxset_0')
∀Y x, SNo_sqrtauxset Y 0 x = 0
Proof:
Proof not loaded.
L41874
Definition. We define SNo_sqrtaux to be λx g ⇒ nat_primrec ({g w|wSNoL_nonneg x},{g z|zSNoR x}) (λk p ⇒ (p 0 SNo_sqrtauxset (p 0) (p 1) x,p 1 SNo_sqrtauxset (p 0) (p 0) x SNo_sqrtauxset (p 1) (p 1) x)) of type set(setset)setset.
L41881
Theorem. (SNo_sqrtaux_0)
∀x, ∀g : setset, SNo_sqrtaux x g 0 = ({g w|wSNoL_nonneg x},{g z|zSNoR x})
Proof:
Proof not loaded.
L41889
Theorem. (SNo_sqrtaux_S)
∀x, ∀g : setset, ∀n, nat_p nSNo_sqrtaux x g (ordsucc n) = (SNo_sqrtaux x g n 0 SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 1) x,SNo_sqrtaux x g n 1 SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 0) x SNo_sqrtauxset (SNo_sqrtaux x g n 1) (SNo_sqrtaux x g n 1) x)
Proof:
Proof not loaded.
L41903
Theorem. (SNo_sqrtaux_mon_lem)
∀x, ∀g : setset, ∀m, nat_p m∀n, nat_p nSNo_sqrtaux x g m 0 SNo_sqrtaux x g (add_nat m n) 0 SNo_sqrtaux x g m 1 SNo_sqrtaux x g (add_nat m n) 1
Proof:
Proof not loaded.
L41945
Theorem. (SNo_sqrtaux_mon)
∀x, ∀g : setset, ∀m, nat_p m∀n, nat_p nm nSNo_sqrtaux x g m 0 SNo_sqrtaux x g n 0 SNo_sqrtaux x g m 1 SNo_sqrtaux x g n 1
Proof:
Proof not loaded.
L41959
Theorem. (SNo_sqrtaux_ext)
∀x, SNo x∀g h : setset, (∀x'SNoS_ (SNoLev x), g x' = h x')∀k, nat_p kSNo_sqrtaux x g k = SNo_sqrtaux x h k
Proof:
Proof not loaded.
Beginning of Section sqrt_SNo_nonneg
L42000
Let G : set(setset)setλx g ⇒ SNoCut (kωSNo_sqrtaux x g k 0) (kωSNo_sqrtaux x g k 1)
L42001
Definition. We define sqrt_SNo_nonneg to be SNo_rec_i G of type setset.
L42002
Proof:
Proof not loaded.
L42027
Theorem. (sqrt_SNo_nonneg_prop1a)
∀x, SNo x0 x(∀wSNoS_ (SNoLev x), 0 wSNo (sqrt_SNo_nonneg w) 0 sqrt_SNo_nonneg w sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w)∀k, nat_p k(∀ySNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y 0 y y * y < x) (∀ySNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y 0 y x < y * y)
Proof:
Proof not loaded.
L42465
Proof:
Proof not loaded.
L42534
Theorem. (sqrt_SNo_nonneg_prop1c)
∀x, SNo x0 xSNoCutP (kωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (kωSNo_sqrtaux x sqrt_SNo_nonneg k 1)(∀z(kωSNo_sqrtaux x sqrt_SNo_nonneg k 1), ∀p : prop, (SNo z0 zx < z * zp)p)0 G x sqrt_SNo_nonneg
Proof:
Proof not loaded.
L42570
Proof:
Proof not loaded.
L42853
Proof:
Proof not loaded.
L43237
Proof:
Proof not loaded.
End of Section sqrt_SNo_nonneg
L43320
Theorem. (SNo_sqrtaux_0_1_prop)
∀x, SNo x0 x∀k, nat_p k(∀ySNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y 0 y y * y < x) (∀ySNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y 0 y x < y * y)
Proof:
Proof not loaded.
L43331
Theorem. (SNo_sqrtaux_0_prop)
∀x, SNo x0 x∀k, nat_p k∀ySNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y 0 y y * y < x
Proof:
Proof not loaded.
L43340
Theorem. (SNo_sqrtaux_1_prop)
∀x, SNo x0 x∀k, nat_p k∀ySNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y 0 y x < y * y
Proof:
Proof not loaded.
L43349
Proof:
Proof not loaded.
L43357
Theorem. (SNo_sqrt_SNo_nonneg)
∀x, SNo x0 xSNo (sqrt_SNo_nonneg x)
Proof:
Proof not loaded.
L43363
Theorem. (sqrt_SNo_nonneg_nonneg)
∀x, SNo x0 x0 sqrt_SNo_nonneg x
Proof:
Proof not loaded.
L43369
Theorem. (sqrt_SNo_nonneg_sqr)
∀x, SNo x0 xsqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x
Proof:
Proof not loaded.
L43375
Proof:
Proof not loaded.
L43455
Proof:
Proof not loaded.
L43579
Theorem. (sqrt_SNo_nonneg_0inL0)
∀x, SNo x0 x0 SNoLev x0 SNo_sqrtaux x sqrt_SNo_nonneg 0 0
Proof:
Proof not loaded.
L43607
Proof:
Proof not loaded.
L43625
Proof:
Proof not loaded.
L43699
Theorem. (SNo_sqrtauxset_real)
∀Y Z x, Y realZ realx realSNo_sqrtauxset Y Z x real
Proof:
Proof not loaded.
L43726
Theorem. (SNo_sqrtauxset_real_nonneg)
∀Y Z x, Y {wreal|0 w}Z {zreal|0 z}x real0 xSNo_sqrtauxset Y Z x {wreal|0 w}
Proof:
Proof not loaded.
L43797
Proof:
Proof not loaded.
L44221
Proof:
Proof not loaded.
End of Section SurrealSqrt
Beginning of Section form100_1
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
L44647
Theorem. (divides_int_div_SNo_int)
∀m n, divides_int m nn :/: m int
Proof:
Proof not loaded.
L44684
Theorem. (form100_1_lem1)
∀m, nat_p m∀n, nat_p nm * m = 2 * n * nn = 0
Proof:
Proof not loaded.
L44847
Theorem. (form100_1_lem2)
∀mω, ∀nω 1, m * m 2 * n * n
Proof:
Proof not loaded.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
L44869
Proof:
Proof not loaded.
End of Section form100_1