() Def 1: [Ordered pair] [X,Y] ≡Df {{X},{{X},{{Y},Y}}}

(8) Def 2: [First component of ordered pair] X&#x ≡Df ∋∋X

(8) Def 3: [Second component of ordered pair] X&#x ≡Df ∋∋(∋(X - {∋X}) - {∋X})

(12) Def setformer.0: [Witness to difference of two setformers] XΘ ≡Df ∋{X ∈ S | E(X) ≠ E0(X) ∨ ¬(P(X) ↔ PP(X))}

(15) Def setformer2.0a: [Witness to difference of two setformers, two-variable case] XYΘ ≡Df ∋{[X,Y]: X ∈ S, Y ∈ F(X)∪FP(X) | F(X) ≠ FP(X) ∨ E2(X,Y) ≠ EP2(X,Y) ∨ ¬(R(X,Y) ↔ PQ(X,Y))}

(15) Def setformer2.0b: [First component of difference witness] XΘ ≡Df XYΘ&#x

(15) Def setformer2.0c: [Second component of difference witness] YΘ ≡Df XYΘ&#x

(16) Def 00g: [Set former] TTΘ ≡Df {X ∈ S | P(X)}

(18) Def 10: [Is-an-ordinal predicate] IsO(S) ≡Df (∀X ∈ S | X ⊆ S) & (∀X ∈ S, Y ∈ S | X ∈ Y ∨ Y ∈ X ∨ X = Y)

(20) Def ordinal_induction.0: [Wtness for ordinal induction arguments] TΘ ≡Df ∋{X ⊆ O | IsO(X) & P(X)}

(21) Def 35a: [Transitive membership closure of \$S\$] ∈..S ≡Df S∪{Y: U ∈ {∈..X: X ∈ S}, Y ∈ U}

(27) Def 25: [Union Set] S ≡Df {X: Y ∈ S, X ∈ Y}

(27) Def 7g: [Set of members of members] MEMBS2(S) ≡Df S∪S

(27) Def 7h: [Recursively defined iterated members] MEMBS_X(S,X) ≡Df if X = ∋s then S else MEMBS2({MEMBS_X(S,Y): Y ∈ X}) end if

(27) Def 7i: [Ultimate members of a set, first definition] ULT_MEMB1(S) ≡Df {MEMBS_X(S,X): X ∈ s}

(29) Def transfinite_induction.0: [Witness for transfinite induction argument] MTΘ ≡Df ∋{M: M ∈ ULT_MEMB1({N}) | P(M)}

(32) Def 00h: [Restricted witness for transfinite induction argument] MTΘ ≡Df ∋{K ∈ ∈..{N} | P(K)}

(34) Def 4: [Is-a-map predicate] IsM(F) ≡Df F = {[X&#x,X&#x]: X ∈ F}

(34) Def 5: [Map domain] ДF ≡Df {X&#x: X ∈ F}

(34) Def 6: [Map range] ЯF ≡Df {X&#x: X ∈ F}

(34) Def 7: [Single-valued map predicate] Is1(F) ≡Df IsM(F) & (∀X ∈ F, Y ∈ F | X&#x = Y&#x → X = Y)

(34) Def 8: [One-one map predicate] 11(F) ≡Df Is1(F) & (∀X ∈ F, Y ∈ F | X&#x = Y&#x → X = Y)

(38) Def Svm_test.0a: [Witness to non-singlevaluedness] XYΘ ≡Df ∋{[X,Y]: X ∈ S, Y ∈ S | A(X) = A(Y) & B(X) ≠ B(Y)}

(38) Def Svm_test.0b: [First component of witness to non-singlevaluedness] XΘ ≡Df XYΘ&#x

(38) Def Svm_test.0c: [Second component of witness to non-singlevaluedness] YΘ ≡Df XYΘ&#x

(39) Def Svm_test.0a: [Witness to non-singlevaluedness, two-variable case] XYΘ ≡Df ∋{[[X,Y],[XP,YP]]: X ∈ S, Y ∈ T, XP ∈ S, YP ∈ T | P2(X,Y) & P2(XP,YP) & A2(X,Y) = A2(XP,YP) & B2(X,Y) ≠ B2(XP,YP)}

(39) Def Svm_test.0b: [1,1 component of witness to non-singlevaluedness, two-variable case] XΘ ≡Df XYΘ&#x&#x

(39) Def Svm_test.0c: [1,2 component of witness to non-singlevaluedness, two-variable case] YΘ ≡Df XYΘ&#x&#x

(39) Def Svm_test.0d: [2,1 component of witness to non-singlevaluedness, two-variable case] XPΘ ≡Df XYΘ&#x&#x

(39) Def Svm_test.0h: [2,2 component of witness to non-singlevaluedness, two-variable case] YPΘ ≡Df XYΘ&#x&#x

(40) Def Svm_test.0a: [Witness to non-singlevaluedness, three-variable case] XYΘ ≡Df ∋{[[X,[Y,WZ]],[XP,[YP,WZP]]]: X ∈ S, Y ∈ T, WZ ∈ U, XP ∈ S, YP ∈ T, WZP ∈ U | A3(X,Y,WZ) = A3(XP,YP,WZP) & B3(X,Y,WZ) ≠ B3(XP,YP,WZP) & P3(X,Y,WZ) & P3(XP,YP,WZP)}

(40) Def Svm_test.0b: [1,1-component of witness to non-singlevaluedness, three-variable case] XΘ ≡Df XYΘ&#x&#x

(40) Def Svm_test.0c: [1,2,1-component of witness to non-singlevaluedness, three-variable case] YΘ ≡Df XYΘ&#x&#x&#x

(40) Def Svm_test.0c: [1,2,2-component of witness to non-singlevaluedness, three-variable case] ZΘ ≡Df XYΘ&#x&#x&#x

(40) Def Svm_test.0d: [2,1-component of witness to non-singlevaluedness, three-variable case] XPΘ ≡Df XYΘ&#x&#x

(40) Def Svm_test.0h: [2,2,1-component of witness to non-singlevaluedness, three-variable case] YPΘ ≡Df XYΘ&#x&#x&#x

(40) Def Svm_test.0f: [2,2,2-component of witness to non-singlevaluedness, three-variable case] ZPΘ ≡Df XYΘ&#x&#x&#x

(41) Def one_1_test.0a: [Witness to non-one-oneness of a map] XYΘ ≡Df ∋{[X,Y]: X ∈ S, Y ∈ S | A(X) = A(Y)¬↔(B(X) = B(Y))}

(41) Def one_1_test.0b: [First component of witness to map non-one-oneness] XΘ ≡Df XYΘ&#x

(41) Def one_1_test.0c: [Second component of witness to map non-one-oneness] YΘ ≡Df XYΘ&#x

(42) Def one_1_test_2.0a: [Witness to map non-one-oneness, two-variable case] XYΘ ≡Df ∋{[[X,Y],[X2,Y2]]: X ∈ S, Y ∈ T, X2 ∈ S, Y2 ∈ T | ¬(A2(X,Y) = A2(X2,Y2) ↔ B2(X,Y) = B2(X2,Y2))}

(42) Def one_1_test_2.0b: [1,1-component of witness to map non-one-oneness, two-variable case] XΘ ≡Df XYΘ&#x&#x

(42) Def one_1_test_2.0c: [1-2-component of witness to map non-one-oneness, two-variable case] YΘ ≡Df XYΘ&#x&#x

(42) Def one_1_test_2.0d: [2,1-component of witness to map non-one-oneness, two-variable case] X2Θ ≡Df XYΘ&#x&#x

(42) Def one_1_test_2.0h: [2,1-component of witness to map non-one-oneness, two-variable case] Y2Θ ≡Df XYΘ&#x&#x

(43) Def one_1_test_3.0a: [Witness to map non one-ness, three-variable case] XYZΘ ≡Df ∋{[[X,[Y,WZ]],[X2,[Y2,Z2]]]: X ∈ S, Y ∈ T, WZ ∈ R, X2 ∈ S, Y2 ∈ T, Z2 ∈ R | P3(X,Y,WZ) & P3(X2,Y2,Z2) & (A3(X,Y,WZ) ≠ A3(X2,Y2,Z2) ↔ B3(X,Y,WZ) = B3(X2,Y2,Z2))}

(43) Def one_1_test_3.0b: [1,1-component of witness to map non one-ness, three-variable case] XΘ ≡Df XYZΘ&#x&#x

(43) Def one_1_test_3.0c: [1,2,1-component of witness to map non one-ness, three-variable case] YΘ ≡Df XYZΘ&#x&#x&#x

(43) Def one_1_test_3.0c: [1,2,2-component of witness to map non one-ness, three-variable case] ZΘ ≡Df XYZΘ&#x&#x&#x

(43) Def one_1_test_3.0d: [2,1-component of witness to map non one-ness, three-variable case] XPΘ ≡Df XYZΘ&#x&#x

(43) Def one_1_test_3.0h: [2,2,1-component of witness to map non one-ness, three-variable case] YPΘ ≡Df XYZΘ&#x&#x&#x

(43) Def one_1_test_3.0f: [2,2,2-component of witness to map non one-ness, three-variable case] ZPΘ ≡Df XYZΘ&#x&#x&#x

(49) Def 11: S+ ≡Df S∪{S}

(58) Def 9: [The enumeration of a set] ENUM(X,S) ≡Df if S ⊆ {ENUM(Y,S): Y ∈ X} then S else ∋(S - {ENUM(Y,S): Y ∈ X}) end if

(64) Def 12: [Map Restriction] (FɭA) ≡Df {P ∈ F | P&#x ∈ A}

(64) Def 13: [Value of single-valued function] (Fˆ(X)) ≡Df ∋(Fɭ{X})&#x

(64) Def 14: [Map Product] (F◊G) ≡Df {[X&#x,Y&#x]: X ∈ G, Y ∈ F | X&#x = Y&#x}

(64) Def 14a: [Inverse Map] F ≡Df {[X&#x,X&#x]: X ∈ F}

(64) Def 14b: [Identity Map on a set \$S\$] ϊS ≡Df {[X,X]: X ∈ S}

(65) Def 15: [Cardinality] #S ≡Df ∋{X: X ∈ ENUM_ORD(S)+ | (∃F ∈ Ω | 11(F) & ДF = X & ЯF = S)}

(65) Def 16: [Is-a-cardinal predicate] IsC(C) ≡Df IsO(C) & (∀Y ∈ C, F ∈ Ω | ¬ДF = Y ∨ ¬ЯF = C ∨ ¬Is1(F))

(96) Def fcn_symbol.0a: [Witness to non-singlevaluedness of map inverse] XYΘ ≡Df ∋{[XX,YY]: XX ∈ S, YY ∈ S | F(XX) = F(YY) & XX ≠ YY}

(96) Def fcn_symbol.0b: [First component of witness to non-singlevaluedness of map inverse] XΘ ≡Df XYΘ&#x

(96) Def fcn_symbol.0c: [Second component of witness to non-singlevaluedness of map inverse] YΘ ≡Df XYΘ&#x

(154) Def 17: [Cartesian Product] (S × T) ≡Df {[X,Y]: X ∈ S, Y ∈ T}

(192) Def 14d: [Inverse Map Image] (G↶R) ≡Df {P&#x: P ∈ G | P&#x ∈ R}

(203) Def 18: [Finiteness] IsΦ(S) ≡Df ¬(∃F ∈ Ω | 11(F) & ДF = S & ЯF ⊆ S & S ≠ ЯF)

(226) Def 18a: [The set of integers] ℕ ≡Df ∋{X: X ∈ #s+ | ¬IsΦ(X)}

(228) Def 18b: [The integer 1] 1 ≡Df 0+

(228) Def 18b: [The integer 2] 2 ≡Df 1+

(228) Def 18b: [The integer 3] 3 ≡Df 2+

(228) Def 18b: [The integer 4] 4 ≡Df 3+

(231) Def 19: [Cardinal sum] (N + M) ≡Df #({[X,0]: X ∈ N}∪{[X,1]: X ∈ M})

(231) Def 20: [Cardinal product] (N • M) ≡Df #(N × M)

(231) Def 21: [Powerset of a set] S ≡Df {X: X ⊆ S}

(231) Def 22: [Cardinal Difference] (N - M) ≡Df #(N - M)

(231) Def 23: [Integer Quotient; Note that \$x/0\$ is defined as \$Za\$ for \$x in Za\$] (M / N) ≡Df {K ∈ ℕ | K • N ⊆ M}

(231) Def 24: [Integer Remainder] (M ↓ N) ≡Df M - M / N • N

(252) Def finite_induction0: [Witness for finite induction argument by subset induction] MΘ ≡Df ∋{M: M ⊆ N | P(M) & (∀K ⊆ M | K ≠ M → ¬P(K))}

(330) Def 00q: [Upper bound of integer set] BYNDΘ ≡Df {X ∈ ℕ | Q1(X)}+

(337) Def 24a: [Finite sequences] IsΦσ(S) ≡Df {F ⊆ ℕ × S | Is1(F) & ДF ∈ ℕ}

(337) Def 24b: [Sequence concatenation] F +σ G ≡Df {[N,if N ∈ ДF then Fˆ(N) else Gˆ(N - ДF) end if]: N ∈ ДF + ДG}

(337) Def 24c: [Subsequences] σ(F) ≡Df {F◊H: H ⊆ ℕ × ℕ | Is1(H) & (∀I | I+ ∈ ДH → I ∈ ДH & Hˆ(I) ∈ Hˆ(I+))}

(337) Def 24d: [Shift operation for sequences] SHIFT(M) ≡Df {[I,M + I]: I ∈ ℕ}

(337) Def 24e: [Shifted sequence] SHIFTED_SEQ(F,M) ≡Df F◊SHIFT(M)

(352) Def subseq.0: [Subsequence generator] HΘ ≡Df {P ∈ ∋{H ⊆ ℕ × ℕ | G = F◊H & Is1(H) & (∀I | I+ ∈ ДH → I ∈ ДH & Hˆ(I) ∈ Hˆ(I+))} | P&#x ∈ ДF}

(360) Def 00a: [Points at which f attains its minimum] RNGΘ ≡Df {X: X ∈ S | F(X) = ∋{F(U): U ∈ S}}

(364) Def 10000: [?] MINRELΘ(T) ≡Df if T ⊆ S & T ≠ 0 then ∋{M: M ∈ T | (∀Y ∈ T | ¬ ∠ (Y,M))} else S end if

(368) Def 00b: [The enumeration defined by a well-founded ordering relationship] ORDENMΘ(X) ≡Df MINRELΘ(S - {ORDENMΘ(Y): Y ∈ X})

(376) Def well_founded_set.b: [?] IsOΘ ≡Df ∋{O ∈ #S+ | IsO(O) & S = {ORDENMΘ(X): X ∈ O} & (∀X ∈ O | ORDENMΘ(X) ≠ S) & 11({[X,ORDENMΘ(X)]: X ∈ O})}

(393) Def product_order_c: [Lexicographic ordering of a Cartesian product set] ≪Θ(X,Y) ≡Df X&#x∪X&#x ∈ Y&#x∪Y&#x ∨ X&#x∪X&#x = Y&#x∪Y&#x & X&#x ∈ Y&#x ∨ X&#x∪X&#x = Y&#x∪Y&#x & X&#x = Y&#x & X&#x ∈ Y&#x

(410) Def 26: [The signed Integers] ℤ ≡Df {[X,Y]: X ∈ ℕ, Y ∈ ℕ | X = 0 ∨ Y = 0}

(410) Def 27: [Signed Integer Reduction to Normal Form] P➮ℤ ≡Df [P&#x - P&#x∩P&#x,P&#x - P&#x∩P&#x]

(410) Def 28: [Signed addition] (MM + NN) ≡Df [MM&#x + NN&#x,MM&#x + NN&#x]➮ℤ

(410) Def 28a: [Absolute value of a signed integer] ǁM ≡Df M&#x∪M&#x

(410) Def 28b: [Negative of a signed integer] −M ≡Df [M&#x,M&#x]

(410) Def 29: [Signed Product] (MM • NN) ≡Df [MM&#x • NN&#x + MM&#x • NN&#x,MM&#x • NN&#x + NN&#x • MM&#x]➮ℤ

(410) Def 32: [Signed Difference] (N - M) ≡Df [M&#x + N&#x,M&#x + N&#x]➮ℤ

(410) Def 33: [Sign of a signed integer] Is≥0(X) ≡Df X&#x ⊇ X&#x

(472) Def 00r: [Ordinal index defined by the standard enumeration of sets] INDEX(X) ≡Df ∋{J: J ∈ O | ORDEN(J) = X}

(472) Def 00s: [?] HH(X,T) ≡Df F3({G4(HH(J,T),ORDEN(J),ORDEN(X),T): J ∈ X |  ∠ (ORDEN(J),ORDEN(X)) & P4(HH(J,T),ORDEN(J),ORDEN(X),T)},ORDEN(X),T)

(472) Def 00t: [?] H2Θ(V,T) ≡Df HH(INDEX(V),T)

(482) Def finite_recursive_fcn.b: [?] H2Θ(U,V) ≡Df HSKO(U,V)ˆ(U)

(488) Def 00f: [?] H1Θ(S) ≡Df H(S,0)

(497) Def equivalence_classes.0a: [The equivalence class of an element \$X\$] FΘ(X) ≡Df {Z ∈ S | R(X,Z)}

(497) Def equivalence_classes.0b: [The set of all equivalence classes formed by partitioning] EQCΘ ≡Df {FΘ(X): X ∈ S}

(501) Def 10030: [Less-than-or-equal comparison] (X  ΘY) ≡Df  ∠ (X,Y) ∨ X = Y

(503) Def 10031: [Choice of the smaller] SMALLERΘ(X,Y) ≡Df if X ∉ S0 & Y ∉ S0 then S0 elseif X ∉ S0 then Y elseif Y ∉ S0 then X elseif  ∠ (X,Y) then X else Y end if

(503) Def 10032: [Choice of the larger] LARGERΘ(X,Y) ≡Df if X ∉ S0 & Y ∉ S0 then S0 elseif X ∉ S0 then Y elseif Y ∉ S0 then X elseif  ∠ (X,Y) then Y else X end if

(513) Def 10033: [Upper bounds] UBSΘ(T) ≡Df {X ∈ S0 | (∀Y ∈ T∩S0 | SMALLERΘ(Y,X) = Y)}

(513) Def 10034: [Maximum of a set] MAXΘ(T) ≡Df ∋({S0}∪T∩UBSΘ(T))

(513) Def 10035: [Least upper bound of a set] LUBΘ(T) ≡Df ∋({S0}∪{X ∈ UBSΘ(T) | UBSΘ(T) ⊆ UBSΘ({X})})

(516) Def transfinite_definition_0_params.0a: [Function defined by a 1-parameter transfinite recursion] FΘ(X) ≡Df G({H1(FΘ(T)): T ∈ X})

(517) Def transfinite_definition_1_params.0a: [Function defined by a transfinite recursion with supplementary parameter] F2Θ(X,A) ≡Df G2({H(FΘ(T),A): T ∈ X},A)

(521) Def 332a: [The predicate '\$T\$ is a filter on the set \$S\$] FILTER(T,S) ≡Df T ⊆ S & 0 ∉ T & (∀X ∈ T, Y ∈ T | X∩Y ∈ T) & (∀X ∈ T, Y ⊆ S | Y ⊇ X → Y ∈ T)

(521) Def 332b: [The predicate '\$T\$ is an ultrafilter on the set \$S\$] ULTRAFILTER(T,S) ≡Df FILTER(T,S) & (∀Y ⊆ S | Y ∈ T ∨ S - Y ∈ T)

(524) Def 35: [The set of formal fractions] Fr ≡Df {[X,Y]: X ∈ ℤ, Y ∈ ℤ | Y ≠ [0,0]}

(524) Def 36: [Equivalence of formal fractions] P ≈ Q ≡Df P&#x • Q&#x = P&#x • Q&#x

(524) Def 36a: [Nonnegative fraction] Is≥0Fr(X) ≡Df Is≥0(X&#x • X&#x)

(530) Def 37: [The zero rational] 0 ≡Df [[0,0],[1,0]]➮ℚ

(530) Def 37a: [The unit rational] 1 ≡Df [[1,0],[1,0]]➮ℚ

(530) Def 38: [Rational Sum] (X + Y) ≡Df [∋X&#x • ∋Y&#x + ∋Y&#x • ∋X&#x,∋X&#x • ∋Y&#x]➮ℚ

(530) Def 39: [Rational product] (X • Y) ≡Df [∋X&#x • ∋Y&#x,∋X&#x • ∋Y&#x]➮ℚ

(530) Def 40: [Rational reciprocal] ⅟(X) ≡Df [∋X&#x,∋X&#x]➮ℚ

(530) Def 41: [Rational quotient] (X / Y) ≡Df X • ⅟(Y)

(530) Def 42: [Rational negative] −X ≡Df [−∋X&#x,∋X&#x]➮ℚ

(530) Def 43: [Nonnegative Rational] Is≥0(X) ≡Df Is≥0(∋X&#x • ∋X&#x)

(530) Def 44: [Rational Subtraction] (X - Y) ≡Df X + −Y

(530) Def 45: [Rational Comparison] (X > Y) ≡Df Is≥0(X - Y) & X ≠ Y

(530) Def 00j: [Generic 'greater or equal' comparison] (X  ΘY) ≡Df NNEG(X ⊕ RVZ(Y))

(530) Def 00k: [Generic 'less or equal' comparison] (X  ΘY) ≡Df Y  ΘX

(530) Def 00m: [Generic 'greater than' comparison] (X ≻ ΘY) ≡Df X  ΘY & X ≠ Y

(530) Def 00n: [Generic 'less than' comparison] (X ≺ ΘY) ≡Df Y ≻ ΘX

(640) Def 46: [The set of rational sequences] Seq ≡Df {F: F ⊆ ℕ × ℚ | ДF = ℕ & Is1(F)}

(640) Def 47: [The constant 0 rational sequence] 0 ≡Df ℕ × {0}

(640) Def 48: [The constant 1 rational sequence] 1 ≡Df ℕ × {1}

(640) Def 49: [Pointwise sum of rational sequences] (X + Y) ≡Df {[P&#x,P&#x + Yˆ(P&#x)]: P ∈ X}

(640) Def 50: [Pointwise additive inverse of rational sequence]  −X ≡Df {[P&#x,−P&#x]: P ∈ X}

(640) Def 51: [Pointwise absolute value of rational sequence] ǁX ≡Df {[P&#x,ǁP&#x]: P ∈ X}

(640) Def 52: [Pointwise difference of rational sequences] (X - Y) ≡Df X +  −Y

(640) Def 53: [Product of rational sequences] (X • Y) ≡Df {[P&#x,P&#x • Yˆ(P&#x)]: P ∈ X}

(640) Def 54: [Pointwise reciprocal of rational sequence] RAS_RECIPX ≡Df SHIFTED_SEQ({[I,⅟(Xˆ(I))]: I ∈ ℕ},∋{H ∈ ℕ | (∀I ∈ ℕ - H | Xˆ(I) ≠ 0)})

(640) Def 55: [Pointwise quotient of rational sequences] (X / Y) ≡Df X • RAS_RECIPY

(640) Def 56: [Rational Cauchy sequences] Cau ≡Df {F: F ∈ Seq | (∀ε ∈ ℚ | ε > 0 → IsΦ({I∩J: I ∈ ℕ, J ∈ ℕ | ǁ(Fˆ(I) - Fˆ(J)) > ε}))}

(640) Def 57: [Equivalence of rational sequences] F ≈ G ≡Df (∀ε ∈ ℚ | ε > 0 → IsΦ({X: X ∈ ДF | ǁ(Fˆ(X) - Gˆ(X)) > ε}))

(706) Def 58: [The zero real] 0 ≡Df 0➮ℝ

(706) Def 58a: [The unit real] 1 ≡Df 1➮ℝ

(706) Def 59: [Real Sum] (X + Y) ≡Df (∋X + ∋Y)➮ℝ

(706) Def 60: [Real Negative] −X ≡Df  −∋X➮ℝ

(706) Def 61: [Real Subtraction] (X - Y) ≡Df (∋X - ∋Y)➮ℝ

(706) Def 62: [Absolute value, i.e. the larger of \$X\$ and \$R_Rev(X)\$] ǁX ≡Df ǁ∋X➮ℝ

(706) Def 63: [Real Multiplication] (X • Y) ≡Df (∋X • ∋Y)➮ℝ

(706) Def 64: [Real Reciprocal] ⅟X ≡Df RAS_RECIP∋X➮ℝ

(706) Def 65: [Real Quotient] (X / Y) ≡Df X • ⅟Y

(706) Def 66: [Non-negative Real] Is≥0(X) ≡Df ǁ∋X➮ℝ = X

(706) Def 67: [Real Comparison] (X > Y) ≡Df Is≥0(X - Y) & ¬X = Y

(706) Def 68: [Real Comparison] (X ≥ Y) ≡Df Is≥0(X - Y)

(803) Def 69: [Embedding of rationals into reals] RERA(X) ≡Df (ℕ × {X})➮ℝ

(808) Def 70: [Embedding of signed integers into rationals] RASI(X) ≡Df [X,1]➮ℚ

(812) Def 71: [Embedding of integers into signed integers] SIZA(X) ≡Df [X,0]

(816) Def 72: [The set of real sequences] RESEQ ≡Df {F: F ⊆ ℕ × ℝ | ДF = ℕ & Is1(F)}

(816) Def 73: [Real Cauchy sequences] RECAUCHY ≡Df {F: F ∈ RESEQ | (∀ε ∈ ℝ | ε > 0 → IsΦ({I∩J: I ∈ ℕ, J ∈ ℕ | RE_ABS(Fˆ(I) - Fˆ(J)) > ε}))}

(816) Def 74: [Sum of real functions] (X�RES_PLUSY) ≡Df {[P&#x,P&#x + Yˆ(P&#x)]: P ∈ X}

(816) Def 75: [Addditive inverse of real function] RES_REV(X) ≡Df {[P&#x,RE_REV(P&#x)]: P ∈ X}

(816) Def 76: [Absolute values of real function] RES_ABS(X) ≡Df {[P&#x,RE_ABS(P&#x)]: P ∈ X}

(816) Def 77: [Difference of real functions] (X�RES_MINUSY) ≡Df X�RES_PLUSRES_REV(Y)

(816) Def 78: [Product of real functions] (X�RES_TIMESY) ≡Df {[P&#x,P&#x • Yˆ(P&#x)]: P ∈ X}

(817) Def 79: [Approximating rational sequence for a real sequence] RA_APSEQ(F,G) ≡Df (∀ε ∈ ℝ | ε > 0 → IsΦ({X: X ∈ ДF | ǁ(RERA(Fˆ(X)) - Gˆ(X)) > ε}))

(819) Def 80: [Limit of a real Cauchy sequence] LIMIT(F) ≡Df ∋{G ∈ Cau | RA_APSEQ(F,G)}➮ℝ

(834) Def 81: [Continuous real function of a real variable] CF_RR(F) ↔ ДF = ℝ & ЯF ⊆ ℝ & Is1(F) & (∀G ∈ RECAUCHY | F◊G ∈ RECAUCHY)

(842) Def 10001: [Integer divisibility] DIVIDES(K,N) ≡Df (∃J | N = K • J)

(842) Def 10002: [Primality criterion for unsigned integers] IS_PRIME(P) ≡Df 1 ∈ P & ¬(∃K ∈ P | 1 ∈ K & DIVIDES(K,P))

(842) Def 10003: [Smallest factor of an unsigned integer] SMALLEST_FACTOR(N) ≡Df ∋{K ∈ N+ | 1 ∈ K & DIVIDES(K,N)}

(842) Def 10004: [Increasing sequence of unsigned prime integers factors of an unsigned integer] STANDARD_FACTORIZATION(N) ≡Df {[0,SMALLEST_FACTOR(N)]} +σ ∋{STANDARD_FACTORIZATION(M): M ∈ N | M • SMALLEST_FACTOR(N) = N}

(852) Def 70: [The set of complex numbers] ℂ ≡Df ℝ × ℝ

(852) Def 71: [Complex addition] (X + Y) ≡Df [X&#x + Y&#x,X&#x + Y&#x]

(852) Def 72: [Complex product] (X • Y) ≡Df [X&#x • Y&#x - X&#x • Y&#x,X&#x • Y&#x + X&#x • Y&#x]

(852) Def 73: [The complex norm] ǁX ≡Df √(X&#x • X&#x + X&#x • X&#x)

(852) Def 74: [The complex reciprocal] ⅟X ≡Df [X&#x / (ǁX • ǁX),−(X&#x / (ǁX • ǁX))]

(852) Def 75: [Complex Quotient] (X / Y) ≡Df X • ⅟Y

(852) Def 76: [Complex negative] −(X) ≡Df [−X&#x,−X&#x]

(852) Def 77: [Complex difference] (N - M) ≡Df N + −(M)

(852) Def 78: [Complex zero] 0 ≡Df [0,0]

(852) Def 79: [Complex unity] 1 ≡Df [1,0]

(875) Def 80: [Sums of absolutely convergent infinite series] ∑(F) ≡Df {∑(FɭS): S ⊆ ДF | IsΦ(S)}

(875) Def 81a: [Real functions of a real variable] ℝF ≡Df {F ⊆ ℝ × ℝ | (Is1(F) & ДF) = ℝ}

(875) Def 82: [Pointwise sum of Real Functions] (F •F G) ≡Df {[X,(Fˆ(X) + G)ˆ(X)]: X ∈ ℝ}

(875) Def 83: [Pointwise product of Real Functions] (F •F G) ≡Df {[X,(Fˆ(X) • G)ˆ(X)]: X ∈ ℝ}

(875) Def 84: [Pointwise LUB of a set of Real Functions] LUBS ≡Df {[X,{Fˆ(X): F ∈ S}]: X ∈ ℝ}

(875) Def 85: [Constant zero function] 0ℝF ≡Df {[X,0]: X ∈ ℝ}

(882) Def 86: [Pointwise sums of absolutely convergent infinite series of real functions] ∑ℝF(SER) ≡Df LUB{∑(SERɭS): S ⊆ ДSER | IsΦ(S)}

(882) Def 87: [Greatest lower bound of a set of ordinals] GLB(S) ≡Df {X ∈ ∋S | (∀Y ∈ S | X ∈ Y)}

(882) Def 88: [Block function] BL_F(A,B,C) ≡Df {[X,if A ⊆ X & X ⊆ B then C else 0 end if]: X ∈ ℝ}

(882) Def 89: [Block function integral] BFINT(F) ≡Df ∋{C • (B - A): A ∈ ℝ, B ∈ ℝ, C ∈ ℝ | BL_F(A,B,C) = F}

(882) Def 90: [Block functions] RBF ≡Df {BL_F(A,B,C): A ∈ ℝ, B ∈ ℝ, C ∈ ℝ}

(882) Def 91: [Comparison of real functions] (F >ℝF G) ≡Df F ≠ (G & (∀X ∈ ℝ | Fˆ(X) ⊇ Gˆ(X)))

(882) Def 92: [Lebesgue Upper Integral of a Positive Function] ∫+(F) ≡Df GLB({∑({[N,BFINT(SERˆ(N))]: N ∈ ℕ}): SER ⊆ ℕ × RBF | Is1(SER) & ∑ℝF(SER) >ℝF F})

(882) Def 93: [Positive Part of a real function] POS_PART(F) ≡Df {[X,if Fˆ(X) ⊇ 0 then Fˆ(X) else 0 end if]: X ∈ ℝ}

(882) Def 94: [Pointwise additive inverse of a real function] −ℝFF ≡Df {[X,−(Fˆ(X))]: X ∈ ℝ}

(882) Def 95: [Lebesgue Integral of a real-valued function] ∫ F ≡Df ∫+(POS_PART(F)) - ∫+(POS_PART(−ℝFF))

(882) Def 96: [Continuous real function of a real variable] ≀ℝF(F) ≡Df F ⊆ ℝ × ℝ & Is1(F) & (∀X ∈ ДF, ε ∈ ℝ | (∃δ ∈ ℝ, Y ∈ ДF | δ > 0 & ε ⊇ (0 & ε) ≠ (0 & δ) ⊇ ǁ(X - Y) → ε ⊇ ǁ((Fˆ(X) - F)ˆ(Y))))

(882) Def 97: [Euclidean n-space] ℰ(N) ≡Df {F ⊆ N × ℝ | (Is1(F) & ДF) = N}

(882) Def 98: [Euclidean norm] ǁ(F) ≡Df √∑ℝF(F)

(882) Def 99: [Pointwise difference of Real Functions] (F •F G) ≡Df {[X,(Fˆ(X) - G)ˆ(X)]: X ∈ ДF}

(882) Def 100: [Continuous function on Euclidean n-space] ≀ℝFn(F,N) ≡Df F ⊆ ℰ(N) × ℰ(N) & Is1(F) & (∀X ∈ ДF, ε ∈ ℝ | (∃δ ∈ ℝ | (∀Y ∈ ДF | δ ⊇ (0 & δ) ≠ (0 & ε ⊇ (0 & ε) ≠ (0 & δ) ⊇ ǁ(X •F Y) → ε ⊇ ǁ((Fˆ(X) - F)ˆ(Y))))))

(882) Def 101: [Difference-and-diagonal trick for defining the derivative] DD(F,DF) ≡Df {if Xˆ(0) ≠ Xˆ(1) then (Fˆ(Xˆ(0)) - F)ˆ(Xˆ(1)) / (Xˆ(0) - X)ˆ(1) else DFˆ(Xˆ(0)) end if: X ∈ ℰ(2)}

(882) Def 102: [Derivative of function of a real variable] DER(F) ≡Df ∋{DF ∈ ℝF | ДF = (ДDF & ≀ℝFn(DD(F,DF)ɭ(ДF × ДF),2))}

(882) Def 103: [Complex functions of a complex variable] ℂF ≡Df {F ⊆ ℂ × ℂ | (Is1(F) & ДF) = ℂ}

(882) Def 104: [Complex Euclidean \$n\$-space] ℰ(N) ≡Df {F ⊆ N × ℂ | (Is1(F) & ДF) = N}

(882) Def 105: [Difference-and-diagonal trick, complex case] CDD(F,DF) ≡Df {if Xˆ(0) ≠ Xˆ(1) then (Fˆ(Xˆ(0)) - F)ˆ(Xˆ(1)) / (Xˆ(0) - X)ˆ(1) else DFˆ(Xˆ(0)) end if: X ∈ ℰ(2)}

(882) Def 106: [Continuous function of a complex variable] ≀ℂF(F) ≡Df F ⊆ ℂ × ℂ & Is1(F) & (∀X ∈ ДF, ε ∈ ℝ | (∃δ ∈ ℝ | (∀Y ∈ ДF | δ ⊇ (0 & δ) ≠ (0 & ε ⊇ (0 & ε) ≠ (0 & δ) ⊇ ǁ(X - Y) → ε ⊇ ǁ((Fˆ(X) - F)ˆ(Y))))))

(882) Def 107: [Complex Euclidean norm] CNORM(F) ≡Df √∑ℝF({[M,ǁ(Fˆ(M)) • ǁ(Fˆ(M))]: M ∈ ДF})

(882) Def 108: [Difference of Complex Functions] (F -ℂF G) ≡Df {[X,(Fˆ(X) - G)ˆ(X)]: X ∈ ℂ}

(882) Def 109: [Continuous function on Complex Euclidean n-space] ≀ℂFn(F,N) ≡Df F ⊆ CE(N) × CE(N) & Is1(F) & (∀X ∈ ДF, ε ∈ ℝ | (∃δ ∈ ℝ | (∀Y ∈ ДF | δ ⊇ (0 & δ) ≠ (0 & ε ⊇ (0 & ε) ≠ (0 & δ) ⊇ CNORM(X -ℂF Y) → ε ⊇ CNORM((Fˆ(X) -ℂF F)ˆ(Y))))))

(882) Def 110: [Derivative of function of a complex variable] ↁ(F) ≡Df ∋{DF ∈ ℂF | ДF = (ДDF & ≀ℂFn(CDD(F,DF)ɭ(ДF × ДF),2))}

(882) Def 111: [Open set in the complex plane] IS_OPEN_C_SET(S) ≡Df S ⊆ ℂ & ≀ℂF({[Z,if Z ∈ S then [0,0] else [1,0] end if]: Z ∈ ℂ})

(882) Def 112: [Analytic function of a complex variable] ◈(F) ≡Df (≀ℂF(F) & IS_OPEN_C_SET(ДF) & ↁ(F)) ≠ 0

(882) Def 113: [Complex exponential function] C_EXP_FCN ≡Df ∋{F: F ⊆ ℂ × ℂ | (◈(F) & ↁ(F)) = (F & F)ˆ([0,0]) = [1,0]}

(882) Def 114: [The constant \$pi\$] п ≡Df ∋{X ∈ ℝ | X ⊇ (0 & X) ≠ (0 & C_EXP_FCN([0,X])) = ([1,0] & (∀Y ∈ ℝ | C_EXP_FCN([0,Y]) = [1,0] → Y = X ∨ 0 ⊇ Y))}

(882) Def 115: [Continuous complex function on the reals] ≀(F) ≡Df F ⊆ ℝ × ℂ & Is1(F) & (∀X ∈ ДF, ε ∈ ℝ | (∃δ ∈ ℝ | (∀Y ∈ ДF | δ > 0 & ε ⊇ (0 & ε) ≠ (0 & δ) ⊇ ǁ(X - Y) → ε ⊇ ǁ((Fˆ(X) - F)ˆ(Y)))))

(882) Def 116: [Difference-and-diagonal trick, real-to-complex case] CRDD(F,DF) ≡Df {if Xˆ(0) ≠ Xˆ(1) then (Fˆ(Xˆ(0)) - F)ˆ(Xˆ(1)) / (Xˆ(0) - X)ˆ(1) else DFˆ(Xˆ(0)) end if: X ∈ E(2)}

(882) Def 117: [Continuous complex function on \$E(n)\$] IS_CONTINUOUS_CRENF(F,N) ≡Df F ⊆ E(N) × ℂ & Is1(F) & (∀X ∈ ДF, ε ∈ ℝ | (∃δ ∈ ℝ | (∀Y ∈ ДF | δ > 0 & (ε > 0 & δ ≥ ǁ(X •F Y)) → ε ≥ ǁ((Fˆ(X) -ℂF F)ˆ(Y)))))

(882) Def 118: [Derivative of complex function of a real variable] ↁ(F) ≡Df ∋{DF ∈ ℂF | ДF = (ДDF & IS_CONTINUOUS_CRENF(CRDD(F,DF)ɭ(ДF × ДF),2))}

(882) Def 119: [Real Interval] INTERVAL(A,B) ≡Df {X ∈ ℝ | (A ⊆ X & X) ⊆ B}

(882) Def 120: [Continuously differentiable curve in the complex plane] IS_CD_CURV(F,A,B) ≡Df (≀(F) & ДF) = (INTERVAL(A,B) & 0) ≠ (ↁ(F) & ≀(ↁ(F)))

(882) Def 121: [Complex line integral] ∫⋄(F,CURV,A,B) ≡Df [∫ {[X,if X ∉ INTERVAL(A,B) then 0 else ((Fˆ(CURVˆ(X)) • ↁ(CURV))ˆ(X))&#x end if]: X ∈ ℝ},∫ {[X,if X ∉ INTERVAL(A,B) then 0 else ((Fˆ(CURVˆ(X)) • ↁ(CURV))ˆ(X))&#x end if]: X ∈ ℝ}]