Type  Label  Description 
Statement 

Definition  dfmpq 7101* 
Define premultiplication on positive fractions. This is a
"temporary"
set used in the construction of complex numbers, and is intended to be
used only by the construction. From Proposition 92.4 of [Gleason]
p. 119. (Contributed by NM, 28Aug1995.)

⊢ ·_{pQ} =
(𝑥 ∈ (N
× N), 𝑦 ∈ (N ×
N) ↦ ⟨((1^{st} ‘𝑥) ·_{N}
(1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) 

Definition  dfltpq 7102* 
Define preordering relation on positive fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. Similar to Definition 5
of [Suppes] p. 162. (Contributed by NM,
28Aug1995.)

⊢ <_{pQ} =
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N
× N) ∧ 𝑦 ∈ (N ×
N)) ∧ ((1^{st} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦))
<_{N} ((1^{st} ‘𝑦) ·_{N}
(2^{nd} ‘𝑥)))} 

Definition  dfenq 7103* 
Define equivalence relation for positive fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. From Proposition 92.1 of
[Gleason] p. 117. (Contributed by NM,
27Aug1995.)

⊢ ~_{Q} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·_{N} 𝑢) = (𝑤 ·_{N} 𝑣)))} 

Definition  dfnqqs 7104 
Define class of positive fractions. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. From Proposition 92.2 of [Gleason] p. 117.
(Contributed by NM, 16Aug1995.)

⊢ Q = ((N ×
N) / ~_{Q} ) 

Definition  dfplqqs 7105* 
Define addition on positive fractions. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only
by the construction. From Proposition 92.3 of [Gleason] p. 117.
(Contributed by NM, 24Aug1995.)

⊢ +_{Q} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~_{Q} ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~_{Q} ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +_{pQ}
⟨𝑢, 𝑓⟩)]
~_{Q} ))} 

Definition  dfmqqs 7106* 
Define multiplication on positive fractions. This is a "temporary"
set
used in the construction of complex numbers, and is intended to be used
only by the construction. From Proposition 92.4 of [Gleason] p. 119.
(Contributed by NM, 24Aug1995.)

⊢ ·_{Q} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~_{Q} ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~_{Q} ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ ·_{pQ}
⟨𝑢, 𝑓⟩)]
~_{Q} ))} 

Definition  df1nqqs 7107 
Define positive fraction constant 1. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. From Proposition 92.2 of [Gleason] p. 117.
(Contributed by NM, 29Oct1995.)

⊢ 1_{Q} =
[⟨1_{o}, 1_{o}⟩]
~_{Q} 

Definition  dfrq 7108* 
Define reciprocal on positive fractions. It means the same thing as one
divided by the argument (although we don't define full division since we
will never need it). This is a "temporary" set used in the
construction
of complex numbers, and is intended to be used only by the construction.
From Proposition 92.5 of [Gleason] p.
119, who uses an asterisk to
denote this unary operation. (Contributed by Jim Kingdon,
20Sep2019.)

⊢ *_{Q} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧
(𝑥
·_{Q} 𝑦) =
1_{Q})} 

Definition  dfltnqqs 7109* 
Define ordering relation on positive fractions. This is a
"temporary"
set used in the construction of complex numbers, and is intended to be
used only by the construction. Similar to Definition 5 of [Suppes]
p. 162. (Contributed by NM, 13Feb1996.)

⊢ <_{Q} =
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~_{Q} ∧
𝑦 = [⟨𝑣, 𝑢⟩] ~_{Q} ) ∧
(𝑧
·_{N} 𝑢) <_{N} (𝑤
·_{N} 𝑣)))} 

Theorem  dfplpq2 7110* 
Alternate definition of preaddition on positive fractions.
(Contributed by Jim Kingdon, 12Sep2019.)

⊢ +_{pQ} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·_{N} 𝑓) +_{N}
(𝑣
·_{N} 𝑢)), (𝑣 ·_{N} 𝑓)⟩))} 

Theorem  dfmpq2 7111* 
Alternate definition of premultiplication on positive fractions.
(Contributed by Jim Kingdon, 13Sep2019.)

⊢ ·_{pQ} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·_{N} 𝑢), (𝑣 ·_{N} 𝑓)⟩))} 

Theorem  enqbreq 7112 
Equivalence relation for positive fractions in terms of positive
integers. (Contributed by NM, 27Aug1995.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → (⟨𝐴, 𝐵⟩ ~_{Q}
⟨𝐶, 𝐷⟩ ↔ (𝐴 ·_{N} 𝐷) = (𝐵 ·_{N} 𝐶))) 

Theorem  enqbreq2 7113 
Equivalence relation for positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8May2013.)

⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ~_{Q} 𝐵 ↔ ((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) = ((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)))) 

Theorem  enqer 7114 
The equivalence relation for positive fractions is an equivalence
relation. Proposition 92.1 of [Gleason] p. 117. (Contributed by NM,
27Aug1995.) (Revised by Mario Carneiro, 6Jul2015.)

⊢ ~_{Q} Er
(N × N) 

Theorem  enqeceq 7115 
Equivalence class equality of positive fractions in terms of positive
integers. (Contributed by NM, 29Nov1995.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([⟨𝐴, 𝐵⟩] ~_{Q} =
[⟨𝐶, 𝐷⟩]
~_{Q} ↔ (𝐴 ·_{N} 𝐷) = (𝐵 ·_{N} 𝐶))) 

Theorem  enqex 7116 
The equivalence relation for positive fractions exists. (Contributed by
NM, 3Sep1995.)

⊢ ~_{Q} ∈
V 

Theorem  enqdc 7117 
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7Sep2019.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → DECID ⟨𝐴, 𝐵⟩ ~_{Q}
⟨𝐶, 𝐷⟩) 

Theorem  enqdc1 7118 
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7Sep2019.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
𝐶 ∈ (N
× N)) → DECID ⟨𝐴, 𝐵⟩ ~_{Q} 𝐶) 

Theorem  nqex 7119 
The class of positive fractions exists. (Contributed by NM,
16Aug1995.) (Revised by Mario Carneiro, 27Apr2013.)

⊢ Q ∈ V 

Theorem  0nnq 7120 
The empty set is not a positive fraction. (Contributed by NM,
24Aug1995.) (Revised by Mario Carneiro, 27Apr2013.)

⊢ ¬ ∅ ∈
Q 

Theorem  ltrelnq 7121 
Positive fraction 'less than' is a relation on positive fractions.
(Contributed by NM, 14Feb1996.) (Revised by Mario Carneiro,
27Apr2013.)

⊢ <_{Q} ⊆
(Q × Q) 

Theorem  1nq 7122 
The positive fraction 'one'. (Contributed by NM, 29Oct1995.)

⊢ 1_{Q} ∈
Q 

Theorem  addcmpblnq 7123 
Lemma showing compatibility of addition. (Contributed by NM,
27Aug1995.)

⊢ ((((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·_{N} 𝐷) = (𝐵 ·_{N} 𝐶) ∧ (𝐹 ·_{N} 𝑆) = (𝐺 ·_{N} 𝑅)) → ⟨((𝐴
·_{N} 𝐺) +_{N} (𝐵
·_{N} 𝐹)), (𝐵 ·_{N} 𝐺)⟩
~_{Q} ⟨((𝐶 ·_{N} 𝑆) +_{N}
(𝐷
·_{N} 𝑅)), (𝐷 ·_{N} 𝑆)⟩)) 

Theorem  mulcmpblnq 7124 
Lemma showing compatibility of multiplication. (Contributed by NM,
27Aug1995.)

⊢ ((((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·_{N} 𝐷) = (𝐵 ·_{N} 𝐶) ∧ (𝐹 ·_{N} 𝑆) = (𝐺 ·_{N} 𝑅)) → ⟨(𝐴
·_{N} 𝐹), (𝐵 ·_{N} 𝐺)⟩
~_{Q} ⟨(𝐶 ·_{N} 𝑅), (𝐷 ·_{N} 𝑆)⟩)) 

Theorem  addpipqqslem 7125 
Lemma for addpipqqs 7126. (Contributed by Jim Kingdon, 11Sep2019.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ⟨((𝐴 ·_{N} 𝐷) +_{N}
(𝐵
·_{N} 𝐶)), (𝐵 ·_{N} 𝐷)⟩ ∈ (N
× N)) 

Theorem  addpipqqs 7126 
Addition of positive fractions in terms of positive integers.
(Contributed by NM, 28Aug1995.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([⟨𝐴, 𝐵⟩] ~_{Q}
+_{Q} [⟨𝐶, 𝐷⟩] ~_{Q} ) =
[⟨((𝐴
·_{N} 𝐷) +_{N} (𝐵
·_{N} 𝐶)), (𝐵 ·_{N} 𝐷)⟩]
~_{Q} ) 

Theorem  mulpipq2 7127 
Multiplication of positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8May2013.)

⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·_{pQ} 𝐵) = ⟨((1^{st}
‘𝐴)
·_{N} (1^{st} ‘𝐵)), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) 

Theorem  mulpipq 7128 
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28Aug1995.) (Revised by Mario Carneiro,
8May2013.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → (⟨𝐴, 𝐵⟩ ·_{pQ}
⟨𝐶, 𝐷⟩) = ⟨(𝐴 ·_{N} 𝐶), (𝐵 ·_{N} 𝐷)⟩) 

Theorem  mulpipqqs 7129 
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28Aug1995.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([⟨𝐴, 𝐵⟩] ~_{Q}
·_{Q} [⟨𝐶, 𝐷⟩] ~_{Q} ) =
[⟨(𝐴
·_{N} 𝐶), (𝐵 ·_{N} 𝐷)⟩]
~_{Q} ) 

Theorem  ordpipqqs 7130 
Ordering of positive fractions in terms of positive integers.
(Contributed by Jim Kingdon, 14Sep2019.)

⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([⟨𝐴, 𝐵⟩] ~_{Q}
<_{Q} [⟨𝐶, 𝐷⟩] ~_{Q} ↔
(𝐴
·_{N} 𝐷) <_{N} (𝐵
·_{N} 𝐶))) 

Theorem  addclnq 7131 
Closure of addition on positive fractions. (Contributed by NM,
29Aug1995.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
+_{Q} 𝐵) ∈ Q) 

Theorem  mulclnq 7132 
Closure of multiplication on positive fractions. (Contributed by NM,
29Aug1995.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
·_{Q} 𝐵) ∈ Q) 

Theorem  dmaddpqlem 7133* 
Decomposition of a positive fraction into numerator and denominator.
Lemma for dmaddpq 7135. (Contributed by Jim Kingdon, 15Sep2019.)

⊢ (𝑥 ∈ Q → ∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~_{Q}
) 

Theorem  nqpi 7134* 
Decomposition of a positive fraction into numerator and denominator.
Similar to dmaddpqlem 7133 but also shows that the numerator and
denominator are positive integers. (Contributed by Jim Kingdon,
20Sep2019.)

⊢ (𝐴 ∈ Q → ∃𝑤∃𝑣((𝑤 ∈ N ∧ 𝑣 ∈ N) ∧
𝐴 = [⟨𝑤, 𝑣⟩] ~_{Q}
)) 

Theorem  dmaddpq 7135 
Domain of addition on positive fractions. (Contributed by NM,
24Aug1995.)

⊢ dom +_{Q} =
(Q × Q) 

Theorem  dmmulpq 7136 
Domain of multiplication on positive fractions. (Contributed by NM,
24Aug1995.)

⊢ dom ·_{Q} =
(Q × Q) 

Theorem  addcomnqg 7137 
Addition of positive fractions is commutative. (Contributed by Jim
Kingdon, 15Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
+_{Q} 𝐵) = (𝐵 +_{Q} 𝐴)) 

Theorem  addassnqg 7138 
Addition of positive fractions is associative. (Contributed by Jim
Kingdon, 16Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ ((𝐴
+_{Q} 𝐵) +_{Q} 𝐶) = (𝐴 +_{Q} (𝐵 +_{Q}
𝐶))) 

Theorem  mulcomnqg 7139 
Multiplication of positive fractions is commutative. (Contributed by
Jim Kingdon, 17Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
·_{Q} 𝐵) = (𝐵 ·_{Q} 𝐴)) 

Theorem  mulassnqg 7140 
Multiplication of positive fractions is associative. (Contributed by
Jim Kingdon, 17Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ ((𝐴
·_{Q} 𝐵) ·_{Q} 𝐶) = (𝐴 ·_{Q} (𝐵
·_{Q} 𝐶))) 

Theorem  mulcanenq 7141 
Lemma for distributive law: cancellation of common factor. (Contributed
by NM, 2Sep1995.) (Revised by Mario Carneiro, 8May2013.)

⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ⟨(𝐴
·_{N} 𝐵), (𝐴 ·_{N} 𝐶)⟩
~_{Q} ⟨𝐵, 𝐶⟩) 

Theorem  mulcanenqec 7142 
Lemma for distributive law: cancellation of common factor. (Contributed
by Jim Kingdon, 17Sep2019.)

⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ [⟨(𝐴
·_{N} 𝐵), (𝐴 ·_{N} 𝐶)⟩]
~_{Q} = [⟨𝐵, 𝐶⟩] ~_{Q}
) 

Theorem  distrnqg 7143 
Multiplication of positive fractions is distributive. (Contributed by
Jim Kingdon, 17Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
·_{Q} (𝐵 +_{Q} 𝐶)) = ((𝐴 ·_{Q} 𝐵) +_{Q}
(𝐴
·_{Q} 𝐶))) 

Theorem  1qec 7144 
The equivalence class of ratio 1. (Contributed by NM, 4Mar1996.)

⊢ (𝐴 ∈ N →
1_{Q} = [⟨𝐴, 𝐴⟩] ~_{Q}
) 

Theorem  mulidnq 7145 
Multiplication identity element for positive fractions. (Contributed by
NM, 3Mar1996.)

⊢ (𝐴 ∈ Q → (𝐴
·_{Q} 1_{Q}) = 𝐴) 

Theorem  recexnq 7146* 
Existence of positive fraction reciprocal. (Contributed by Jim Kingdon,
20Sep2019.)

⊢ (𝐴 ∈ Q → ∃𝑦(𝑦 ∈ Q ∧ (𝐴
·_{Q} 𝑦) =
1_{Q})) 

Theorem  recmulnqg 7147 
Relationship between reciprocal and multiplication on positive
fractions. (Contributed by Jim Kingdon, 19Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
((*_{Q}‘𝐴) = 𝐵 ↔ (𝐴 ·_{Q} 𝐵) =
1_{Q})) 

Theorem  recclnq 7148 
Closure law for positive fraction reciprocal. (Contributed by NM,
6Mar1996.) (Revised by Mario Carneiro, 8May2013.)

⊢ (𝐴 ∈ Q →
(*_{Q}‘𝐴) ∈ Q) 

Theorem  recidnq 7149 
A positive fraction times its reciprocal is 1. (Contributed by NM,
6Mar1996.) (Revised by Mario Carneiro, 8May2013.)

⊢ (𝐴 ∈ Q → (𝐴
·_{Q} (*_{Q}‘𝐴)) =
1_{Q}) 

Theorem  recrecnq 7150 
Reciprocal of reciprocal of positive fraction. (Contributed by NM,
26Apr1996.) (Revised by Mario Carneiro, 29Apr2013.)

⊢ (𝐴 ∈ Q →
(*_{Q}‘(*_{Q}‘𝐴)) = 𝐴) 

Theorem  rec1nq 7151 
Reciprocal of positive fraction one. (Contributed by Jim Kingdon,
29Dec2019.)

⊢
(*_{Q}‘1_{Q}) =
1_{Q} 

Theorem  nqtri3or 7152 
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<_{Q} 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <_{Q} 𝐴)) 

Theorem  ltdcnq 7153 
Lessthan for positive fractions is decidable. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
DECID 𝐴
<_{Q} 𝐵) 

Theorem  ltsonq 7154 
'Less than' is a strict ordering on positive fractions. (Contributed by
NM, 19Feb1996.) (Revised by Mario Carneiro, 4May2013.)

⊢ <_{Q} Or
Q 

Theorem  nqtric 7155 
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<_{Q} 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <_{Q} 𝐴))) 

Theorem  ltanqg 7156 
Ordering property of addition for positive fractions. Proposition
92.6(ii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
<_{Q} 𝐵 ↔ (𝐶 +_{Q} 𝐴)
<_{Q} (𝐶 +_{Q} 𝐵))) 

Theorem  ltmnqg 7157 
Ordering property of multiplication for positive fractions. Proposition
92.6(iii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
<_{Q} 𝐵 ↔ (𝐶 ·_{Q} 𝐴)
<_{Q} (𝐶 ·_{Q} 𝐵))) 

Theorem  ltanqi 7158 
Ordering property of addition for positive fractions. One direction of
ltanqg 7156. (Contributed by Jim Kingdon, 9Dec2019.)

⊢ ((𝐴 <_{Q} 𝐵 ∧ 𝐶 ∈ Q) → (𝐶 +_{Q}
𝐴)
<_{Q} (𝐶 +_{Q} 𝐵)) 

Theorem  ltmnqi 7159 
Ordering property of multiplication for positive fractions. One direction
of ltmnqg 7157. (Contributed by Jim Kingdon, 9Dec2019.)

⊢ ((𝐴 <_{Q} 𝐵 ∧ 𝐶 ∈ Q) → (𝐶
·_{Q} 𝐴) <_{Q} (𝐶
·_{Q} 𝐵)) 

Theorem  lt2addnq 7160 
Ordering property of addition for positive fractions. (Contributed by Jim
Kingdon, 7Dec2019.)

⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧
(𝐶 ∈ Q
∧ 𝐷 ∈
Q)) → ((𝐴 <_{Q} 𝐵 ∧ 𝐶 <_{Q} 𝐷) → (𝐴 +_{Q} 𝐶)
<_{Q} (𝐵 +_{Q} 𝐷))) 

Theorem  lt2mulnq 7161 
Ordering property of multiplication for positive fractions. (Contributed
by Jim Kingdon, 18Jul2021.)

⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧
(𝐶 ∈ Q
∧ 𝐷 ∈
Q)) → ((𝐴 <_{Q} 𝐵 ∧ 𝐶 <_{Q} 𝐷) → (𝐴 ·_{Q} 𝐶)
<_{Q} (𝐵 ·_{Q} 𝐷))) 

Theorem  1lt2nq 7162 
One is less than two (one plus one). (Contributed by NM, 13Mar1996.)
(Revised by Mario Carneiro, 10May2013.)

⊢ 1_{Q}
<_{Q} (1_{Q}
+_{Q} 1_{Q}) 

Theorem  ltaddnq 7163 
The sum of two fractions is greater than one of them. (Contributed by
NM, 14Mar1996.) (Revised by Mario Carneiro, 10May2013.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
𝐴
<_{Q} (𝐴 +_{Q} 𝐵)) 

Theorem  ltexnqq 7164* 
Ordering on positive fractions in terms of existence of sum. Definition
in Proposition 92.6 of [Gleason] p.
119. (Contributed by Jim Kingdon,
23Sep2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<_{Q} 𝐵 ↔ ∃𝑥 ∈ Q (𝐴 +_{Q} 𝑥) = 𝐵)) 

Theorem  ltexnqi 7165* 
Ordering on positive fractions in terms of existence of sum.
(Contributed by Jim Kingdon, 30Apr2020.)

⊢ (𝐴 <_{Q} 𝐵 → ∃𝑥 ∈ Q (𝐴 +_{Q}
𝑥) = 𝐵) 

Theorem  halfnqq 7166* 
Onehalf of any positive fraction is a fraction. (Contributed by Jim
Kingdon, 23Sep2019.)

⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q (𝑥 +_{Q}
𝑥) = 𝐴) 

Theorem  halfnq 7167* 
Onehalf of any positive fraction exists. Lemma for Proposition
92.6(i) of [Gleason] p. 120.
(Contributed by NM, 16Mar1996.)
(Revised by Mario Carneiro, 10May2013.)

⊢ (𝐴 ∈ Q → ∃𝑥(𝑥 +_{Q} 𝑥) = 𝐴) 

Theorem  nsmallnqq 7168* 
There is no smallest positive fraction. (Contributed by Jim Kingdon,
24Sep2019.)

⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q 𝑥 <_{Q}
𝐴) 

Theorem  nsmallnq 7169* 
There is no smallest positive fraction. (Contributed by NM,
26Apr1996.) (Revised by Mario Carneiro, 10May2013.)

⊢ (𝐴 ∈ Q → ∃𝑥 𝑥 <_{Q} 𝐴) 

Theorem  subhalfnqq 7170* 
There is a number which is less than half of any positive fraction. The
case where 𝐴 is one is Lemma 11.4 of [BauerTaylor], p. 50, and they
use the word "approximate half" for such a number (since there
may be
constructions, for some structures other than the rationals themselves,
which rely on such an approximate half but do not require division by
two as seen at halfnqq 7166). (Contributed by Jim Kingdon,
25Nov2019.)

⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q (𝑥 +_{Q}
𝑥)
<_{Q} 𝐴) 

Theorem  ltbtwnnqq 7171* 
There exists a number between any two positive fractions. Proposition
92.6(i) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
24Sep2019.)

⊢ (𝐴 <_{Q} 𝐵 ↔ ∃𝑥 ∈ Q (𝐴 <_{Q}
𝑥 ∧ 𝑥 <_{Q} 𝐵)) 

Theorem  ltbtwnnq 7172* 
There exists a number between any two positive fractions. Proposition
92.6(i) of [Gleason] p. 120.
(Contributed by NM, 17Mar1996.)
(Revised by Mario Carneiro, 10May2013.)

⊢ (𝐴 <_{Q} 𝐵 ↔ ∃𝑥(𝐴 <_{Q} 𝑥 ∧ 𝑥 <_{Q} 𝐵)) 

Theorem  archnqq 7173* 
For any fraction, there is an integer that is greater than it. This is
also known as the "archimedean property". (Contributed by Jim
Kingdon,
1Dec2019.)

⊢ (𝐴 ∈ Q → ∃𝑥 ∈ N 𝐴 <_{Q}
[⟨𝑥,
1_{o}⟩] ~_{Q} ) 

Theorem  prarloclemarch 7174* 
A version of the Archimedean property. This variation is "stronger"
than archnqq 7173 in the sense that we provide an integer which
is larger
than a given rational 𝐴 even after being multiplied by a
second
rational 𝐵. (Contributed by Jim Kingdon,
30Nov2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
∃𝑥 ∈
N 𝐴
<_{Q} ([⟨𝑥, 1_{o}⟩]
~_{Q} ·_{Q} 𝐵)) 

Theorem  prarloclemarch2 7175* 
Like prarloclemarch 7174 but the integer must be at least two, and
there is
also 𝐵 added to the right hand side. These
details follow
straightforwardly but are chosen to be helpful in the proof of
prarloc 7259. (Contributed by Jim Kingdon, 25Nov2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ ∃𝑥 ∈
N (1_{o} <_{N} 𝑥 ∧ 𝐴 <_{Q} (𝐵 +_{Q}
([⟨𝑥,
1_{o}⟩] ~_{Q}
·_{Q} 𝐶)))) 

Theorem  ltrnqg 7176 
Ordering property of reciprocal for positive fractions. For a simplified
version of the forward implication, see ltrnqi 7177. (Contributed by Jim
Kingdon, 29Dec2019.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<_{Q} 𝐵 ↔
(*_{Q}‘𝐵) <_{Q}
(*_{Q}‘𝐴))) 

Theorem  ltrnqi 7177 
Ordering property of reciprocal for positive fractions. For the converse,
see ltrnqg 7176. (Contributed by Jim Kingdon, 24Sep2019.)

⊢ (𝐴 <_{Q} 𝐵 →
(*_{Q}‘𝐵) <_{Q}
(*_{Q}‘𝐴)) 

Theorem  nnnq 7178 
The canonical embedding of positive integers into positive fractions.
(Contributed by Jim Kingdon, 26Apr2020.)

⊢ (𝐴 ∈ N → [⟨𝐴, 1_{o}⟩]
~_{Q} ∈ Q) 

Theorem  ltnnnq 7179 
Ordering of positive integers via <_{N} or <_{Q} is equivalent.
(Contributed by Jim Kingdon, 3Oct2020.)

⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<_{N} 𝐵 ↔ [⟨𝐴, 1_{o}⟩]
~_{Q} <_{Q} [⟨𝐵, 1_{o}⟩]
~_{Q} )) 

Definition  dfenq0 7180* 
Define equivalence relation for nonnegative fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. (Contributed by Jim
Kingdon, 2Nov2019.)

⊢ ~_{Q0} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·_{o} 𝑢) = (𝑤 ·_{o} 𝑣)))} 

Definition  dfnq0 7181 
Define class of nonnegative fractions. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only
by the construction. (Contributed by Jim Kingdon, 2Nov2019.)

⊢ Q_{0} = ((ω
× N) / ~_{Q0}
) 

Definition  df0nq0 7182 
Define nonnegative fraction constant 0. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only
by the construction. (Contributed by Jim Kingdon, 5Nov2019.)

⊢ 0_{Q0} =
[⟨∅, 1_{o}⟩]
~_{Q0} 

Definition  dfplq0 7183* 
Define addition on nonnegative fractions. This is a "temporary" set
used in the construction of complex numbers, and is intended to be used
only by the construction. (Contributed by Jim Kingdon, 2Nov2019.)

⊢ +_{Q0} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q_{0} ∧
𝑦 ∈
Q_{0}) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~_{Q0} ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~_{Q0} ) ∧
𝑧 = [⟨((𝑤 ·_{o} 𝑓) +_{o} (𝑣 ·_{o} 𝑢)), (𝑣 ·_{o} 𝑓)⟩] ~_{Q0}
))} 

Definition  dfmq0 7184* 
Define multiplication on nonnegative fractions. This is a
"temporary"
set used in the construction of complex numbers, and is intended to be
used only by the construction. (Contributed by Jim Kingdon,
2Nov2019.)

⊢ ·_{Q0} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q_{0} ∧
𝑦 ∈
Q_{0}) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~_{Q0} ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~_{Q0} ) ∧
𝑧 = [⟨(𝑤 ·_{o} 𝑢), (𝑣 ·_{o} 𝑓)⟩] ~_{Q0}
))} 

Theorem  dfmq0qs 7185* 
Multiplication on nonnegative fractions. This definition is similar to
dfmq0 7184 but expands Q_{0} (Contributed by Jim Kingdon,
22Nov2019.)

⊢ ·_{Q0} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((ω × N)
/ ~_{Q0} ) ∧ 𝑦 ∈ ((ω × N)
/ ~_{Q0} )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~_{Q0} ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~_{Q0} ) ∧
𝑧 = [⟨(𝑤 ·_{o} 𝑢), (𝑣 ·_{o} 𝑓)⟩] ~_{Q0}
))} 

Theorem  dfplq0qs 7186* 
Addition on nonnegative fractions. This definition is similar to
dfplq0 7183 but expands Q_{0} (Contributed by Jim Kingdon,
24Nov2019.)

⊢ +_{Q0} =
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((ω × N)
/ ~_{Q0} ) ∧ 𝑦 ∈ ((ω × N)
/ ~_{Q0} )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~_{Q0} ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~_{Q0} ) ∧
𝑧 = [⟨((𝑤 ·_{o} 𝑓) +_{o} (𝑣 ·_{o} 𝑢)), (𝑣 ·_{o} 𝑓)⟩] ~_{Q0}
))} 

Theorem  enq0enq 7187 
Equivalence on positive fractions in terms of equivalence on nonnegative
fractions. (Contributed by Jim Kingdon, 12Nov2019.)

⊢ ~_{Q} = (
~_{Q0} ∩ ((N × N)
× (N × N))) 

Theorem  enq0sym 7188 
The equivalence relation for nonnegative fractions is symmetric. Lemma
for enq0er 7191. (Contributed by Jim Kingdon, 14Nov2019.)

⊢ (𝑓 ~_{Q0} 𝑔 → 𝑔 ~_{Q0} 𝑓) 

Theorem  enq0ref 7189 
The equivalence relation for nonnegative fractions is reflexive. Lemma
for enq0er 7191. (Contributed by Jim Kingdon, 14Nov2019.)

⊢ (𝑓 ∈ (ω × N)
↔ 𝑓
~_{Q0} 𝑓) 

Theorem  enq0tr 7190 
The equivalence relation for nonnegative fractions is transitive. Lemma
for enq0er 7191. (Contributed by Jim Kingdon, 14Nov2019.)

⊢ ((𝑓 ~_{Q0} 𝑔 ∧ 𝑔 ~_{Q0} ℎ) → 𝑓 ~_{Q0} ℎ) 

Theorem  enq0er 7191 
The equivalence relation for nonnegative fractions is an equivalence
relation. (Contributed by Jim Kingdon, 12Nov2019.)

⊢ ~_{Q0} Er (ω
× N) 

Theorem  enq0breq 7192 
Equivalence relation for nonnegative fractions in terms of natural
numbers. (Contributed by NM, 27Aug1995.)

⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N))
→ (⟨𝐴, 𝐵⟩
~_{Q0} ⟨𝐶, 𝐷⟩ ↔ (𝐴 ·_{o} 𝐷) = (𝐵 ·_{o} 𝐶))) 

Theorem  enq0eceq 7193 
Equivalence class equality of nonnegative fractions in terms of natural
numbers. (Contributed by Jim Kingdon, 24Nov2019.)

⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N))
→ ([⟨𝐴, 𝐵⟩]
~_{Q0} = [⟨𝐶, 𝐷⟩] ~_{Q0} ↔
(𝐴 ·_{o}
𝐷) = (𝐵 ·_{o} 𝐶))) 

Theorem  nqnq0pi 7194 
A nonnegative fraction is a positive fraction if its numerator and
denominator are positive integers. (Contributed by Jim Kingdon,
10Nov2019.)

⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
[⟨𝐴, 𝐵⟩]
~_{Q0} = [⟨𝐴, 𝐵⟩] ~_{Q}
) 

Theorem  enq0ex 7195 
The equivalence relation for positive fractions exists. (Contributed by
Jim Kingdon, 18Nov2019.)

⊢ ~_{Q0} ∈
V 

Theorem  nq0ex 7196 
The class of positive fractions exists. (Contributed by Jim Kingdon,
18Nov2019.)

⊢ Q_{0} ∈
V 

Theorem  nqnq0 7197 
A positive fraction is a nonnegative fraction. (Contributed by Jim
Kingdon, 18Nov2019.)

⊢ Q ⊆
Q_{0} 

Theorem  nq0nn 7198* 
Decomposition of a nonnegative fraction into numerator and denominator.
(Contributed by Jim Kingdon, 24Nov2019.)

⊢ (𝐴 ∈ Q_{0} →
∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [⟨𝑤, 𝑣⟩] ~_{Q0}
)) 

Theorem  addcmpblnq0 7199 
Lemma showing compatibility of addition on nonnegative fractions.
(Contributed by Jim Kingdon, 23Nov2019.)

⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N)) ∧
((𝐹 ∈ ω ∧
𝐺 ∈ N)
∧ (𝑅 ∈ ω
∧ 𝑆 ∈
N))) → (((𝐴 ·_{o} 𝐷) = (𝐵 ·_{o} 𝐶) ∧ (𝐹 ·_{o} 𝑆) = (𝐺 ·_{o} 𝑅)) → ⟨((𝐴 ·_{o} 𝐺) +_{o} (𝐵 ·_{o} 𝐹)), (𝐵 ·_{o} 𝐺)⟩ ~_{Q0}
⟨((𝐶
·_{o} 𝑆)
+_{o} (𝐷
·_{o} 𝑅)),
(𝐷 ·_{o}
𝑆)⟩)) 

Theorem  mulcmpblnq0 7200 
Lemma showing compatibility of multiplication on nonnegative fractions.
(Contributed by Jim Kingdon, 20Nov2019.)

⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N)) ∧
((𝐹 ∈ ω ∧
𝐺 ∈ N)
∧ (𝑅 ∈ ω
∧ 𝑆 ∈
N))) → (((𝐴 ·_{o} 𝐷) = (𝐵 ·_{o} 𝐶) ∧ (𝐹 ·_{o} 𝑆) = (𝐺 ·_{o} 𝑅)) → ⟨(𝐴 ·_{o} 𝐹), (𝐵 ·_{o} 𝐺)⟩ ~_{Q0}
⟨(𝐶
·_{o} 𝑅),
(𝐷 ·_{o}
𝑆)⟩)) 