Arithmetization — Explore equations

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Equation and object guide

All 243 stable expressions, 40 formal objects, 29 source references, and 9 disclosed corrections are indexed here.

243 expression records

Expression 1

[f] \neq 0_{R}

Conventional reading: the real-equivalence class of f is not equal to real zero

Meaning here: This states that the real-equivalence class of f is not equal to real zero. The frozen source prints rational zero, but the surrounding construction compares real-equivalence classes; the reader therefore says real zero and discloses the correction.

1 occurrence

Occurrence 1: cauchy.tex, line 150, column 26

Expression 2

(\forall ε > 0)

Conventional reading: for every epsilon greater than zero

Meaning here: This is the universal positive-epsilon prefix of the following Cauchy or convergence condition.

1 occurrence

Occurrence 1: cauchy.tex, line 77, column 47

Expression 3

{[f]}_{≎}

Conventional reading: the real-equivalence class of f

Meaning here: This denotes the real-equivalence class of f in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 133, column 43

Expression 4

\begin{matrix} i + (j + k) & = [a_{1}, b_{1}] + ([a_{2}, b_{2}] + [a_{3}, b_{3}]) \\ = [a_{1}, b_{1}] + [a_{2} + a_{3}, b_{2} + b_{3}] \\ = [a_{1} + (a_{2} + a_{3}), b_{1} + (b_{2} + b_{3})] \\ = [(a_{1} + a_{2}) + a_{3}, (b_{1} + b_{2}) + b_{3}] \\ = [a_{1} + a_{2}, b_{1} + b_{2}] + [a_{3}, b_{3}] \\ = ([a_{1}, b_{1}] + [a_{2}, b_{2}]) + [a_{3}, b_{3}] \\ = (i + j) + k \end{matrix}

Conventional reading: seven-line associativity calculation. First, i plus the quantity j plus k equals the integer-equivalence class of a sub one comma b sub one, plus the sum of the classes of a sub two comma b sub two and a sub three comma b sub three. Second, combine the last two classes coordinatewise. Third, reassociate both natural-number coordinates. Fourth, use associativity of natural-number addition. Fifth, split the resulting class back into two classes. Sixth, identify those classes as i, j, and k. Seventh, the result is the quantity i plus j, plus k

Meaning here: This seven-line calculation proves associativity of addition for integer-equivalence classes.

1 occurrence

Occurrence 1: checking-details.tex, line 50, column 1

Expression 5

⟨ a, b ⟩ \sim ⟨ c, d ⟩ iff a + d = c + b

Conventional reading: the ordered pair a comma b is integer-equivalent to the ordered pair c comma d if and only if a plus d equals c plus b

Meaning here: This states that the ordered pair a comma b is integer-equivalent to the ordered pair c comma d if and only if a plus d equals c plus b.

1 occurrence

Occurrence 1: integers.tex, line 25, column 1

Expression 6

\emptyset \neq λ

Conventional reading: the empty set is not equal to lambda

Meaning here: This states that the empty set is not equal to lambda.

1 occurrence

Occurrence 1: cuts.tex, line 65, column 1

Expression 7

Q

Conventional reading: the rational numbers

Meaning here: This denotes the rational numbers in the construction of the rationals, the Dedekind-cut construction of the reals, the ordered-ring and ordered-field verification, and the Cauchy-sequence construction of the reals.

10 occurrences

Expression 8

λ \subseteq β

Conventional reading: lambda is a subset of beta

Meaning here: This states that lambda is a subset of beta.

1 occurrence

Occurrence 1: cuts.tex, line 77, column 325

Expression 9

⟨ a, b ⟩ \sim ⟨ c, d ⟩

Conventional reading: the ordered pair a comma b is integer-equivalent to the ordered pair c comma d

Meaning here: This states that the ordered pair a comma b is integer-equivalent to the ordered pair c comma d.

1 occurrence

Occurrence 1: integers.tex, line 34, column 27

Expression 10

\sqrt{2} = {p \in Q : p^{2} < 2 or p < 0}

Conventional reading: the square root of two equals the cut of all rational p such that p squared is less than two or p is negative

Meaning here: This states that the square root of two equals the cut of all rational p such that p squared is less than two or p is negative.

1 occurrence

Occurrence 1: cuts.tex, line 38, column 24

Expression 11

q \in Q

Conventional reading: q is an element of the rational numbers

Meaning here: This states that q is an element of the rational numbers.

2 occurrences

Expression 12

\begin{matrix} α \times β & = {\begin{matrix} - α \times - β & if α < 0_{R} and β < 0_{R} \\ - (- α \times β) & if α < 0_{R} and β > 0_{R} \\ - (α \times - β) & if α > 0_{R} and β < 0_{R} \end{matrix} \end{matrix}

Conventional reading: alpha times beta is defined in three remaining sign cases. If alpha and beta are both negative, use negative alpha times negative beta. If alpha is negative and beta is positive, take the negative of negative alpha times beta. If alpha is positive and beta is negative, take the negative of alpha times negative beta

Meaning here: These three cases extend multiplication of Dedekind cuts to the remaining sign combinations.

1 occurrence

Occurrence 1: cuts.tex, line 101, column 1

Expression 13

⟨ m, n ⟩

Conventional reading: the ordered pair m comma n

Meaning here: This denotes the ordered pair m comma n in the construction of the integers.

1 occurrence

Occurrence 1: integers.tex, line 47, column 189

Expression 14

q \in β

Conventional reading: q is an element of beta

Meaning here: This states that q is an element of beta.

1 occurrence

Occurrence 1: checking-details.tex, line 161, column 61

Expression 15

x = p + (x - p) \in α + β

Conventional reading: x equals p plus the quantity x minus p, and x belongs to alpha plus beta

Meaning here: This states that x equals p plus the quantity x minus p, and x belongs to alpha plus beta.

1 occurrence

Occurrence 1: checking-details.tex, line 162, column 45

Expression 16

p

Conventional reading: p

Meaning here: This is the reusable atomic notation spoken as p. Its exact mathematical role is supplied separately for every bound source occurrence.

2 occurrences

Expression 17

p_{R}

Conventional reading: p under the real embedding

Meaning here: This denotes p under the real embedding in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 185, column 44

Expression 18

f (n) = {\begin{matrix} 1 & if n is odd \\ 0 & if n is even \end{matrix}

Conventional reading: f of n equals one when n is odd, and zero when n is even

Meaning here: This states that f of n equals one when n is odd, and zero when n is even.

1 occurrence

Occurrence 1: cauchy.tex, line 64, column 1

Expression 19

a_{n} = \frac{f (n) + g (n)}{2}

Conventional reading: a sub n equals the average of f of n and g of n

Meaning here: This states that a sub n equals the average of f of n and g of n.

1 occurrence

Occurrence 1: cauchy.tex, line 195, column 13

Expression 20

g (0) \neq f (0)

Conventional reading: g of zero is not equal to f of zero

Meaning here: This states that g of zero is not equal to f of zero.

1 occurrence

Occurrence 1: cauchy.tex, line 102, column 57

Expression 21

α \times β

Conventional reading: alpha times beta

Meaning here: This denotes alpha times beta in the ordered-ring and ordered-field verification.

1 occurrence

Occurrence 1: checking-details.tex, line 171, column 1

Expression 22

(\forall α \in S) α \subseteq ⋃ S = λ

Conventional reading: for every alpha in S, alpha is a subset of the union of S, which equals lambda

Meaning here: This states that for every alpha in S, alpha is a subset of the union of S, which equals lambda.

1 occurrence

Occurrence 1: cuts.tex, line 76, column 42

Expression 23

j

Conventional reading: j

Meaning here: This is the reusable atomic notation spoken as j. Its exact mathematical role is supplied separately for every bound source occurrence.

3 occurrences

Expression 24

d

Conventional reading: d

Meaning here: This is the reusable atomic notation spoken as d. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: integers.tex, line 24, column 94

Expression 25

1.414

Conventional reading: one point four one four

Meaning here: This denotes one point four one four in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 92, column 38

Expression 26

m \leq n \leftrightarrow m_{Z} \leq n_{Z}

Conventional reading: m is at most n if and only if the integer embedding of m is at most the integer embedding of n

Meaning here: This states that m is at most n if and only if the integer embedding of m is at most the integer embedding of n.

1 occurrence

Occurrence 1: integers.tex, line 86, column 49

Expression 27

n - m

Conventional reading: n minus m

Meaning here: This denotes n minus m in the construction of the integers.

2 occurrences

Expression 28

1.4

Conventional reading: one point four

Meaning here: This denotes one point four in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 92, column 31

Expression 29

\begin{matrix} p^{2} & < 2 \\ 2 p^{2} + 4 p + 2 & < p^{2} + 4 p + 4 \\ 4 p^{2} + 8 p + 4 & < 2 (p^{2} + 4 p + 4) \\ {(2 p + 2)}^{2} & < 2 {(p + 2)}^{2} \\ \frac{{(2 p + 2)}^{2}}{{(p + 2)}^{2}} & < 2 \\ q^{2} & < 2 \end{matrix}

Conventional reading: six-line calculation proving q squared is less than two: p squared is less than two; two times p squared plus four times p plus two is less than p squared plus four times p plus four; four times p squared plus eight times p plus four is less than two times open parenthesis p squared plus four times p plus four close parenthesis; the square of the quantity two times p plus two is less than two times the square of the quantity p plus two; the square of the fraction with numerator two times p plus two and denominator p plus two is less than two; therefore q squared is less than two

Meaning here: This six-line calculation proves that the constructed rational q still has square strictly below two.

1 occurrence

Occurrence 1: checking-details.tex, line 197, column 1

Expression 30

n

Conventional reading: n

Meaning here: This is the reusable atomic notation spoken as n. Its exact mathematical role is supplied separately for every bound source occurrence.

11 occurrences

Expression 31

a, b \in N

Conventional reading: a and b are natural numbers

Meaning here: This states that a and b are natural numbers.

1 occurrence

Occurrence 1: checking-details.tex, line 65, column 59

Expression 32

⟨ n, m ⟩

Conventional reading: the ordered pair n comma m

Meaning here: This denotes the ordered pair n comma m in the construction of the integers.

1 occurrence

Occurrence 1: integers.tex, line 16, column 100

Expression 33

< \sqrt{2}

Conventional reading: less than the square root of two

Meaning here: This denotes less than the square root of two in the Dedekind-cut construction of the reals.

1 occurrence

Occurrence 1: cuts.tex, line 19, column 1

Expression 34

f : N \to Q

Conventional reading: f is a function from the natural numbers to the rational numbers

Meaning here: This states that f is a function from the natural numbers to the rational numbers.

1 occurrence

Occurrence 1: cauchy.tex, line 84, column 14

Expression 35

{[⟨ m, n ⟩]}_{\sim}

Conventional reading: the integer-equivalence class of the ordered pair m comma n

Meaning here: This denotes the integer-equivalence class of the ordered pair m comma n in the construction of the integers.

1 occurrence

Occurrence 1: integers.tex, line 47, column 336

Expression 36

p, q \in N

Conventional reading: p and q are natural numbers

Meaning here: This states that p and q are natural numbers.

1 occurrence

Occurrence 1: reals.tex, line 55, column 60

Expression 37

\sqrt{2} = \frac{m}{n}

Conventional reading: the square root of two equals the fraction with numerator m and denominator n

Meaning here: This states that the square root of two equals the fraction with numerator m and denominator n.

1 occurrence

Occurrence 1: reals.tex, line 30, column 56

Expression 38

(a \times b)

Conventional reading: a times b

Meaning here: This denotes a times b in the construction of the integers.

1 occurrence

Occurrence 1: integers.tex, line 55, column 44

Expression 39

\begin{matrix} - α & = {p - q : p < 0 \land q \notin α} \end{matrix}

Conventional reading: negative alpha is the set of all p minus q such that p is negative and q is not in alpha

Meaning here: This states that negative alpha is the set of all p minus q such that p is negative and q is not in alpha.

1 occurrence

Occurrence 1: cuts.tex, line 97, column 1

Expression 40

(f + g) (n) = f (n) + g (n)

Conventional reading: f plus g, evaluated at n, equals f of n plus g of n

Meaning here: This states that f plus g, evaluated at n, equals f of n plus g of n.

1 occurrence

Occurrence 1: cauchy.tex, line 144, column 7

Expression 41

f

Conventional reading: f

Meaning here: This is the reusable atomic notation spoken as f. Its exact mathematical role is supplied separately for every bound source occurrence.

9 occurrences

Expression 42

{(f (n))}_{R} = [c_{f (n)}] < [f] + [(h - f)] = [h],

Conventional reading: the real embedding of f of n equals the class of the constant sequence at f of n, which is less than the class of f plus the class of h minus f, which equals the class of h

Meaning here: This states that the real embedding of f of n equals the class of the constant sequence at f of n, which is less than the class of f plus the class of h minus f, which equals the class of h.

1 occurrence

Occurrence 1: cauchy.tex, line 221, column 1

Expression 43

\begin{matrix} {(m + n)}_{Z} & = m_{Z} + n_{Z} \\ {(m \times n)}_{Z} & = m_{Z} \times n_{Z} \\ m \leq n & \leftrightarrow m_{Z} \leq n_{Z} \end{matrix}

Conventional reading: three embedding laws: the integer embedding of m plus n equals the sum of the integer embeddings of m and n; the integer embedding of m times n equals their embedded product; and m is at most n if and only if embedded m is at most embedded n

Meaning here: These three laws state that the natural-number embedding into the integers preserves addition, multiplication, and order.

1 occurrence

Occurrence 1: integers.tex, line 66, column 1

Expression 44

{(m + n)}_{Z} = m_{Z} + n_{Z}

Conventional reading: the integer embedding of m plus n equals the sum of the integer embeddings of m and n

Meaning here: This states that the integer embedding of m plus n equals the sum of the integer embeddings of m and n.

1 occurrence

Occurrence 1: integers.tex, line 86, column 12

Expression 45

0, 1, 0, 1, 0, 1, 0, \dots

Conventional reading: zero, one, zero, one, zero, one, zero, and so on

Meaning here: This denotes zero, one, zero, one, zero, one, zero, and so on in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 70, column 49

Expression 46

⟨ a, b ⟩ \sim ⟨ c, d ⟩ \sim ⟨ m, n ⟩

Conventional reading: the ordered pair a comma b is integer-equivalent to the ordered pair c comma d, and that pair is integer-equivalent to the ordered pair m comma n

Meaning here: This states that the ordered pair a comma b is integer-equivalent to the ordered pair c comma d, and that pair is integer-equivalent to the ordered pair m comma n.

1 occurrence

Occurrence 1: integers.tex, line 36, column 31

Expression 47

x

Conventional reading: x

Meaning here: This is the reusable atomic notation spoken as x. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: reals.tex, line 60, column 39

Expression 48

a + d = c + b

Conventional reading: a plus d equals c plus b

Meaning here: This states that a plus d equals c plus b.

2 occurrences

Expression 49

{(g (n))}_{R} \leq [h]

Conventional reading: the real embedding of g of n is at most the real-equivalence class of h

Meaning here: This states that the real embedding of g of n is at most the real-equivalence class of h.

1 occurrence

Occurrence 1: cauchy.tex, line 226, column 355

Expression 50

Z \times (Z ∖ {0_{Z}})

Conventional reading: the Cartesian product of the integers with the nonzero integers

Meaning here: This denotes the Cartesian product of the integers with the nonzero integers in the construction of the rationals.

2 occurrences

Expression 51

\begin{matrix} f (n + 1) & = {\begin{matrix} a_{n} & if (\forall h \in S) [h] \leq {(a_{n})}_{R} \\ f (n) & otherwise \end{matrix} \\ g (n + 1) & = {\begin{matrix} a_{n} & if (\exists h \in S) [h] \geq {(a_{n})}_{R} \\ g (n) & otherwise \end{matrix} \end{matrix}

Conventional reading: two recursive clauses. f of n plus one equals a sub n if every h in S has class at most the real embedding of a sub n, and otherwise equals f of n. g of n plus one equals a sub n if some h in S has class at least the real embedding of a sub n, and otherwise equals g of n

Meaning here: These two piecewise recursion clauses define upper and lower rational approximation sequences for the least-upper-bound proof.

1 occurrence

Occurrence 1: cauchy.tex, line 198, column 1

Expression 52

λ ⊊ Q

Conventional reading: lambda is a proper subset of the rational numbers

Meaning here: This states that lambda is a proper subset of the rational numbers.

1 occurrence

Occurrence 1: cuts.tex, line 68, column 1

Expression 53

q < q_{1}

Conventional reading: q is less than q sub one

Meaning here: This states that q is less than q sub one.

1 occurrence

Occurrence 1: checking-details.tex, line 166, column 25

Expression 54

\times

Conventional reading: times

Meaning here: This is the multiplication operation of the ring or field under discussion.

2 occurrences

Expression 55

p + q \in α + β

Conventional reading: p plus q is an element of alpha plus beta

Meaning here: This states that p plus q is an element of alpha plus beta.

1 occurrence

Occurrence 1: checking-details.tex, line 164, column 18

Expression 56

2 r^{2} = n^{2}

Conventional reading: two times r squared equals n squared

Meaning here: This states that two times r squared equals n squared.

1 occurrence

Occurrence 1: reals.tex, line 61, column 50

Expression 57

p, q \in Q

Conventional reading: p and q are rational numbers

Meaning here: This states that p and q are rational numbers.

1 occurrence

Occurrence 1: cuts.tex, line 32, column 32

Expression 58

m^{2} = 2 n^{2}

Conventional reading: m squared equals two times n squared

Meaning here: This states that m squared equals two times n squared.

1 occurrence

Occurrence 1: reals.tex, line 50, column 7

Expression 59

\sqrt{2} \notin Q

Conventional reading: the square root of two is not an element of the rational numbers

Meaning here: This states that the square root of two is not an element of the rational numbers.

1 occurrence

Occurrence 1: reals.tex, line 26, column 35

Expression 60

p_{1} \in α

Conventional reading: p sub one is an element of alpha

Meaning here: This states that p sub one is an element of alpha.

1 occurrence

Occurrence 1: checking-details.tex, line 165, column 34

Expression 61

i, j, k \in Z

Conventional reading: i, j, and k are integers

Meaning here: This states that i, j, and k are integers.

1 occurrence

Occurrence 1: checking-details.tex, line 44, column 5

Expression 62

b

Conventional reading: b

Meaning here: This is the reusable atomic notation spoken as b. Its exact mathematical role is supplied separately for every bound source occurrence.

2 occurrences

Expression 63

c_{q} (n) = q

Conventional reading: c sub q of n equals q

Meaning here: This states that c sub q of n equals q.

1 occurrence

Occurrence 1: cauchy.tex, line 138, column 19

Expression 64

r \in S

Conventional reading: r is an element of S

Meaning here: This states that r is an element of S.

1 occurrence

Occurrence 1: cauchy.tex, line 183, column 44

Expression 65

q = \frac{2 p + 2}{p + 2}

Conventional reading: q equals the fraction with numerator two times p plus two and denominator p plus two

Meaning here: This states that q equals the fraction with numerator two times p plus two and denominator p plus two.

1 occurrence

Occurrence 1: checking-details.tex, line 187, column 67

Expression 66

(\forall β \in R) ((\forall α \in S) α \subseteq β \to λ \subseteq β)

Conventional reading: for every real cut beta, if every alpha in S is a subset of beta, then lambda is a subset of beta

Meaning here: This states that for every real cut beta, if every alpha in S is a subset of beta, then lambda is a subset of beta.

1 occurrence

Occurrence 1: cuts.tex, line 51, column 54

Expression 67

\begin{matrix} {(m \times n)}_{Z} & = {[m \times n, 0]}_{\sim} \\ = {[m \times n + 0 \times 0, m \times 0 + 0 \times n]}_{\sim} \\ = {[m, 0]}_{\sim} \times {[n, 0]}_{\sim} \\ = m_{Z} \times n_{Z} \end{matrix}

Conventional reading: four-line calculation for multiplication under the integer embedding. The integer embedding of m times n is the class with coordinates m times n and zero; by the class-product definition this is the class with first coordinate m times n plus zero times zero and second coordinate m times zero plus zero times n; this is the product of the classes of m comma zero and n comma zero; therefore it equals embedded m times embedded n

Meaning here: This four-line calculation proves that the natural-number embedding into the integers preserves multiplication.

1 occurrence

Occurrence 1: integers.tex, line 76, column 2

Expression 68

{p \in Q : p^{2} < 2 or p < 0}

Conventional reading: the set of rational p such that p squared is less than two or p is negative

Meaning here: This states that the set of rational p such that p squared is less than two or p is negative.

1 occurrence

Occurrence 1: reals.tex, line 77, column 1

Expression 69

p \in λ

Conventional reading: p is an element of lambda

Meaning here: This states that p is an element of lambda.

3 occurrences

Expression 70

α

Conventional reading: alpha

Meaning here: This is the reusable atomic notation spoken as alpha. Its exact mathematical role is supplied separately for every bound source occurrence.

10 occurrences

Expression 71

\sim

Conventional reading: is integer-equivalent to

Meaning here: This is the integer-equivalence relation on ordered pairs of natural numbers.

6 occurrences

Expression 72

f (n)

Conventional reading: f of n

Meaning here: This denotes f of n in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 59, column 43

Expression 73

h : N \to Q

Conventional reading: h is a function from the natural numbers to the rational numbers

Meaning here: This states that h is a function from the natural numbers to the rational numbers.

1 occurrence

Occurrence 1: cauchy.tex, line 112, column 29

Expression 74

x - p < q

Conventional reading: x minus p is less than q

Meaning here: This states that x minus p is less than q.

1 occurrence

Occurrence 1: checking-details.tex, line 162, column 6

Expression 75

3

Conventional reading: three

Meaning here: This is the reusable atomic notation spoken as three. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: reals.tex, line 80, column 83

Expression 76

x - p \in β

Conventional reading: x minus p is an element of beta

Meaning here: This states that x minus p is an element of beta.

1 occurrence

Occurrence 1: checking-details.tex, line 162, column 22

Expression 77

\begin{matrix} {[a, b]}_{\sim} + {[c, d]}_{\sim} & = {[a + c, b + d]}_{\sim} \\ {[a, b]}_{\sim} \times {[c, d]}_{\sim} & = {[a c + b d, a d + b c]}_{\sim} \\ {[a, b]}_{\sim} \leq {[c, d]}_{\sim} & iff a + d \leq b + c \end{matrix}

Conventional reading: three definitions on integer-equivalence classes. Their sum is the class with first coordinate a plus c and second coordinate b plus d. Their product is the class with first coordinate a times c plus b times d and second coordinate a times d plus b times c. The class of a comma b is at most the class of c comma d if and only if a plus d is at most b plus c

Meaning here: These clauses define addition, multiplication, and order on integer-equivalence classes.

1 occurrence

Occurrence 1: integers.tex, line 50, column 2

Expression 78

Z = N^{2} /_{\sim}

Conventional reading: the set of integers is the quotient of the natural-number pairs by integer equivalence

Meaning here: This defines the integers as the quotient of ordered natural-number pairs by integer equivalence.

1 occurrence

Occurrence 1: integers.tex, line 42, column 111

Expression 79

\begin{matrix} p^{2} & < 2 \\ p^{2} + 2 p & < 2 + 2 p \\ p (p + 2) & < 2 + 2 p \\ p & < \frac{2 + 2 p}{p + 2} = q \end{matrix}

Conventional reading: four-line calculation proving p is less than q: p squared is less than two; p squared plus two times p is less than two plus two times p; p times open parenthesis p plus two close parenthesis is less than two plus two times p; therefore p is less than the fraction two plus two times p over p plus two, which equals q

Meaning here: This four-line calculation proves that the constructed rational q is strictly greater than p while its square remains below two.

1 occurrence

Occurrence 1: checking-details.tex, line 190, column 1

Expression 80

\frac{1}{10^{n}}

Conventional reading: the fraction with numerator one and denominator ten to the power n

Meaning here: This denotes the fraction with numerator one and denominator ten to the power n in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 94, column 20

Expression 81

{[m, n]}_{\sim} = {⟨ a, b ⟩ \in N^{2} : ⟨ a, b ⟩ \sim ⟨ m, n ⟩}

Conventional reading: the integer-equivalence class of m comma n equals the set of natural-number pairs a comma b that are integer-equivalent to m comma n

Meaning here: This states that the integer-equivalence class of m comma n equals the set of natural-number pairs a comma b that are integer-equivalent to m comma n.

1 occurrence

Occurrence 1: integers.tex, line 48, column 2

Expression 82

λ

Conventional reading: lambda

Meaning here: This is the reusable atomic notation spoken as lambda. Its exact mathematical role is supplied separately for every bound source occurrence.

5 occurrences

Expression 83

⟨ i, j ⟩

Conventional reading: the ordered pair i comma j

Meaning here: This denotes the ordered pair i comma j in the construction of the rationals.

1 occurrence

Occurrence 1: rationals.tex, line 20, column 44

Expression 84

n \in N

Conventional reading: n is an element of the natural numbers

Meaning here: This states that n is an element of the natural numbers.

4 occurrences

Expression 85

x^{2}

Conventional reading: x to the power two

Meaning here: This denotes x to the power two in the irrationality of the square root of two.

1 occurrence

Occurrence 1: reals.tex, line 60, column 56

Expression 86

ℓ

Conventional reading: ell

Meaning here: This is the reusable atomic notation spoken as ell. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: cauchy.tex, line 91, column 47

Expression 87

α \in S

Conventional reading: alpha is an element of S

Meaning here: This states that alpha is an element of S.

4 occurrences

Expression 88

p_{R}

Conventional reading: p under the real embedding

Meaning here: This denotes p under the real embedding in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 183, column 1

Expression 89

0

Conventional reading: zero

Meaning here: This is the reusable atomic notation spoken as zero. Its exact mathematical role is supplied separately for every bound source occurrence.

7 occurrences

Expression 90

Z

Conventional reading: the integers

Meaning here: This denotes the integers in the construction of the integers, the construction of the rationals, the ordered-ring and ordered-field verification, and the Cauchy-sequence construction of the reals.

14 occurrences

Expression 91

⟨ a, b ⟩ \sim ⟨ m, n ⟩

Conventional reading: the ordered pair a comma b is integer-equivalent to the ordered pair m comma n

Meaning here: This states that the ordered pair a comma b is integer-equivalent to the ordered pair m comma n.

1 occurrence

Occurrence 1: integers.tex, line 36, column 198

Expression 92

m

Conventional reading: m

Meaning here: This is the reusable atomic notation spoken as m. Its exact mathematical role is supplied separately for every bound source occurrence.

6 occurrences

Expression 93

(f \times g)

Conventional reading: the pointwise product f times g

Meaning here: This denotes the pointwise product f times g in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 146, column 13

Expression 94

{(i + j)}_{Q} = i_{Q} + j_{Q}

Conventional reading: the rational embedding of i plus j equals the sum of the rational embeddings of i and j

Meaning here: This states that the rational embedding of i plus j equals the sum of the rational embeddings of i and j.

1 occurrence

Occurrence 1: rationals.tex, line 70, column 11

Expression 95

⟨ 3, 2 ⟩ \neq ⟨ 6, 4 ⟩

Conventional reading: the ordered pair three comma two is not equal to the ordered pair six comma four

Meaning here: This states that the ordered pair three comma two is not equal to the ordered pair six comma four.

1 occurrence

Occurrence 1: rationals.tex, line 25, column 42

Expression 96

N \to Q

Conventional reading: the function type from the natural numbers to the rational numbers

Meaning here: This is the function type whose domain is the natural numbers and whose codomain is the rational numbers.

2 occurrences

Expression 97

p_{R} = {q \in Q : q < p}

Conventional reading: the real embedding of rational p is the cut of all rational q less than p

Meaning here: This states that the real embedding of rational p is the cut of all rational q less than p.

1 occurrence

Occurrence 1: cuts.tex, line 86, column 60

Expression 98

1

Conventional reading: one

Meaning here: This is the reusable atomic notation spoken as one. Its exact mathematical role is supplied separately for every bound source occurrence.

4 occurrences

Expression 99

ε \in Q

Conventional reading: epsilon is an element of the rational numbers

Meaning here: This states that epsilon is an element of the rational numbers.

2 occurrences

Expression 100

f (n) = 0

Conventional reading: f of n equals zero

Meaning here: This states that f of n equals zero.

1 occurrence

Occurrence 1: cauchy.tex, line 128, column 5

Expression 101

\begin{matrix} {[a, b]}_{∽} + {[c, d]}_{∽} & = {[a d + b c, b d]}_{∽} \\ {[a, b]}_{∽} \times {[c, d]}_{∽} & = {[a c, b d]}_{∽} . \\ To define r \leq s on these rationals, we use the fact that r \leq s iff s - r is not negative, i.e., r - s can be written as \frac{i}{j} with i non-negative and j positive: & {[a, b]}_{∽} \leq {[c, d]}_{∽} & iff {[c, d]}_{∽} - {[a, b]}_{∽} = {[i_{Z}, j_{Z}]}_{∽} \end{matrix}

Conventional reading: definitions of rational-class arithmetic and order. The sum of the classes a comma b and c comma d is the class with numerator a times d plus b times c and denominator b times d. Their product is the class with numerator a times c and denominator b times d. For order, the first class is at most the second exactly when their difference is represented by a nonnegative integer numerator i and positive integer denominator j

Meaning here: These clauses define addition, multiplication, and order on rational-equivalence classes.

1 occurrence

Occurrence 1: rationals.tex, line 50, column 1

Expression 102

R

Conventional reading: the real numbers

Meaning here: This denotes the real numbers in the Dedekind-cut construction of the reals, and the ordered-ring and ordered-field verification.

6 occurrences

Expression 103

{[i, j]}_{∽}

Conventional reading: the equivalence class of i comma j modulo rational equivalence

Meaning here: This denotes the equivalence class of i comma j modulo rational equivalence in the construction of the rationals.

1 occurrence

Occurrence 1: rationals.tex, line 48, column 7

Expression 104

[j] < [g]

Conventional reading: the real-equivalence class of j is less than the real-equivalence class of g

Meaning here: This states that the real-equivalence class of j is less than the real-equivalence class of g.

1 occurrence

Occurrence 1: cauchy.tex, line 226, column 139

Expression 105

(f - g) (n) = f (n) - g (n)

Conventional reading: f minus g, evaluated at n, equals f of n minus g of n

Meaning here: This states that f minus g, evaluated at n, equals f of n minus g of n.

1 occurrence

Occurrence 1: cauchy.tex, line 118, column 32

Expression 106

\frac{m}{n}

Conventional reading: the fraction with numerator m and denominator n

Meaning here: This denotes the fraction with numerator m and denominator n in the irrationality of the square root of two.

1 occurrence

Occurrence 1: reals.tex, line 68, column 10

Expression 107

⟨ a, b ⟩ \sim ⟨ a, b ⟩

Conventional reading: the ordered pair a comma b is integer-equivalent to the ordered pair a comma b

Meaning here: This states that the ordered pair a comma b is integer-equivalent to the ordered pair a comma b.

1 occurrence

Occurrence 1: integers.tex, line 32, column 32

Expression 108

β \in R

Conventional reading: beta is a real number, meaning a Dedekind cut

Meaning here: This states that beta is a real number, meaning a Dedekind cut.

1 occurrence

Occurrence 1: cuts.tex, line 77, column 90

Expression 109

q \in α

Conventional reading: q is an element of alpha

Meaning here: This states that q is an element of alpha.

3 occurrences

Expression 110

N

Conventional reading: the natural numbers

Meaning here: This denotes the natural numbers in the construction of the integers, the ordered-ring and ordered-field verification, and the Cauchy-sequence construction of the reals.

6 occurrences

Expression 111

k = [a_{3}, b_{3}]

Conventional reading: k equals the equivalence class of a sub three comma b sub three

Meaning here: This states that k equals the equivalence class of a sub three comma b sub three.

2 occurrences

Expression 112

α \leq β iff α \subseteq β

Conventional reading: alpha is at most beta if and only if alpha is a subset of beta

Meaning here: This states that alpha is at most beta if and only if alpha is a subset of beta.

1 occurrence

Occurrence 1: cuts.tex, line 44, column 1

Expression 113

(f + g)

Conventional reading: the pointwise sum f plus g

Meaning here: This denotes the pointwise sum f plus g in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 145, column 55

Expression 114

\begin{matrix} i \times (j + k) & = [a_{1}, b_{1}] \times ([a_{2}, b_{2}] + [a_{3}, b_{3}]) \\ = [a_{1}, b_{1}] \times [a_{2} + a_{3}, b_{2} + b_{3}] \\ = [a_{1} (a_{2} + a_{3}) + b_{1} (b_{2} + b_{3}), a_{1} (b_{2} + b_{3}) + b_{1} (a_{2} + a_{3})] \\ = [a_{1} a_{2} + a_{1} a_{3} + b_{1} b_{2} + b_{1} b_{3}, a_{1} b_{2} + a_{1} b_{3} + a_{2} b_{1} + a_{3} b_{1}] \\ = [a_{1} a_{2} + b_{1} b_{2}, a_{1} b_{2} + a_{2} b_{1}] + [a_{1} a_{3} + b_{1} b_{3}, a_{1} b_{3} + a_{3} b_{1}] \\ = ([a_{1}, b_{1}] \times [a_{2}, b_{2}]) + ([a_{1}, b_{1}] \times [a_{3}, b_{3}]) \\ = (i \times j) + (i \times k) \end{matrix}

Conventional reading: seven-line distributivity calculation. Line one: i times open parenthesis j plus k close parenthesis equals the class of a sub one comma b sub one, times the sum of the classes of a sub two comma b sub two and a sub three comma b sub three. Line two: combine that sum coordinatewise. Line three: multiply the resulting classes, obtaining first coordinate a sub one times open parenthesis a sub two plus a sub three close parenthesis plus b sub one times open parenthesis b sub two plus b sub three close parenthesis, and second coordinate a sub one times open parenthesis b sub two plus b sub three close parenthesis plus b sub one times open parenthesis a sub two plus a sub three close parenthesis. Line four: after distribution, the first coordinate is a sub one times a sub two plus a sub one times a sub three plus b sub one times b sub two plus b sub one times b sub three, and the second coordinate is a sub one times b sub two plus a sub one times b sub three plus a sub two times b sub one plus a sub three times b sub one. Line five: split the class into the class with coordinates a sub one times a sub two plus b sub one times b sub two, and a sub one times b sub two plus a sub two times b sub one, plus the analogous class using subscript three. Line six: these are the product of i with j plus the product of i with k. Line seven: the result is i times j plus i times k

Meaning here: This seven-line calculation proves that multiplication of integer-equivalence classes distributes over their addition.

1 occurrence

Occurrence 1: checking-details.tex, line 79, column 1

Expression 115

q_{1} \in β

Conventional reading: q sub one is an element of beta

Meaning here: This states that q sub one is an element of beta.

1 occurrence

Occurrence 1: checking-details.tex, line 165, column 55

Expression 116

0.999 \dots = 1

Conventional reading: zero point nine nine nine and so on equals one

Meaning here: This states that zero point nine nine nine and so on equals one.

1 occurrence

Occurrence 1: cauchy.tex, line 33, column 59

Expression 117

i = [a_{1}, b_{1}]

Conventional reading: i equals the equivalence class of a sub one comma b sub one

Meaning here: This states that i equals the equivalence class of a sub one comma b sub one.

2 occurrences

Expression 118

n_{Z} = {[n, 0]}_{\sim}

Conventional reading: the integer embedding of n equals the integer-equivalence class of n comma zero

Meaning here: This states that the integer embedding of n equals the integer-equivalence class of n comma zero.

1 occurrence

Occurrence 1: integers.tex, line 63, column 21

Expression 119

j = [a_{2}, b_{2}]

Conventional reading: j equals the equivalence class of a sub two comma b sub two

Meaning here: This states that j equals the equivalence class of a sub two comma b sub two.

2 occurrences

Expression 120

[f]

Conventional reading: the real-equivalence class of f

Meaning here: This denotes the real-equivalence class of f in the Cauchy-sequence construction of the reals.

3 occurrences

Expression 121

j = [b, a] \in Z

Conventional reading: j is the integer-equivalence class of b comma a and is an integer

Meaning here: This states that j is the integer-equivalence class of b comma a and is an integer.

1 occurrence

Occurrence 1: checking-details.tex, line 66, column 12

Expression 122

[j] < [h]

Conventional reading: the real-equivalence class of j is less than the real-equivalence class of h

Meaning here: This states that the real-equivalence class of j is less than the real-equivalence class of h.

1 occurrence

Occurrence 1: cauchy.tex, line 226, column 394

Expression 123

m = 2 r

Conventional reading: m equals two times r

Meaning here: This states that m equals two times r.

1 occurrence

Occurrence 1: reals.tex, line 61, column 4

Expression 124

(f - g)

Conventional reading: the pointwise difference f minus g

Meaning here: This denotes the pointwise difference f minus g in the Cauchy-sequence construction of the reals.

2 occurrences

Expression 125

i \in Z

Conventional reading: i is an element of the integers

Meaning here: This states that i is an element of the integers.

2 occurrences

Expression 126

\sqrt{2} = \frac{p}{q}

Conventional reading: the square root of two equals the fraction with numerator p and denominator q

Meaning here: This states that the square root of two equals the fraction with numerator p and denominator q.

1 occurrence

Occurrence 1: reals.tex, line 55, column 1

Expression 127

≎

Conventional reading: is real-equivalent to

Meaning here: This is real equivalence between rational-valued Cauchy sequences: their difference tends to zero.

2 occurrences

Expression 128

i \leq j \leftrightarrow i_{Q} \leq j_{Q}

Conventional reading: i is at most j if and only if the rational embedding of i is at most the rational embedding of j

Meaning here: This states that i is at most j if and only if the rational embedding of i is at most the rational embedding of j.

1 occurrence

Occurrence 1: rationals.tex, line 71, column 27

Expression 129

ε

Conventional reading: epsilon

Meaning here: This is the reusable atomic notation spoken as epsilon. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: cauchy.tex, line 90, column 41

Expression 130

(f \times g) (n) = f (n) \times g (n)

Conventional reading: f times g, evaluated at n, equals f of n times g of n

Meaning here: This states that f times g, evaluated at n, equals f of n times g of n.

1 occurrence

Occurrence 1: cauchy.tex, line 144, column 38

Expression 131

d : N \to N

Conventional reading: d is a function from the natural numbers to the natural numbers

Meaning here: This states that d is a function from the natural numbers to the natural numbers.

1 occurrence

Occurrence 1: cauchy.tex, line 29, column 28

Expression 132

S

Conventional reading: S

Meaning here: This is the reusable atomic notation spoken as S. Its exact mathematical role is supplied separately for every bound source occurrence.

18 occurrences

Expression 133

0 \neq j \in N

Conventional reading: j is a nonzero natural number

Meaning here: This states that j is a nonzero natural number.

1 occurrence

Occurrence 1: rationals.tex, line 60, column 27

Expression 134

⟨ a, b ⟩ ∽ ⟨ c, d ⟩ iff a \times d = b \times c

Conventional reading: the ordered pair a comma b is rational-equivalent to the ordered pair c comma d if and only if a times d equals b times c

Meaning here: This states that the ordered pair a comma b is rational-equivalent to the ordered pair c comma d if and only if a times d equals b times c.

1 occurrence

Occurrence 1: rationals.tex, line 32, column 1

Expression 135

q

Conventional reading: q

Meaning here: This is the reusable atomic notation spoken as q. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: reals.tex, line 54, column 45

Expression 136

p \in Q

Conventional reading: p is an element of the rational numbers

Meaning here: This states that p is an element of the rational numbers.

4 occurrences

Expression 137

r \in N

Conventional reading: r is an element of the natural numbers

Meaning here: This states that r is an element of the natural numbers.

1 occurrence

Occurrence 1: reals.tex, line 61, column 23

Expression 138

c_{q}

Conventional reading: c sub q

Meaning here: This is the reusable atomic notation spoken as c sub q. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: cauchy.tex, line 137, column 49

Expression 139

\emptyset \neq α ⊊ Q

Conventional reading: alpha is a nonempty proper subset of the rational numbers

Meaning here: This states that alpha is a nonempty proper subset of the rational numbers.

1 occurrence

Occurrence 1: cuts.tex, line 31, column 34

Expression 140

q_{R} = [c_{q}]

Conventional reading: q under the real embedding equals the equivalence class of c sub q

Meaning here: This states that q under the real embedding equals the equivalence class of c sub q.

1 occurrence

Occurrence 1: cauchy.tex, line 137, column 9

Expression 141

1, 1.4, 1.414, 1.4142, 1.41421, \dots

Conventional reading: one, one point four, one point four one four, one point four one four two, one point four one four two one, and so on

Meaning here: This denotes one, one point four, one point four one four, one point four one four two, one point four one four two one, and so on in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 44, column 1

Expression 142

∽

Conventional reading: is rational-equivalent to

Meaning here: This is the rational-equivalence relation on integer pairs with nonzero second coordinate.

3 occurrences

Expression 143

0 - 2 = 4 - 6

Conventional reading: zero minus two equals four minus six

Meaning here: This states that zero minus two equals four minus six.

1 occurrence

Occurrence 1: integers.tex, line 20, column 85

Expression 144

[(c_{f (n)} - f)] < [(h - f)]

Conventional reading: the real-equivalence class of c sub f of n minus f is less than the real-equivalence class of h minus f

Meaning here: This states that the real-equivalence class of c sub f of n minus f is less than the real-equivalence class of h minus f.

1 occurrence

Occurrence 1: cauchy.tex, line 220, column 1

Expression 145

m, n \in N

Conventional reading: m and n are natural numbers

Meaning here: This states that m and n are natural numbers.

2 occurrences

Expression 146

p + q < p_{1} + q_{1} \in α + β

Conventional reading: p plus q is less than p sub one plus q sub one, which belongs to alpha plus beta

Meaning here: This states that p plus q is less than p sub one plus q sub one, which belongs to alpha plus beta.

1 occurrence

Occurrence 1: checking-details.tex, line 166, column 39

Expression 147

⟨ a + b, b + a ⟩ \sim_{Z} ⟨ 0, 0 ⟩

Conventional reading: the pair a plus b comma b plus a is integer-equivalent to the pair zero comma zero

Meaning here: This states that the pair a plus b comma b plus a is integer-equivalent to the pair zero comma zero.

1 occurrence

Occurrence 1: checking-details.tex, line 68, column 1

Expression 148

q_{R}

Conventional reading: q under the real embedding

Meaning here: This denotes q under the real embedding in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 185, column 30

Expression 149

f, g : N \to Q

Conventional reading: f and g are functions from the natural numbers to the rational numbers

Meaning here: This states that f and g are functions from the natural numbers to the rational numbers.

1 occurrence

Occurrence 1: cauchy.tex, line 188, column 58

Expression 150

f \sim_{R} g

Conventional reading: f is real-equivalent to g

Meaning here: This states that f is real-equivalent to g.

1 occurrence

Occurrence 1: cauchy.tex, line 130, column 32

Expression 151

m^{2} = 2 n^{2}

Conventional reading: m squared equals two times n squared

Meaning here: This states that m squared equals two times n squared.

2 occurrences

Expression 152

α + β = {p + q : p \in α \land q \in β}

Conventional reading: alpha plus beta equals the set of p plus q such that p is an element of alpha and q is an element of beta

Meaning here: This states that alpha plus beta equals the set of p plus q such that p is an element of alpha and q is an element of beta.

1 occurrence

Occurrence 1: checking-details.tex, line 159, column 43

Expression 153

[(g - f)]

Conventional reading: the real-equivalence class of g minus f

Meaning here: This denotes the real-equivalence class of g minus f in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 152, column 21

Expression 154

+

Conventional reading: plus

Meaning here: This is the addition operation of the ring or field under discussion.

2 occurrences

Expression 155

i \in N

Conventional reading: i is an element of the natural numbers

Meaning here: This states that i is an element of the natural numbers.

1 occurrence

Occurrence 1: rationals.tex, line 60, column 10

Expression 156

a + b = b + a

Conventional reading: a plus b equals b plus a

Meaning here: This states that a plus b equals b plus a.

1 occurrence

Occurrence 1: integers.tex, line 32, column 77

Expression 157

\sqrt{2}

Conventional reading: the square root of two

Meaning here: This denotes the square root of two in the irrationality of the square root of two, the Dedekind-cut construction of the reals, and the Cauchy-sequence construction of the reals.

12 occurrences

Expression 158

q \in λ

Conventional reading: q is an element of lambda

Meaning here: This states that q is an element of lambda.

1 occurrence

Occurrence 1: cuts.tex, line 74, column 31

Expression 159

i + j = [a, b] + [b, a] = [a + b, b + a] = [0, 0] = 0_{Z}

Conventional reading: i plus j equals the equivalence class of a comma b plus the equivalence class of b comma a equals the equivalence class of a plus b comma b plus a equals the equivalence class of zero comma zero equals zero under the integer embedding

Meaning here: This states that i plus j equals the equivalence class of a comma b plus the equivalence class of b comma a equals the equivalence class of a plus b comma b plus a equals the equivalence class of zero comma zero equals zero under the integer embedding.

1 occurrence

Occurrence 1: checking-details.tex, line 69, column 62

Expression 160

p \notin λ

Conventional reading: p is not an element of lambda

Meaning here: This states that p is not an element of lambda.

1 occurrence

Occurrence 1: cuts.tex, line 67, column 42

Expression 161

Q = (Z \times (Z ∖ {0_{Z}})) /_{∽}

Conventional reading: the set of rational numbers is the quotient of integer pairs with nonzero second coordinate by rational equivalence

Meaning here: This defines the rationals as the quotient of integer pairs with nonzero second coordinate by rational equivalence.

1 occurrence

Occurrence 1: rationals.tex, line 43, column 58

Expression 162

[j] < {(g (n))}_{R}

Conventional reading: the real-equivalence class of j is less than the real embedding of g of n

Meaning here: This states that the real-equivalence class of j is less than the real embedding of g of n.

1 occurrence

Occurrence 1: cauchy.tex, line 226, column 273

Expression 163

(\forall α \in S) α \subseteq λ

Conventional reading: for every alpha in S, alpha is a subset of lambda

Meaning here: This states that for every alpha in S, alpha is a subset of lambda.

1 occurrence

Occurrence 1: cuts.tex, line 50, column 133

Expression 164

\frac{i}{j}

Conventional reading: the fraction with numerator i and denominator j

Meaning here: This denotes the fraction with numerator i and denominator j in the construction of the rationals.

2 occurrences

Expression 165

p < q

Conventional reading: p is less than q

Meaning here: This states that p is less than q.

4 occurrences

Expression 166

a + n = m + b

Conventional reading: a plus n equals m plus b

Meaning here: This states that a plus n equals m plus b.

1 occurrence

Occurrence 1: integers.tex, line 36, column 175

Expression 167

h

Conventional reading: h

Meaning here: This is the reusable atomic notation spoken as h. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: cauchy.tex, line 112, column 65

Expression 168

p < q \in λ

Conventional reading: p is less than q, and q belongs to lambda

Meaning here: This states that p is less than q, and q belongs to lambda.

1 occurrence

Occurrence 1: cuts.tex, line 69, column 15

Expression 169

[x, y]

Conventional reading: the equivalence class of x comma y

Meaning here: This denotes the equivalence class of x comma y in the ordered-ring and ordered-field verification.

1 occurrence

Occurrence 1: checking-details.tex, line 47, column 24

Expression 170

i, j \in Z

Conventional reading: i and j are integers

Meaning here: This states that i and j are integers.

1 occurrence

Occurrence 1: rationals.tex, line 72, column 1

Expression 171

p^{2} < 2

Conventional reading: p squared is less than two

Meaning here: This states that p squared is less than two.

1 occurrence

Occurrence 1: checking-details.tex, line 187, column 53

Expression 172

i_{Q} = {[i, 1_{Z}]}_{∽}

Conventional reading: the rational embedding of integer i equals the rational-equivalence class of i comma integer one

Meaning here: This states that the rational embedding of integer i equals the rational-equivalence class of i comma integer one.

1 occurrence

Occurrence 1: rationals.tex, line 65, column 56

Expression 173

{[0, 0]}_{\sim}

Conventional reading: the integer-equivalence class of zero comma zero

Meaning here: This denotes the integer-equivalence class of zero comma zero in the philosophical reflection on arithmetization.

1 occurrence

Occurrence 1: reflections.tex, line 84, column 7

Expression 174

q < n

Conventional reading: q is less than n

Meaning here: This states that q is less than n.

1 occurrence

Occurrence 1: reals.tex, line 55, column 48

Expression 175

[a + b, b + a] = [0, 0] = 0_{Z}

Conventional reading: the equivalence class of a plus b comma b plus a equals the equivalence class of zero comma zero equals zero under the integer embedding

Meaning here: This states that the equivalence class of a plus b comma b plus a equals the equivalence class of zero comma zero equals zero under the integer embedding.

1 occurrence

Occurrence 1: checking-details.tex, line 69, column 1

Expression 176

[f] < [h]

Conventional reading: the real-equivalence class of f is less than the real-equivalence class of h

Meaning here: This states that the real-equivalence class of f is less than the real-equivalence class of h.

1 occurrence

Occurrence 1: cauchy.tex, line 217, column 29

Expression 177

c + n = m + d

Conventional reading: c plus n equals m plus d

Meaning here: This states that c plus n equals m plus d.

1 occurrence

Occurrence 1: integers.tex, line 36, column 115

Expression 178

\leq

Conventional reading: less than or equal to

Meaning here: This is the less-than-or-equal order relation used by the surrounding ordered-ring or ordered-field definition.

3 occurrences

Expression 179

[f] = [g]

Conventional reading: the real-equivalence class of f equals the real-equivalence class of g

Meaning here: This states that the real-equivalence class of f equals the real-equivalence class of g.

2 occurrences

Expression 180

1.41421

Conventional reading: one point four one four two one

Meaning here: This denotes one point four one four two one in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 93, column 1

Expression 181

Q ≺ R

Conventional reading: the cardinality of the rational numbers is strictly less than the cardinality of the real numbers

Meaning here: This states that the cardinality of the rational numbers is strictly less than the cardinality of the real numbers.

1 occurrence

Occurrence 1: reals.tex, line 20, column 39

Expression 182

p^{2} = 2 q^{2}

Conventional reading: p squared equals two times q squared

Meaning here: This states that p squared equals two times q squared.

1 occurrence

Occurrence 1: reals.tex, line 54, column 50

Expression 183

[h] \leq {(f (n))}_{R}

Conventional reading: the real-equivalence class of h is at most the real embedding of f of n

Meaning here: This states that the real-equivalence class of h is at most the real embedding of f of n.

1 occurrence

Occurrence 1: cauchy.tex, line 224, column 47

Expression 184

a \leq b \lor a = b \lor a \geq b

Conventional reading: either a is at most b, a equals b, or a is at least b

Meaning here: This states that either a is at most b, a equals b, or a is at least b.

1 occurrence

Occurrence 1: checking-details.tex, line 108, column 55

Expression 185

p < p_{1}

Conventional reading: p is less than p sub one

Meaning here: This states that p is less than p sub one.

1 occurrence

Occurrence 1: checking-details.tex, line 166, column 11

Expression 186

f ≎ g iff (f - g) tends to 0 .

Conventional reading: f is real-equivalent to g if and only if f minus g tends to zero

Meaning here: This states that f is real-equivalent to g if and only if f minus g tends to zero.

1 occurrence

Occurrence 1: cauchy.tex, line 119, column 1

Expression 187

1.41421356237 \dots

Conventional reading: one point four one four two one three five six two three seven and so on

Meaning here: This denotes one point four one four two one three five six two three seven and so on in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 25, column 1

Expression 188

α - β

Conventional reading: alpha minus beta

Meaning here: This denotes alpha minus beta in the ordered-ring and ordered-field verification.

1 occurrence

Occurrence 1: checking-details.tex, line 170, column 46

Expression 189

q^{2} < 2

Conventional reading: q squared is less than two

Meaning here: This states that q squared is less than two.

2 occurrences

Expression 190

(\exists ℓ \in N) (\forall m, n > ℓ) | f (m) - f (n) | < ε

Conventional reading: there exists a natural-number index ell such that for every m and n greater than ell, the absolute value of f of m minus f of n is less than epsilon

Meaning here: This states that there exists a natural-number index ell such that for every m and n greater than ell, the absolute value of f of m minus f of n is less than epsilon.

1 occurrence

Occurrence 1: cauchy.tex, line 85, column 49

Expression 191

(\forall α \in S) α \subseteq β

Conventional reading: for every alpha in S, alpha is a subset of beta

Meaning here: This states that for every alpha in S, alpha is a subset of beta.

1 occurrence

Occurrence 1: cuts.tex, line 77, column 143

Expression 192

λ = ⋃ S

Conventional reading: lambda equals the union of S

Meaning here: This states that lambda equals the union of S.

1 occurrence

Occurrence 1: cuts.tex, line 59, column 63

Expression 193

\begin{matrix} [f] + [g] & = [(f + g)] \\ [f] \times [g] & = [(f \times g)] \end{matrix}

Conventional reading: the sum of the real-equivalence classes of f and g is the class of f plus g, and their product is the class of f times g

Meaning here: This states that the sum of the real-equivalence classes of f and g is the class of f plus g, and their product is the class of f times g.

1 occurrence

Occurrence 1: cauchy.tex, line 140, column 1

Expression 194

{[m, n]}_{\sim}

Conventional reading: the integer-equivalence class of m comma n

Meaning here: This denotes the integer-equivalence class of m comma n in the construction of the integers.

1 occurrence

Occurrence 1: integers.tex, line 47, column 111

Expression 195

a

Conventional reading: a

Meaning here: This is the reusable atomic notation spoken as a. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: checking-details.tex, line 108, column 35

Expression 196

g

Conventional reading: g

Meaning here: This is the reusable atomic notation spoken as g. Its exact mathematical role is supplied separately for every bound source occurrence.

7 occurrences

Expression 197

x < p + q

Conventional reading: x is less than p plus q

Meaning here: This states that x is less than p plus q.

1 occurrence

Occurrence 1: checking-details.tex, line 161, column 21

Expression 198

i = [a, b]

Conventional reading: i equals the integer-equivalence class of a comma b

Meaning here: This states that i equals the integer-equivalence class of a comma b.

1 occurrence

Occurrence 1: checking-details.tex, line 65, column 27

Expression 199

h \in S

Conventional reading: h is an element of S

Meaning here: This states that h is an element of S.

2 occurrences

Expression 200

α + β

Conventional reading: alpha plus beta

Meaning here: This denotes alpha plus beta in the ordered-ring and ordered-field verification.

3 occurrences

Expression 201

p < m

Conventional reading: p is less than m

Meaning here: This states that p is less than m.

1 occurrence

Occurrence 1: reals.tex, line 55, column 36

Expression 202

a - b = c - d iff a + d = c + b

Conventional reading: a minus b equals c minus d if and only if a plus d equals c plus b

Meaning here: This states that a minus b equals c minus d if and only if a plus d equals c plus b.

1 occurrence

Occurrence 1: integers.tex, line 23, column 2

Expression 203

g (n) = \frac{1}{{(n + 1)}^{2}}

Conventional reading: g of n equals one divided by the square of the quantity n plus one

Meaning here: This states that g of n equals one divided by the square of the quantity n plus one.

1 occurrence

Occurrence 1: cauchy.tex, line 128, column 35

Expression 204

\begin{matrix} a \leq b & \to a + c \leq b + c \\ (a \leq b \land 0 \leq c) & \to a \times c \leq b \times c \end{matrix}

Conventional reading: two ordered-ring compatibility laws: if a is at most b, then a plus c is at most b plus c; and if a is at most b while c is nonnegative, then a times c is at most b times c

Meaning here: These are the two order-compatibility implications required of an ordered ring.

1 occurrence

Occurrence 1: checking-details.tex, line 114, column 1

Expression 205

> \sqrt{2}

Conventional reading: greater than the square root of two

Meaning here: This denotes greater than the square root of two in the Dedekind-cut construction of the reals.

1 occurrence

Occurrence 1: cuts.tex, line 19, column 33

Expression 206

a_{1}, b_{1}, a_{2}, b_{2}, a_{3}, b_{3} \in N

Conventional reading: a sub one, b sub one, a sub two, b sub two, a sub three, and b sub three are natural numbers

Meaning here: This states that a sub one, b sub one, a sub two, b sub two, a sub three, and b sub three are natural numbers.

1 occurrence

Occurrence 1: checking-details.tex, line 44, column 38

Expression 207

1.4142

Conventional reading: one point four one four two

Meaning here: This denotes one point four one four two in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 92, column 47

Expression 208

N^{2}

Conventional reading: the Cartesian square of the natural numbers

Meaning here: This denotes the Cartesian square of the natural numbers in the construction of the integers.

2 occurrences

Expression 209

p \in α

Conventional reading: p is an element of alpha

Meaning here: This states that p is an element of alpha.

6 occurrences

Expression 210

c + b = a + d

Conventional reading: c plus b equals a plus d

Meaning here: This states that c plus b equals a plus d.

1 occurrence

Occurrence 1: integers.tex, line 34, column 91

Expression 211

{[x, y]}_{\sim}

Conventional reading: the integer-equivalence class of x comma y

Meaning here: This denotes the integer-equivalence class of x comma y in the ordered-ring and ordered-field verification.

1 occurrence

Occurrence 1: checking-details.tex, line 48, column 3

Expression 212

i

Conventional reading: i

Meaning here: This is the reusable atomic notation spoken as i. Its exact mathematical role is supplied separately for every bound source occurrence.

1 occurrence

Occurrence 1: rationals.tex, line 18, column 13

Expression 213

⟨ i, j ⟩

Conventional reading: the ordered pair i comma j

Meaning here: This denotes the ordered pair i comma j in the construction of the rationals.

1 occurrence

Occurrence 1: rationals.tex, line 49, column 18

Expression 214

\begin{matrix} f (0) & = p \\ g (0) & = q \end{matrix}

Conventional reading: f of zero equals p; g of zero equals q

Meaning here: This states that f of zero equals p; g of zero equals q.

1 occurrence

Occurrence 1: cauchy.tex, line 191, column 1

Expression 215

\begin{matrix} Multiplicative Inverse & (\forall a \in S ∖ {0}) (\exists b \in S) a \times b & = 1 \end{matrix}

Conventional reading: for every nonzero a in S there exists b in S such that a times b equals one

Meaning here: This is the multiplicative-inverse requirement for every nonzero element of an ordered field.

1 occurrence

Occurrence 1: checking-details.tex, line 133, column 1

Expression 216

0_{R} < [(h - f)]

Conventional reading: real zero is less than the real-equivalence class of h minus f

Meaning here: This states that real zero is less than the real-equivalence class of h minus f.

1 occurrence

Occurrence 1: cauchy.tex, line 218, column 1

Expression 217

\frac{a}{b} = \frac{c}{d} iff a \times d = b \times c

Conventional reading: a over b equals c over d if and only if a times d equals b times c

Meaning here: This states that a over b equals c over d if and only if a times d equals b times c.

1 occurrence

Occurrence 1: rationals.tex, line 27, column 1

Expression 218

q_{R} < r

Conventional reading: the real embedding of q is less than the real represented by r

Meaning here: This states that the real embedding of q is less than the real represented by r.

1 occurrence

Occurrence 1: cauchy.tex, line 184, column 29

Expression 219

0 \neq {[0, 0]}_{\sim}

Conventional reading: zero is not equal to the equivalence class of zero comma zero modulo integer equivalence

Meaning here: This states that zero is not equal to the equivalence class of zero comma zero modulo integer equivalence.

1 occurrence

Occurrence 1: reflections.tex, line 84, column 41

Expression 220

{(i \times j)}_{Q} = i_{Q} \times j_{Q}

Conventional reading: the rational embedding of i times j equals the product of the rational embeddings of i and j

Meaning here: This states that the rational embedding of i times j equals the product of the rational embeddings of i and j.

1 occurrence

Occurrence 1: rationals.tex, line 70, column 47

Expression 221

a + d + c + n = c + b + m + d

Conventional reading: a plus d plus c plus n equals c plus b plus m plus d

Meaning here: This states that a plus d plus c plus n equals c plus b plus m plus d.

1 occurrence

Occurrence 1: integers.tex, line 36, column 135

Expression 222

\begin{matrix} α + β & = {p + q : p \in α \land q \in β} \\ α \times β & = {p \times q : 0 \leq p \in α \land 0 \leq q \in β} \cup 0^{R} & if α, β \geq 0_{R} \end{matrix}

Conventional reading: two operations on nonnegative cuts. Alpha plus beta is the set of p plus q for p in alpha and q in beta. Alpha times beta is the union of the real-zero cut with all products p times q for nonnegative p in alpha and nonnegative q in beta

Meaning here: These clauses define addition and multiplication for nonnegative Dedekind cuts. Real zero is itself a cut, so union with it supplies all negative rationals; no singleton brace is missing.

1 occurrence

Occurrence 1: cuts.tex, line 88, column 1

Expression 223

\sqrt{2} = {p \in Q : p < 0 or p^{2} < 2}

Conventional reading: the square root of two equals the cut of all rational p such that p is negative or p squared is less than two

Meaning here: This states that the square root of two equals the cut of all rational p such that p is negative or p squared is less than two.

1 occurrence

Occurrence 1: checking-details.tex, line 180, column 48

Expression 224

n, m \in N

Conventional reading: n and m are natural numbers

Meaning here: This states that n and m are natural numbers.

1 occurrence

Occurrence 1: integers.tex, line 15, column 64

Expression 225

⟨ 0, 2 ⟩ \neq ⟨ 4, 6 ⟩

Conventional reading: the ordered pair zero comma two is not equal to the ordered pair four comma six

Meaning here: This states that the ordered pair zero comma two is not equal to the ordered pair four comma six.

1 occurrence

Occurrence 1: integers.tex, line 20, column 115

Expression 226

(\exists ℓ \in N) (\forall n > ℓ) | h (n) | < ε

Conventional reading: there exists a natural-number index ell such that for every n greater than ell, the absolute value of h of n is less than epsilon

Meaning here: This states that there exists a natural-number index ell such that for every n greater than ell, the absolute value of h of n is less than epsilon.

1 occurrence

Occurrence 1: cauchy.tex, line 114, column 1

Expression 227

[j]

Conventional reading: the real-equivalence class of j

Meaning here: This denotes the real-equivalence class of j in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 226, column 442

Expression 228

λ \subseteq Q

Conventional reading: lambda is a subset of the rational numbers

Meaning here: This states that lambda is a subset of the rational numbers.

1 occurrence

Occurrence 1: cuts.tex, line 65, column 55

Expression 229

d (n)

Conventional reading: d of n

Meaning here: This denotes d of n in the Cauchy-sequence construction of the reals.

1 occurrence

Occurrence 1: cauchy.tex, line 29, column 60

Expression 230

N \subseteq Q

Conventional reading: the set of natural numbers is a subset of the rational numbers

Meaning here: This states that the set of natural numbers is a subset of the rational numbers.

1 occurrence

Occurrence 1: reflections.tex, line 88, column 28

Expression 231

\lim_{x \to \infty} f (x) = 0

Conventional reading: the limit of f of x as x approaches infinity equals zero

Meaning here: This states that the limit of f of x as x approaches infinity equals zero.

1 occurrence

Occurrence 1: cauchy.tex, line 115, column 57

Expression 232

\begin{matrix} Associativity & a + (b + c) & = (a + b) + c \\ (a \times b) \times c & = a \times (b \times c) \\ Commutativity & a + b & = b + a \\ a \times b & = b \times a \\ Identities & a + 0 & = a \\ a \times 1 & = a \\ Additive Inverse & (\exists b \in S) 0 & = a + b \\ Distributivity & a \times (b + c) & = (a \times b) + (a \times c) \end{matrix}

Conventional reading: the eight commutative-ring laws: associativity of addition and multiplication; commutativity of addition and multiplication; additive identity zero; multiplicative identity one; existence of an additive inverse for each a; and distributivity of multiplication over addition

Meaning here: These are the eight algebraic laws used to define a commutative ring.

1 occurrence

Occurrence 1: checking-details.tex, line 25, column 2

Expression 233

⟨ c, d ⟩ \sim ⟨ a, b ⟩

Conventional reading: the ordered pair c comma d is integer-equivalent to the ordered pair a comma b

Meaning here: This states that the ordered pair c comma d is integer-equivalent to the ordered pair a comma b.

1 occurrence

Occurrence 1: integers.tex, line 34, column 116

Expression 234

α \div β

Conventional reading: alpha divided by beta

Meaning here: This denotes alpha divided by beta in the ordered-ring and ordered-field verification.

1 occurrence

Occurrence 1: checking-details.tex, line 171, column 27

Expression 235

β

Conventional reading: beta

Meaning here: This is the reusable atomic notation spoken as beta. Its exact mathematical role is supplied separately for every bound source occurrence.

4 occurrences

Expression 236

(\exists ℓ \in N) (\forall n > ℓ) 0 < f (n)

Conventional reading: there exists a natural-number index ell such that f of n is positive for every n greater than ell

Meaning here: This states that there exists a natural-number index ell such that f of n is positive for every n greater than ell.

1 occurrence

Occurrence 1: cauchy.tex, line 150, column 58

Expression 237

(a + b) + 0 = 0 + (a + b)

Conventional reading: the quantity a plus b, plus zero, equals zero plus the quantity a plus b

Meaning here: This states that the quantity a plus b, plus zero, equals zero plus the quantity a plus b.

1 occurrence

Occurrence 1: checking-details.tex, line 67, column 28

Expression 238

[f] < [g]

Conventional reading: the real-equivalence class of f is less than the real-equivalence class of g

Meaning here: This states that the real-equivalence class of f is less than the real-equivalence class of g.

1 occurrence

Occurrence 1: cauchy.tex, line 151, column 53

Expression 239

\frac{3}{2} = \frac{6}{4}

Conventional reading: the fraction with numerator three and denominator two equals the fraction with numerator six and denominator four

Meaning here: This states that the fraction with numerator three and denominator two equals the fraction with numerator six and denominator four.

1 occurrence

Occurrence 1: rationals.tex, line 25, column 1

Expression 240

p < q \in α

Conventional reading: p is less than q, and q belongs to alpha

Meaning here: This states that p is less than q, and q belongs to alpha.

1 occurrence

Occurrence 1: cuts.tex, line 32, column 51

Expression 241

a b

Conventional reading: a times b

Meaning here: This denotes a times b in the construction of the integers.

1 occurrence

Occurrence 1: integers.tex, line 55, column 27

Expression 242

(\forall h \in S) [h] \leq [f]

Conventional reading: for every h in S, the real-equivalence class of h is at most the real-equivalence class of f

Meaning here: This states that for every h in S, the real-equivalence class of h is at most the real-equivalence class of f.

1 occurrence

Occurrence 1: cauchy.tex, line 215, column 74

Expression 243

p \in β

Conventional reading: p is an element of beta

Meaning here: This states that p is an element of beta.

1 occurrence

Occurrence 1: cuts.tex, line 77, column 296

One diagram

Overlapping-squares proof diagram

Two equal squares of side n overlap inside a larger square of side m. The central orange overlap and two uncovered corner squares encode a smaller solution to the same square-area equation.

Words-only linearization: Diagram for the geometric irrationality proof. A large outer square has side m. Two equal inner squares, each of side n, occupy the lower-left and upper-right corners and overlap in a central orange square. Two congruent corner regions remain uncovered. Because m squared equals twice n squared, the central overlap has the same total area as the two uncovered regions. Calling the overlap side p and each uncovered-square side q yields p squared equals twice q squared, with p less than m and q less than n.

Open in reading context.

40 formal objects

Integer equivalence is an equivalence relation — integers.tex, line 27.
Definition of the integers as equivalence classes — integers.tex, line 41.
Definitions of integer-class addition, multiplication, and order — integers.tex, line 50.
Natural-number embedding laws for integers — integers.tex, line 66.
Integer-embedding multiplication calculation — integers.tex, line 76.
Exercise on the natural-number embedding into the integers — integers.tex, line 85; unsolved source prompt.
Exercise proving rational equivalence — rationals.tex, line 37; unsolved source prompt.
Definition of the rationals as equivalence classes — rationals.tex, line 41.
Definitions of rational-class addition, multiplication, and order — rationals.tex, line 50.
Exercise on the integer embedding into the rationals — rationals.tex, line 69; unsolved source prompt.
The square root of two is irrational — reals.tex, line 25.
Overlapping-squares proof diagram — reals.tex, line 39.
Definition of a Dedekind cut — cuts.tex, line 26.
Order on Dedekind cuts — cuts.tex, line 44.
Completeness of the set of cuts — cuts.tex, line 54.
Addition and nonnegative multiplication of cuts — cuts.tex, line 88.
Additive inverse of a cut — cuts.tex, line 97.
Remaining sign cases for multiplying cuts — cuts.tex, line 101.
Eight commutative-ring laws — checking-details.tex, line 25.
Definition of a commutative ring — checking-details.tex, line 23.
Associativity calculation for integer addition — checking-details.tex, line 50.
Distributivity calculation for integer multiplication — checking-details.tex, line 79.
Exercise proving the integers form a commutative ring — checking-details.tex, line 97; unsolved source prompt.
Order compatibility laws for an ordered ring — checking-details.tex, line 114.
Definition of an ordered ring — checking-details.tex, line 111.
Exercise proving the integers form an ordered ring — checking-details.tex, line 120; unsolved source prompt.
Multiplicative-inverse law for an ordered field — checking-details.tex, line 133.
Definition of an ordered field — checking-details.tex, line 131.
Exercise proving the rationals form an ordered field — checking-details.tex, line 141; unsolved source prompt.
Exercise proving the Dedekind-cut reals form an ordered field — checking-details.tex, line 175; unsolved source prompt.
Calculation proving p is less than q — checking-details.tex, line 190.
Calculation proving q squared is less than two — checking-details.tex, line 197.
Definition of a Cauchy sequence — cauchy.tex, line 83.
Exercise comparing two Cauchy sequences — cauchy.tex, line 127; unsolved source prompt.
Addition and multiplication of real-equivalence classes — cauchy.tex, line 140.
Cauchy-sequence reals form an ordered field — cauchy.tex, line 161.
Exercise proving the Cauchy-sequence ordered-field theorem — cauchy.tex, line 169; unsolved source prompt.
Completeness of the Cauchy-sequence reals — cauchy.tex, line 176.
Initial values for the bounding sequences — cauchy.tex, line 191.
Recursive upper and lower approximation sequences — cauchy.tex, line 198.

29 resolved source references

9 disclosed reader corrections

TR006-SOURCE-FORMULA-007: The source compares a real-equivalence class with rational zero. The reader says real zero, which is the identity in the constructed ordered field, while preserving the printed formula and source MathML.
TR006-SOURCE-PROSE-001: The reader supplies the missing word 'to' in the source explanation of multiplication by juxtaposition.
TR006-SOURCE-PROSE-002: Nonemptiness, not the existence of an upper bound, supplies a member of S; the immutable source wording is retained separately.
TR006-SOURCE-PROSE-003: The reader supplies the missing noun 'details.'
TR006-SOURCE-PROSE-004: The reader supplies the missing word 'is.'
TR006-SOURCE-PROSE-005: The construction identifies reals with equivalence classes, not with the equivalence relation itself.
TR006-SOURCE-PROSE-006: The reader removes the duplicated word 'we.'
TR006-SOURCE-PROSE-008: The reader corrects the blended phrase 'hone on in' to 'home in on.'
TR006-SOURCE-PROSE-009: The printed equality is a proposition, not an object that can be an upper bound. The reader identifies the common class intended by the surrounding proof while retaining the source formula and its MathML.

Words-only presentation normalization

SFR-ARITH-PRESENTATION-001: The projected source has a redundant less-than character immediately before the words 'are all smaller than.' The prose reader omits that duplicate symbol; the exact accepted projected TeX remains available in Source and provenance.