Type  Label  Description 
Statement 

Syntax  c0r 6801 
The signed real constant 0.

class 0_{R} 

Syntax  c1r 6802 
The signed real constant 1.

class 1_{R} 

Syntax  cm1r 6803 
The signed real constant 1.

class 1_{R} 

Syntax  cplr 6804 
Signed real addition.

class +_{R} 

Syntax  cmr 6805 
Signed real multiplication.

class
·_{R} 

Syntax  cltr 6806 
Signed real ordering relation.

class
<_{R} 

Definition  dfni 6807 
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 6808 
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 6809 
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 6810 
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 6811 
Membership in the class of positive integers. (Contributed by NM,
15Aug1995.)

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

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

⊢ (𝐴 ∈ N → 𝐴 ∈
ω) 

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

⊢ (𝐴 ∈ N → 𝐴 ∈ On) 

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

⊢ (𝐴 ∈ N → Ord 𝐴) 

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

⊢ N ∈ V 

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

⊢ ¬ ∅ ∈
N 

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

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

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

⊢ 1_{𝑜} ∈
N 

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

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

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

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

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

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

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

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

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

⊢ <_{N} Or
N 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  ltexpi 6840* 
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 6841 
Ordering property of addition for positive integers. (Contributed by Jim
Kingdon, 31Aug2019.)

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

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

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

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

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

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

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

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

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

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

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

Definition  dfplpq 6847* 
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 6852) works with the equivalence classes of these
ordered pairs determined by the equivalence relation ~_{Q}
(dfenq 6850). (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 6848* 
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 6849* 
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 6850* 
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 6851 
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 6852* 
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 6853* 
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 6854 
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 6855* 
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 6856* 
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 6857* 
Alternate definition of preaddition on positive fractions.
(Contributed by Jim Kingdon, 12Sep2019.)

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

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

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

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

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

Theorem  enqbreq2 6860 
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 6861 
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 6862 
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 6863 
The equivalence relation for positive fractions exists. (Contributed by
NM, 3Sep1995.)

⊢ ~_{Q} ∈
V 

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

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

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

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

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

⊢ Q ∈ V 

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

⊢ ¬ ∅ ∈
Q 

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

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

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

⊢ 1_{Q} ∈
Q 

Theorem  addcmpblnq 6870 
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 6871 
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 6872 
Lemma for addpipqqs 6873. (Contributed by Jim Kingdon, 11Sep2019.)

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

Theorem  addpipqqs 6873 
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 6874 
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 6875 
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 6876 
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 6877 
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 6878 
Closure of addition on positive fractions. (Contributed by NM,
29Aug1995.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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