Type  Label  Description 
Statement 

Syntax  cltr 6401 
Signed real ordering relation.

class
<_{R} 

Definition  dfni 6402 
Define the class of positive integers. This is a "temporary" set
used in
the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 15Aug1995.)

⊢ N = (ω ∖
{∅}) 

Definition  dfpli 6403 
Define addition on positive integers. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 26Aug1995.)

⊢ +_{N} = (
+_{𝑜} ↾ (N ×
N)) 

Definition  dfmi 6404 
Define multiplication on positive integers. This is a "temporary"
set
used in the construction of complex numbers and is intended to be used
only by the construction. (Contributed by NM, 26Aug1995.)

⊢ ·_{N} = (
·_{𝑜} ↾ (N ×
N)) 

Definition  dflti 6405 
Define 'less than' on positive integers. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 6Feb1996.)

⊢ <_{N} = ( E ∩
(N × N)) 

Theorem  elni 6406 
Membership in the class of positive integers. (Contributed by NM,
15Aug1995.)

⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠
∅)) 

Theorem  pinn 6407 
A positive integer is a natural number. (Contributed by NM,
15Aug1995.)

⊢ (𝐴 ∈ N → 𝐴 ∈
ω) 

Theorem  pion 6408 
A positive integer is an ordinal number. (Contributed by NM,
23Mar1996.)

⊢ (𝐴 ∈ N → 𝐴 ∈ On) 

Theorem  piord 6409 
A positive integer is ordinal. (Contributed by NM, 29Jan1996.)

⊢ (𝐴 ∈ N → Ord 𝐴) 

Theorem  niex 6410 
The class of positive integers is a set. (Contributed by NM,
15Aug1995.)

⊢ N ∈ V 

Theorem  0npi 6411 
The empty set is not a positive integer. (Contributed by NM,
26Aug1995.)

⊢ ¬ ∅ ∈
N 

Theorem  elni2 6412 
Membership in the class of positive integers. (Contributed by NM,
27Nov1995.)

⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅
∈ 𝐴)) 

Theorem  1pi 6413 
Ordinal 'one' is a positive integer. (Contributed by NM, 29Oct1995.)

⊢ 1_{𝑜} ∈
N 

Theorem  addpiord 6414 
Positive integer addition in terms of ordinal addition. (Contributed by
NM, 27Aug1995.)

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

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

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

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

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

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

⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<_{N} 𝐵 ↔ 𝐴 ∈ 𝐵)) 

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

⊢ <_{N} Or
N 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ (𝑥 = 1_{𝑜} → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +_{N}
1_{𝑜}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ N →
(𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ N → 𝜏) 

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

⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) → (𝐴 +_{𝑜} 𝐵) ∈
N) 

Definition  dfplpq 6442* 
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 6447) works with the equivalence classes of these
ordered pairs determined by the equivalence relation ~_{Q}
(dfenq 6445). (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} = (𝑥 ∈ (N
× N), 𝑦 ∈ (N ×
N) ↦ ⟨(((1^{st} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦))
+_{N} ((1^{st} ‘𝑦) ·_{N}
(2^{nd} ‘𝑥))), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) 

Definition  dfmpq 6443* 
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 6444* 
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 6445* 
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 6446 
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 6447* 
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 6448* 
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 6449 
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 6450* 
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 6451* 
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 6452* 
Alternative definition of preaddition on positive fractions.
(Contributed by Jim Kingdon, 12Sep2019.)

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

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

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

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

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

Theorem  enqbreq2 6455 
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 6456 
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 6457 
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 6458 
The equivalence relation for positive fractions exists. (Contributed by
NM, 3Sep1995.)

⊢ ~_{Q} ∈
V 

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

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

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

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

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

⊢ Q ∈ V 

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

⊢ ¬ ∅ ∈
Q 

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

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

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

⊢ 1_{Q} ∈
Q 

Theorem  addcmpblnq 6465 
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 6466 
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 6467 
Lemma for addpipqqs 6468. (Contributed by Jim Kingdon, 11Sep2019.)

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

Theorem  addpipqqs 6468 
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 6469 
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 6470 
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 6471 
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 6472 
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 6473 
Closure of addition on positive fractions. (Contributed by NM,
29Aug1995.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  mulcanenq 6483 
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 6484 
Lemma for distributive law: cancellation of common factor. (Contributed
by Jim Kingdon, 17Sep2019.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ <_{Q} Or
Q 

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

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

Theorem  ltanqg 6498 
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 6499 
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 6500 
Ordering property of addition for positive fractions. One direction of
ltanqg 6498. (Contributed by Jim Kingdon, 9Dec2019.)

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