Type  Label  Description 
Statement 

Theorem  mulpiord 6301 
Positive integer multiplication in terms of ordinal multiplication.
(Contributed by NM, 27Aug1995.)

⊢ ((A ∈ N ∧ B ∈ N) → (A ·_{N} B) = (A
·_{𝑜} B)) 

Theorem  mulidpi 6302 
1 is an identity element for multiplication on positive integers.
(Contributed by NM, 4Mar1996.) (Revised by Mario Carneiro,
17Nov2014.)

⊢ (A ∈ N → (A ·_{N}
1_{𝑜}) = A) 

Theorem  ltpiord 6303 
Positive integer 'less than' in terms of ordinal membership. (Contributed
by NM, 6Feb1996.) (Revised by Mario Carneiro, 28Apr2015.)

⊢ ((A ∈ N ∧ B ∈ N) → (A <_{N} B ↔ A
∈ B)) 

Theorem  ltsopi 6304 
Positive integer 'less than' is a strict ordering. (Contributed by NM,
8Feb1996.) (Proof shortened by Mario Carneiro, 10Jul2014.)

⊢ <_{N} Or
N 

Theorem  pitric 6305 
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21Sep2019.)

⊢ ((A ∈ N ∧ B ∈ N) → (A <_{N} B ↔ ¬ (A = B ∨ B
<_{N} A))) 

Theorem  pitri3or 6306 
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21Sep2019.)

⊢ ((A ∈ N ∧ B ∈ N) → (A <_{N} B ∨ A = B ∨ B
<_{N} A)) 

Theorem  ltdcpi 6307 
Lessthan for positive integers is decidable. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ ((A ∈ N ∧ B ∈ N) → DECID
A <_{N} B) 

Theorem  ltrelpi 6308 
Positive integer 'less than' is a relation on positive integers.
(Contributed by NM, 8Feb1996.)

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

Theorem  dmaddpi 6309 
Domain of addition on positive integers. (Contributed by NM,
26Aug1995.)

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

Theorem  dmmulpi 6310 
Domain of multiplication on positive integers. (Contributed by NM,
26Aug1995.)

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

Theorem  addclpi 6311 
Closure of addition of positive integers. (Contributed by NM,
18Oct1995.)

⊢ ((A ∈ N ∧ B ∈ N) → (A +_{N} B) ∈
N) 

Theorem  mulclpi 6312 
Closure of multiplication of positive integers. (Contributed by NM,
18Oct1995.)

⊢ ((A ∈ N ∧ B ∈ N) → (A ·_{N} B) ∈
N) 

Theorem  addcompig 6313 
Addition of positive integers is commutative. (Contributed by Jim
Kingdon, 26Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N) → (A +_{N} B) = (B
+_{N} A)) 

Theorem  addasspig 6314 
Addition of positive integers is associative. (Contributed by Jim
Kingdon, 26Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → ((A
+_{N} B)
+_{N} 𝐶) = (A
+_{N} (B
+_{N} 𝐶))) 

Theorem  mulcompig 6315 
Multiplication of positive integers is commutative. (Contributed by Jim
Kingdon, 26Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N) → (A ·_{N} B) = (B
·_{N} A)) 

Theorem  mulasspig 6316 
Multiplication of positive integers is associative. (Contributed by Jim
Kingdon, 26Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → ((A
·_{N} B)
·_{N} 𝐶) = (A
·_{N} (B
·_{N} 𝐶))) 

Theorem  distrpig 6317 
Multiplication of positive integers is distributive. (Contributed by Jim
Kingdon, 26Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → (A
·_{N} (B
+_{N} 𝐶)) = ((A ·_{N} B) +_{N} (A ·_{N} 𝐶))) 

Theorem  addcanpig 6318 
Addition cancellation law for positive integers. (Contributed by Jim
Kingdon, 27Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → ((A
+_{N} B) = (A +_{N} 𝐶) ↔ B = 𝐶)) 

Theorem  mulcanpig 6319 
Multiplication cancellation law for positive integers. (Contributed by
Jim Kingdon, 29Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → ((A
·_{N} B) =
(A ·_{N}
𝐶) ↔ B = 𝐶)) 

Theorem  addnidpig 6320 
There is no identity element for addition on positive integers.
(Contributed by NM, 28Nov1995.)

⊢ ((A ∈ N ∧ B ∈ N) → ¬ (A +_{N} B) = A) 

Theorem  ltexpi 6321* 
Ordering on positive integers in terms of existence of sum.
(Contributed by NM, 15Mar1996.) (Revised by Mario Carneiro,
14Jun2013.)

⊢ ((A ∈ N ∧ B ∈ N) → (A <_{N} B ↔ ∃x ∈ N (A +_{N} x) = B)) 

Theorem  ltapig 6322 
Ordering property of addition for positive integers. (Contributed by Jim
Kingdon, 31Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → (A
<_{N} B ↔
(𝐶
+_{N} A)
<_{N} (𝐶 +_{N} B))) 

Theorem  ltmpig 6323 
Ordering property of multiplication for positive integers. (Contributed
by Jim Kingdon, 31Aug2019.)

⊢ ((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → (A
<_{N} B ↔
(𝐶
·_{N} A)
<_{N} (𝐶 ·_{N}
B))) 

Theorem  1lt2pi 6324 
One is less than two (one plus one). (Contributed by NM, 13Mar1996.)

⊢ 1_{𝑜}
<_{N} (1_{𝑜}
+_{N} 1_{𝑜}) 

Theorem  nlt1pig 6325 
No positive integer is less than one. (Contributed by Jim Kingdon,
31Aug2019.)

⊢ (A ∈ N → ¬ A <_{N}
1_{𝑜}) 

Theorem  indpi 6326* 
Principle of Finite Induction on positive integers. (Contributed by NM,
23Mar1996.)

⊢ (x =
1_{𝑜} → (φ ↔
ψ)) & ⊢ (x = y →
(φ ↔ χ)) & ⊢ (x = (y
+_{N} 1_{𝑜}) → (φ ↔ θ)) & ⊢ (x = A →
(φ ↔ τ)) & ⊢ ψ
& ⊢ (y ∈ N → (χ → θ)) ⇒ ⊢ (A ∈
N → τ) 

Theorem  nnppipi 6327 
A natural number plus a positive integer is a positive integer.
(Contributed by Jim Kingdon, 10Nov2019.)

⊢ ((A ∈ 𝜔 ∧
B ∈
N) → (A
+_{𝑜} B) ∈ N) 

Definition  dfplpq 6328* 
Define preaddition 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. This "preaddition" operation works
directly
with ordered pairs of integers. The actual positive fraction addition
+_{Q} (dfplqqs 6333) works with the equivalence classes of these
ordered pairs determined by the equivalence relation ~_{Q}
(dfenq 6331). (Analogous remarks apply to the other
"pre" operations
in the complex number construction that follows.) From Proposition
92.3 of [Gleason] p. 117. (Contributed
by NM, 28Aug1995.)

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

Definition  dfmpq 6329* 
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} =
(x ∈
(N × N), y ∈
(N × N) ↦ ⟨((1^{st}
‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) 

Definition  dfltpq 6330* 
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} =
{⟨x, y⟩ ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
((1^{st} ‘x)
·_{N} (2^{nd} ‘y)) <_{N} ((1^{st}
‘y)
·_{N} (2^{nd} ‘x)))} 

Definition  dfenq 6331* 
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} = {⟨x, y⟩
∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃z∃w∃v∃u((x =
⟨z, w⟩ ∧ y = ⟨v,
u⟩) ∧ (z
·_{N} u) =
(w ·_{N}
v)))} 

Definition  dfnqqs 6332 
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 6333* 
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} =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [⟨w,
v⟩] ~_{Q} ∧ y =
[⟨u, f⟩] ~_{Q} ) ∧ z =
[(⟨w, v⟩ +_{pQ} ⟨u, f⟩)]
~_{Q} ))} 

Definition  dfmqqs 6334* 
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} =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [⟨w,
v⟩] ~_{Q} ∧ y =
[⟨u, f⟩] ~_{Q} ) ∧ z =
[(⟨w, v⟩ ·_{pQ}
⟨u, f⟩)] ~_{Q}
))} 

Definition  df1nqqs 6335 
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_{𝑜}, 1_{𝑜}⟩]
~_{Q} 

Definition  dfrq 6336* 
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} = {⟨x, y⟩
∣ (x ∈ Q ∧ y ∈ Q ∧ (x
·_{Q} y) =
1_{Q})} 

Definition  dfltnqqs 6337* 
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} =
{⟨x, y⟩ ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃z∃w∃v∃u((x = [⟨z,
w⟩] ~_{Q} ∧ y =
[⟨v, u⟩] ~_{Q} ) ∧ (z
·_{N} u)
<_{N} (w
·_{N} v)))} 

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

⊢ +_{pQ} =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
∃w∃v∃u∃f((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨((w
·_{N} f)
+_{N} (v
·_{N} u)),
(v ·_{N}
f)⟩))} 

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

⊢ ·_{pQ} =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
∃w∃v∃u∃f((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨(w
·_{N} u),
(v ·_{N}
f)⟩))} 

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

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

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

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

Theorem  enqer 6342 
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 6343 
Equivalence class equality of positive fractions in terms of positive
integers. (Contributed by NM, 29Nov1995.)

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

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

⊢ ~_{Q} ∈ V 

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

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

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

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

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

⊢ Q ∈ V 

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

⊢ ¬ ∅ ∈ Q 

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

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

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

⊢ 1_{Q} ∈ Q 

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

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

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

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

Theorem  addpipqqslem 6353 
Lemma for addpipqqs 6354. (Contributed by Jim Kingdon, 11Sep2019.)

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ((A ∈ Q ∧ B ∈ Q) → (A +_{Q} B) ∈
Q) 

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

⊢ ((A ∈ Q ∧ B ∈ Q) → (A ·_{Q} B) ∈
Q) 

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

⊢ (x ∈ Q → ∃w∃v x = [⟨w,
v⟩] ~_{Q}
) 

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

⊢ (A ∈ Q → ∃w∃v((w ∈
N ∧ v ∈
N) ∧ A = [⟨w,
v⟩] ~_{Q}
)) 

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

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

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

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

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

⊢ ((A ∈ Q ∧ B ∈ Q) → (A +_{Q} B) = (B
+_{Q} A)) 

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

⊢ ((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈
Q) → ((A
+_{Q} B)
+_{Q} 𝐶) = (A
+_{Q} (B
+_{Q} 𝐶))) 

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

⊢ ((A ∈ Q ∧ B ∈ Q) → (A ·_{Q} B) = (B
·_{Q} A)) 

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

⊢ ((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈
Q) → ((A
·_{Q} B)
·_{Q} 𝐶) = (A
·_{Q} (B
·_{Q} 𝐶))) 

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

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

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

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

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

⊢ ((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈
Q) → (A
·_{Q} (B
+_{Q} 𝐶)) = ((A ·_{Q} B) +_{Q} (A ·_{Q} 𝐶))) 

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

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

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

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

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

⊢ (A ∈ Q → ∃y(y ∈
Q ∧ (A ·_{Q} y) = 1_{Q})) 

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

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

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

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

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

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

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

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

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

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

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

⊢ ((A ∈ Q ∧ B ∈ Q) → (A <_{Q} B ∨ A = B ∨ B
<_{Q} A)) 

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

⊢ ((A ∈ Q ∧ B ∈ Q) → DECID
A <_{Q} B) 

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

⊢ <_{Q} Or
Q 

Theorem  nqtric 6383 
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21Sep2019.)

⊢ ((A ∈ Q ∧ B ∈ Q) → (A <_{Q} B ↔ ¬ (A = B ∨ B
<_{Q} A))) 

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

⊢ ((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈
Q) → (A
<_{Q} B ↔
(𝐶
+_{Q} A)
<_{Q} (𝐶 +_{Q} B))) 

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

⊢ ((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈
Q) → (A
<_{Q} B ↔
(𝐶
·_{Q} A)
<_{Q} (𝐶 ·_{Q}
B))) 

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

⊢ ((A
<_{Q} B ∧ 𝐶 ∈
Q) → (𝐶
+_{Q} A)
<_{Q} (𝐶 +_{Q} B)) 

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

⊢ ((A
<_{Q} B ∧ 𝐶 ∈
Q) → (𝐶
·_{Q} A)
<_{Q} (𝐶 ·_{Q}
B)) 

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

⊢ (((A ∈ Q ∧ B ∈ Q) ∧ (𝐶 ∈
Q ∧ 𝐷 ∈
Q)) → ((A
<_{Q} B ∧ 𝐶 <_{Q} 𝐷) → (A +_{Q} 𝐶) <_{Q} (B +_{Q} 𝐷))) 

Theorem  1lt2nq 6389 
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 6390 
The sum of two fractions is greater than one of them. (Contributed by
NM, 14Mar1996.) (Revised by Mario Carneiro, 10May2013.)

⊢ ((A ∈ Q ∧ B ∈ Q) → A <_{Q} (A +_{Q} B)) 

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

⊢ ((A ∈ Q ∧ B ∈ Q) → (A <_{Q} B ↔ ∃x ∈ Q (A +_{Q} x) = B)) 

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

⊢ (A
<_{Q} B →
∃x
∈ Q (A +_{Q} x) = B) 

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

⊢ (A ∈ Q → ∃x ∈ Q (x +_{Q} x) = A) 

Theorem  halfnq 6394* 
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.)

⊢ (A ∈ Q → ∃x(x +_{Q} x) = A) 

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

⊢ (A ∈ Q → ∃x ∈ Q x <_{Q} A) 

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

⊢ (A ∈ Q → ∃x x <_{Q} A) 

Theorem  subhalfnqq 6397* 
There is a number which is less than half of any positive fraction. The
case where A
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 6393). (Contributed by Jim Kingdon,
25Nov2019.)

⊢ (A ∈ Q → ∃x ∈ Q (x +_{Q} x) <_{Q} A) 

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

⊢ (A
<_{Q} B ↔
∃x
∈ Q (A <_{Q} x ∧ x <_{Q} B)) 

Theorem  ltbtwnnq 6399* 
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.)

⊢ (A
<_{Q} B ↔
∃x(A
<_{Q} x ∧ x
<_{Q} B)) 

Theorem  archnqq 6400* 
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.)

⊢ (A ∈ Q → ∃x ∈ N A <_{Q} [⟨x, 1_{𝑜}⟩]
~_{Q} ) 