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

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

(12) Def setformer.0: [Witness to difference of two setformers] X_Θ ≡_Df ∋{X ∈ S | E(X) ≠ E₀(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) ∨ E₂(X,Y) ≠ EP₂(X,Y) ∨ ¬(R(X,Y) ↔ PQ(X,Y))}

(15) Def setformer2.0b: [First component of difference witness] X_Θ ≡_Df XY_Θ&#x[1]

(15) Def setformer2.0c: [Second component of difference witness] Y_Θ ≡_Df XY_Θ&#x[2]

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

(18) Def 10: [Is-an-ordinal predicate] Is_O(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 | Is_O(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] MEMBS₂(S) ≡_Df S∪∪S

(27) Def 7h: [Recursively defined iterated members] MEMBS_X(S,X) ≡_Df if X = ∋s_∞ then S else MEMBS₂(∪{MEMBS_X(S,Y): Y ∈ X}) end if

(27) Def 7i: [Ultimate members of a set, first definition] ULT_MEMB₁(S) ≡_Df ∪{MEMBS_X(S,X): X ∈ s_∞}

(29) Def transfinite_induction.0: [Witness for transfinite induction argument] MT_Θ ≡_Df ∋{M: M ∈ ULT_MEMB₁({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] Is_M(F) ≡_Df F = {[X&#x[1],X&#x[2]]: X ∈ F}

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

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

(34) Def 7: [Single-valued map predicate] Is₁(F) ≡_Df Is_M(F) & (∀X ∈ F, Y ∈ F | X&#x[1] = Y&#x[1] → X = Y)

(34) Def 8: [One-one map predicate] 1₁(F) ≡_Df Is₁(F) & (∀X ∈ F, Y ∈ F | X&#x[2] = Y&#x[2] → 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[1]

(38) Def Svm_test.0c: [Second component of witness to non-singlevaluedness] Y_Θ ≡_Df XY_Θ&#x[2]

(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 | P₂(X,Y) & P₂(XP,YP) & A₂(X,Y) = A₂(XP,YP) & B₂(X,Y) ≠ B₂(XP,YP)}

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

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

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

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

(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 | A₃(X,Y,WZ) = A₃(XP,YP,WZP) & B₃(X,Y,WZ) ≠ B₃(XP,YP,WZP) & P₃(X,Y,WZ) & P₃(XP,YP,WZP)}

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

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

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

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

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

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

(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[1]

(41) Def one_1_test.0c: [Second component of witness to map non-one-oneness] Y_Θ ≡_Df XY_Θ&#x[2]

(42) Def one_1_test_2.0a: [Witness to map non-one-oneness, two-variable case] XY_Θ ≡_Df ∋{[[X,Y],[X₂,Y₂]]: X ∈ S, Y ∈ T, X₂ ∈ S, Y₂ ∈ T | ¬(A₂(X,Y) = A₂(X₂,Y₂) ↔ B₂(X,Y) = B₂(X₂,Y₂))}

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

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

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

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

(43) Def one_1_test_3.0a: [Witness to map non one-ness, three-variable case] XYZ_Θ ≡_Df ∋{[[X,[Y,WZ]],[X₂,[Y₂,Z₂]]]: X ∈ S, Y ∈ T, WZ ∈ R, X₂ ∈ S, Y₂ ∈ T, Z₂ ∈ R | P₃(X,Y,WZ) & P₃(X₂,Y₂,Z₂) & (A₃(X,Y,WZ) ≠ A₃(X₂,Y₂,Z₂) ↔ B₃(X,Y,WZ) = B₃(X₂,Y₂,Z₂))}

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

(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[1]&#x[2]&#x[1]

(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[1]&#x[2]&#x[2]

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

(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[2]&#x[2]&#x[1]

(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[2]&#x[2]&#x[2]

(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[1] ∈ A}

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

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

(64) Def 14a: [Inverse Map] F^← ≡_Df {[X&#x[2],X&#x[1]]: 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 ∈ Ω | 1₁(F) & ДF = X & ЯF = S)}

(65) Def 16: [Is-a-cardinal predicate] Is_C(C) ≡_Df Is_O(C) & (∀Y ∈ C, F ∈ Ω | ¬ДF = Y ∨ ¬ЯF = C ∨ ¬Is₁(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[1]

(96) Def fcn_symbol.0c: [Second component of witness to non-singlevaluedness of map inverse] Y_Θ ≡_Df XY_Θ&#x[2]

(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[1]: P ∈ G | P&#x[2] ∈ R}

(203) Def 18: [Finiteness] Is_Φ(S) ≡_Df ¬(∃F ∈ Ω | 1₁(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 ∈ ℕ | Q₁(X)}⁺

(337) Def 24a: [Finite sequences] Is_Φσ(S) ≡_Df {F ⊆ ℕ × S | Is₁(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 ⊆ ℕ × ℕ | Is₁(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 & Is₁(H) & (∀I | I⁺ ∈ ДH → I ∈ ДH & Hˆ(I) ∈ Hˆ(I⁺))} | P&#x[2] ∈ Д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: [?] Is_OΘ ≡_Df ∋{O ∈ #℘S⁺ | Is_O(O) & S = {ORDENM_Θ(X): X ∈ O} & (∀X ∈ O | ORDENM_Θ(X) ≠ S) & 1₁({[X,ORDENM_Θ(X)]: X ∈ O})}

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

(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[1] - P&#x[1]∩P&#x[2],P&#x[2] - P&#x[1]∩P&#x[2]]

(410) Def 28: [Signed addition] (MM +_ℤ NN) ≡_Df [MM&#x[1] + NN&#x[1],MM&#x[2] + NN&#x[2]]^➮ℤ

(410) Def 28a: [Absolute value of a signed integer] ǁ_ℤM ≡_Df M&#x[1]∪M&#x[2]

(410) Def 28b: [Negative of a signed integer] −_ℤM ≡_Df [M&#x[2],M&#x[1]]

(410) Def 29: [Signed Product] (MM •_ℤ NN) ≡_Df [MM&#x[1] • NN&#x[1] + MM&#x[2] • NN&#x[2],MM&#x[1] • NN&#x[2] + NN&#x[1] • MM&#x[2]]^➮ℤ

(410) Def 32: [Signed Difference] (N -_ℤ M) ≡_Df [M&#x[2] + N&#x[1],M&#x[1] + N&#x[2]]^➮ℤ

(410) Def 33: [Sign of a signed integer] Is_≥0ℤ(X) ≡_Df X&#x[1] ⊇ X&#x[2]

(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 F₃({G₄(HH(J,T),ORDEN(J),ORDEN(X),T): J ∈ X |  ∠ (ORDEN(J),ORDEN(X)) & P₄(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 ∉ S₀ & Y ∉ S₀ then S₀ elseif X ∉ S₀ then Y elseif Y ∉ S₀ then X elseif  ∠ (X,Y) then X else Y end if

(503) Def 10032: [Choice of the larger] LARGER_Θ(X,Y) ≡_Df if X ∉ S₀ & Y ∉ S₀ then S₀ elseif X ∉ S₀ then Y elseif Y ∉ S₀ then X elseif  ∠ (X,Y) then Y else X end if

(513) Def 10033: [Upper bounds] UBS_Θ(T) ≡_Df {X ∈ S₀ | (∀Y ∈ T∩S₀ | SMALLER_Θ(Y,X) = Y)}

(513) Def 10034: [Maximum of a set] MAX_Θ(T) ≡_Df ∋({S₀}∪T∩UBS_Θ(T))

(513) Def 10035: [Least upper bound of a set] LUB_Θ(T) ≡_Df ∋({S₀}∪{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({H₁(F_Θ(T)): T ∈ X})

(517) Def transfinite_definition_1_params.0a: [Function defined by a transfinite recursion with supplementary parameter] F2_Θ(X,A) ≡_Df G₂({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[1] •_ℤ Q&#x[2] = P&#x[2] •_ℤ Q&#x[1]

(524) Def 36a: [Nonnegative fraction] Is_≥0Fr(X) ≡_Df Is_≥0ℤ(X&#x[1] •_ℤ X&#x[2])

(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[1] •_ℤ ∋Y&#x[2] +_ℤ ∋Y&#x[1] •_ℤ ∋X&#x[2],∋X&#x[2] •_ℤ ∋Y&#x[2]]^➮ℚ

(530) Def 39: [Rational product] (X •_ℚ Y) ≡_Df [∋X&#x[1] •_ℤ ∋Y&#x[1],∋X&#x[2] •_ℤ ∋Y&#x[2]]^➮ℚ

(530) Def 40: [Rational reciprocal] ⅟_ℚ(X) ≡_Df [∋X&#x[2],∋X&#x[1]]^➮ℚ

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

(530) Def 42: [Rational negative] −_ℚX ≡_Df [−_ℤ∋X&#x[1],∋X&#x[2]]^➮ℚ

(530) Def 43: [Nonnegative Rational] Is_≥0ℚ(X) ≡_Df Is_≥0ℤ(∋X&#x[1] •_ℤ ∋X&#x[2])

(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 = ℕ & Is₁(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[1],P&#x[2] +_ℚ Yˆ(P&#x[1])]: P ∈ X}

(640) Def 50: [Pointwise additive inverse of rational sequence]  −_ℚ^ℕX ≡_Df {[P&#x[1],−_ℚP&#x[2]]: P ∈ X}

(640) Def 51: [Pointwise absolute value of rational sequence] ǁ_ℚ^ℕX ≡_Df {[P&#x[1],ǁ_ℚP&#x[2]]: 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[1],P&#x[2] •_ℚ Yˆ(P&#x[1])]: 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 = ℕ & Is₁(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[1],P&#x[2] +_ℝ Yˆ(P&#x[1])]: P ∈ X}

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

(816) Def 76: [Absolute values of real function] RES_ABS(X) ≡_Df {[P&#x[1],RE_ABS(P&#x[2])]: 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[1],P&#x[2] •_ℝ Yˆ(P&#x[1])]: 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 ⊆ ℝ & Is₁(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[1] +_ℝ Y&#x[1],X&#x[2] +_ℝ Y&#x[2]]

(852) Def 72: [Complex product] (X •_ℂ Y) ≡_Df [X&#x[1] •_ℝ Y&#x[1] -_ℝ X&#x[2] •_ℝ Y&#x[2],X&#x[1] •_ℝ Y&#x[2] +_ℝ X&#x[2] •_ℝ Y&#x[1]]

(852) Def 73: [The complex norm] ǁ_ℂX ≡_Df √(X&#x[1] •_ℝ X&#x[1] +_ℝ X&#x[2] •_ℝ X&#x[2])

(852) Def 74: [The complex reciprocal] ⅟_ℂX ≡_Df [X&#x[1] /_ℝ (ǁ_ℂX •_ℝ ǁ_ℂX),−_ℝ(X&#x[2] /_ℝ (ǁ_ℂX •_ℝ ǁ_ℂX))]

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

(852) Def 76: [Complex negative] −_ℂ(X) ≡_Df [−_ℝX&#x[1],−_ℝX&#x[2]]

(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 ⊆ ℝ × ℝ | (Is₁(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 | Is₁(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 ⊆ ℝ × ℝ & Is₁(F) & (∀X ∈ ДF, ε ∈ ℝ | (∃δ ∈ ℝ, Y ∈ ДF | δ >_ℝ 0 & ε ⊇ (0_ℝ & ε) ≠ (0_ℝ & δ) ⊇ ǁ_ℝ(X -_ℝ Y) → ε ⊇ ǁ_ℝ((Fˆ(X) -_ℝ F)ˆ(Y))))

(882) Def 97: [Euclidean n-space] ℰ(N) ≡_Df {F ⊆ N × ℝ | (Is₁(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] ≀_ℝFⁿ(F,N) ≡_Df F ⊆ ℰ(N) × ℰ(N) & Is₁(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 & ≀_ℝFⁿ(DD(F,DF)ɭ(ДF × ДF),2))}

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

(882) Def 104: [Complex Euclidean $n$-space] ℰ_ℂ(N) ≡_Df {F ⊆ N × ℂ | (Is₁(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 ⊆ ℂ × ℂ & Is₁(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] ≀_ℂFⁿ(F,N) ≡_Df F ⊆ CE(N) × CE(N) & Is₁(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 & ≀_ℂFⁿ(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 ⊆ ℝ × ℂ & Is₁(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) × ℂ & Is₁(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[1] end if]: X ∈ ℝ},∫ {[X,if X ∉ INTERVAL(A,B) then 0_ℝ else ((Fˆ(CURVˆ(X)) •_ℂ ↁ_ℂ(CURV))ˆ(X))&#x[2] end if]: X ∈ ℝ}]