Type  Label  Description 
Statement 

Theorem  recexprlemloc 6601* 
B is located.
Lemma for recexpr 6608. (Contributed by Jim Kingdon,
27Dec2019.)

⊢ B =
⟨{x ∣ ∃y(x <_{Q} y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))}, {x
∣ ∃y(y
<_{Q} x ∧ (*_{Q}‘y) ∈
(1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈
P → ∀𝑞 ∈
Q ∀𝑟 ∈
Q (𝑞
<_{Q} 𝑟 → (𝑞 ∈
(1^{st} ‘B) ∨ 𝑟 ∈
(2^{nd} ‘B)))) 

Theorem  recexprlempr 6602* 
B is a positive
real. Lemma for recexpr 6608. (Contributed by Jim
Kingdon, 27Dec2019.)

⊢ B =
⟨{x ∣ ∃y(x <_{Q} y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))}, {x
∣ ∃y(y
<_{Q} x ∧ (*_{Q}‘y) ∈
(1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈
P → B ∈ P) 

Theorem  recexprlem1ssl 6603* 
The lower cut of one is a subset of the lower cut of A ·_{P} B.
Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27Dec2019.)

⊢ B =
⟨{x ∣ ∃y(x <_{Q} y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))}, {x
∣ ∃y(y
<_{Q} x ∧ (*_{Q}‘y) ∈
(1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈
P → (1^{st} ‘1_{P})
⊆ (1^{st} ‘(A
·_{P} B))) 

Theorem  recexprlem1ssu 6604* 
The upper cut of one is a subset of the upper cut of A ·_{P} B.
Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27Dec2019.)

⊢ B =
⟨{x ∣ ∃y(x <_{Q} y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))}, {x
∣ ∃y(y
<_{Q} x ∧ (*_{Q}‘y) ∈
(1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈
P → (2^{nd} ‘1_{P})
⊆ (2^{nd} ‘(A
·_{P} B))) 

Theorem  recexprlemss1l 6605* 
The lower cut of A
·_{P} B
is a subset of the lower cut of one. Lemma
for recexpr 6608. (Contributed by Jim Kingdon, 27Dec2019.)

⊢ B =
⟨{x ∣ ∃y(x <_{Q} y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))}, {x
∣ ∃y(y
<_{Q} x ∧ (*_{Q}‘y) ∈
(1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈
P → (1^{st} ‘(A ·_{P} B)) ⊆ (1^{st}
‘1_{P})) 

Theorem  recexprlemss1u 6606* 
The upper cut of A
·_{P} B
is a subset of the upper cut of one. Lemma
for recexpr 6608. (Contributed by Jim Kingdon, 27Dec2019.)

⊢ B =
⟨{x ∣ ∃y(x <_{Q} y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))}, {x
∣ ∃y(y
<_{Q} x ∧ (*_{Q}‘y) ∈
(1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈
P → (2^{nd} ‘(A ·_{P} B)) ⊆ (2^{nd}
‘1_{P})) 

Theorem  recexprlemex 6607* 
B is the reciprocal
of A. Lemma for recexpr 6608. (Contributed
by Jim Kingdon, 27Dec2019.)

⊢ B =
⟨{x ∣ ∃y(x <_{Q} y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))}, {x
∣ ∃y(y
<_{Q} x ∧ (*_{Q}‘y) ∈
(1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈
P → (A
·_{P} B) =
1_{P}) 

Theorem  recexpr 6608* 
The reciprocal of a positive real exists. Part of Proposition 93.7(v)
of [Gleason] p. 124. (Contributed by
NM, 15May1996.) (Revised by
Mario Carneiro, 12Jun2013.)

⊢ (A ∈ P → ∃x ∈ P (A ·_{P} x) = 1_{P}) 

Theorem  aptiprleml 6609 
Lemma for aptipr 6611. (Contributed by Jim Kingdon, 28Jan2020.)

⊢ ((A ∈ P ∧ B ∈ P ∧ ¬ B<_{P} A) → (1^{st} ‘A) ⊆ (1^{st} ‘B)) 

Theorem  aptiprlemu 6610 
Lemma for aptipr 6611. (Contributed by Jim Kingdon, 28Jan2020.)

⊢ ((A ∈ P ∧ B ∈ P ∧ ¬ B<_{P} A) → (2^{nd} ‘B) ⊆ (2^{nd} ‘A)) 

Theorem  aptipr 6611 
Apartness of positive reals is tight. (Contributed by Jim Kingdon,
28Jan2020.)

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

Theorem  ltmprr 6612 
Ordering property of multiplication. (Contributed by Jim Kingdon,
18Feb2020.)

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

Theorem  archpr 6613* 
For any positive real, there is an integer that is greater than it.
This is also known as the "archimedean property". The integer
x is
embedded into the reals as described at nnprlu 6533. (Contributed by Jim
Kingdon, 22Apr2020.)

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

Definition  dfenr 6614* 
Define equivalence relation for signed reals. This is a "temporary"
set
used in the construction of complex numbers, and is intended to be used
only by the construction. From Proposition 94.1 of [Gleason] p. 126.
(Contributed by NM, 25Jul1995.)

⊢ ~_{R} = {⟨x, y⟩
∣ ((x ∈ (P × P) ∧ y ∈ (P × P)) ∧ ∃z∃w∃v∃u((x =
⟨z, w⟩ ∧ y = ⟨v,
u⟩) ∧ (z
+_{P} u) = (w +_{P} v)))} 

Definition  dfnr 6615 
Define class of signed reals. This is a "temporary" set used in the
construction of complex numbers, and is intended to be used only by the
construction. From Proposition 94.2 of [Gleason] p. 126. (Contributed
by NM, 25Jul1995.)

⊢ R = ((P ×
P) / ~_{R} ) 

Definition  dfplr 6616* 
Define addition on signed reals. This is a "temporary" set used in
the
construction of complex numbers, and is intended to be used only by the
construction. From Proposition 94.3 of [Gleason] p. 126. (Contributed
by NM, 25Aug1995.)

⊢ +_{R} =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈
R ∧ y ∈
R) ∧ ∃w∃v∃u∃f((x = [⟨w,
v⟩] ~_{R} ∧ y =
[⟨u, f⟩] ~_{R} ) ∧ z =
[⟨(w +_{P}
u), (v
+_{P} f)⟩]
~_{R} ))} 

Definition  dfmr 6617* 
Define multiplication on signed reals. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only
by the construction. From Proposition 94.3 of [Gleason] p. 126.
(Contributed by NM, 25Aug1995.)

⊢ ·_{R} =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈
R ∧ y ∈
R) ∧ ∃w∃v∃u∃f((x = [⟨w,
v⟩] ~_{R} ∧ y =
[⟨u, f⟩] ~_{R} ) ∧ z =
[⟨((w
·_{P} u)
+_{P} (v
·_{P} f)),
((w ·_{P}
f) +_{P} (v ·_{P} u))⟩] ~_{R}
))} 

Definition  dfltr 6618* 
Define ordering relation on signed reals. This is a "temporary" set
used in the construction of complex numbers, and is intended to be used
only by the construction. From Proposition 94.4 of [Gleason] p. 127.
(Contributed by NM, 14Feb1996.)

⊢ <_{R} =
{⟨x, y⟩ ∣ ((x ∈
R ∧ y ∈
R) ∧ ∃z∃w∃v∃u((x = [⟨z,
w⟩] ~_{R} ∧ y =
[⟨v, u⟩] ~_{R} ) ∧ (z
+_{P} u)<_{P} (w +_{P} v)))} 

Definition  df0r 6619 
Define signed real constant 0. This is a "temporary" set used in the
construction of complex numbers, and is intended to be used only by the
construction. From Proposition 94.2 of [Gleason] p. 126. (Contributed
by NM, 9Aug1995.)

⊢ 0_{R} =
[⟨1_{P}, 1_{P}⟩]
~_{R} 

Definition  df1r 6620 
Define signed real 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 94.2 of [Gleason] p. 126. (Contributed
by NM, 9Aug1995.)

⊢ 1_{R} =
[⟨(1_{P} +_{P}
1_{P}), 1_{P}⟩]
~_{R} 

Definition  dfm1r 6621 
Define signed real constant 1. 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, 9Aug1995.)

⊢ 1_{R} =
[⟨1_{P}, (1_{P}
+_{P} 1_{P})⟩]
~_{R} 

Theorem  enrbreq 6622 
Equivalence relation for signed reals in terms of positive reals.
(Contributed by NM, 3Sep1995.)

⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) → (⟨A,
B⟩ ~_{R}
⟨𝐶, 𝐷⟩ ↔ (A +_{P} 𝐷) = (B
+_{P} 𝐶))) 

Theorem  enrer 6623 
The equivalence relation for signed reals is an equivalence relation.
Proposition 94.1 of [Gleason] p. 126.
(Contributed by NM,
3Sep1995.) (Revised by Mario Carneiro, 6Jul2015.)

⊢ ~_{R} Er
(P × P) 

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

⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) → ([⟨A,
B⟩] ~_{R} =
[⟨𝐶, 𝐷⟩]
~_{R} ↔ (A
+_{P} 𝐷) = (B
+_{P} 𝐶))) 

Theorem  enrex 6625 
The equivalence relation for signed reals exists. (Contributed by NM,
25Jul1995.)

⊢ ~_{R} ∈ V 

Theorem  ltrelsr 6626 
Signed real 'less than' is a relation on signed reals. (Contributed by
NM, 14Feb1996.)

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

Theorem  addcmpblnr 6627 
Lemma showing compatibility of addition. (Contributed by NM,
3Sep1995.)

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

Theorem  mulcmpblnrlemg 6628 
Lemma used in lemma showing compatibility of multiplication.
(Contributed by Jim Kingdon, 1Jan2020.)

⊢ ((((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) ∧ ((𝐹 ∈
P ∧ 𝐺 ∈
P) ∧ (𝑅 ∈
P ∧ 𝑆 ∈
P))) → (((A
+_{P} 𝐷) = (B
+_{P} 𝐶) ∧ (𝐹 +_{P}
𝑆) = (𝐺 +_{P} 𝑅)) → ((𝐷 ·_{P} 𝐹) +_{P}
(((A ·_{P}
𝐹)
+_{P} (B
·_{P} 𝐺)) +_{P} ((𝐶
·_{P} 𝑆) +_{P} (𝐷
·_{P} 𝑅)))) = ((𝐷 ·_{P} 𝐹) +_{P}
(((A ·_{P}
𝐺)
+_{P} (B
·_{P} 𝐹)) +_{P} ((𝐶
·_{P} 𝑅) +_{P} (𝐷
·_{P} 𝑆)))))) 

Theorem  mulcmpblnr 6629 
Lemma showing compatibility of multiplication. (Contributed by NM,
5Sep1995.)

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

Theorem  prsrlem1 6630* 
Decomposing signed reals into positive reals. Lemma for addsrpr 6633 and
mulsrpr 6634. (Contributed by Jim Kingdon, 30Dec2019.)

⊢ (((A ∈ ((P × P)
/ ~_{R} ) ∧
B ∈
((P × P) /
~_{R} )) ∧ ((A = [⟨w,
v⟩] ~_{R} ∧ B =
[⟨u, 𝑡⟩] ~_{R} ) ∧ (A =
[⟨𝑠, f⟩] ~_{R} ∧ B =
[⟨g, ℎ⟩] ~_{R} )))
→ ((((w ∈ P ∧ v ∈ P) ∧ (𝑠 ∈
P ∧ f ∈
P)) ∧ ((u ∈
P ∧ 𝑡 ∈
P) ∧ (g ∈
P ∧ ℎ ∈
P))) ∧ ((w +_{P} f) = (v
+_{P} 𝑠) ∧
(u +_{P} ℎ) = (𝑡 +_{P} g)))) 

Theorem  addsrmo 6631* 
There is at most one result from adding signed reals. (Contributed by
Jim Kingdon, 30Dec2019.)

⊢ ((A ∈ ((P × P)
/ ~_{R} ) ∧
B ∈
((P × P) /
~_{R} )) → ∃*z∃w∃v∃u∃𝑡((A =
[⟨w, v⟩] ~_{R} ∧ B =
[⟨u, 𝑡⟩] ~_{R} ) ∧ z =
[⟨(w +_{P}
u), (v
+_{P} 𝑡)⟩] ~_{R}
)) 

Theorem  mulsrmo 6632* 
There is at most one result from multiplying signed reals. (Contributed
by Jim Kingdon, 30Dec2019.)

⊢ ((A ∈ ((P × P)
/ ~_{R} ) ∧
B ∈
((P × P) /
~_{R} )) → ∃*z∃w∃v∃u∃𝑡((A =
[⟨w, v⟩] ~_{R} ∧ B =
[⟨u, 𝑡⟩] ~_{R} ) ∧ z =
[⟨((w
·_{P} u)
+_{P} (v
·_{P} 𝑡)), ((w
·_{P} 𝑡) +_{P} (v ·_{P} u))⟩] ~_{R}
)) 

Theorem  addsrpr 6633 
Addition of signed reals in terms of positive reals. (Contributed by
NM, 3Sep1995.) (Revised by Mario Carneiro, 12Aug2015.)

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

Theorem  mulsrpr 6634 
Multiplication of signed reals in terms of positive reals. (Contributed
by NM, 3Sep1995.) (Revised by Mario Carneiro, 12Aug2015.)

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

Theorem  ltsrprg 6635 
Ordering of signed reals in terms of positive reals. (Contributed by
Jim Kingdon, 2Jan2019.)

⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) → ([⟨A,
B⟩] ~_{R}
<_{R} [⟨𝐶, 𝐷⟩] ~_{R} ↔
(A +_{P} 𝐷)<_{P}
(B +_{P} 𝐶))) 

Theorem  gt0srpr 6636 
Greater than zero in terms of positive reals. (Contributed by NM,
13May1996.)

⊢ (0_{R}
<_{R} [⟨A,
B⟩] ~_{R}
↔ B<_{P}
A) 

Theorem  0nsr 6637 
The empty set is not a signed real. (Contributed by NM, 25Aug1995.)
(Revised by Mario Carneiro, 10Jul2014.)

⊢ ¬ ∅ ∈ R 

Theorem  0r 6638 
The constant 0_{R} is a signed
real. (Contributed by NM, 9Aug1995.)

⊢ 0_{R} ∈ R 

Theorem  1sr 6639 
The constant 1_{R} is a signed
real. (Contributed by NM, 9Aug1995.)

⊢ 1_{R} ∈ R 

Theorem  m1r 6640 
The constant 1_{R} is a signed
real. (Contributed by NM,
9Aug1995.)

⊢ 1_{R} ∈ R 

Theorem  addclsr 6641 
Closure of addition on signed reals. (Contributed by NM,
25Jul1995.)

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

Theorem  mulclsr 6642 
Closure of multiplication on signed reals. (Contributed by NM,
10Aug1995.)

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

Theorem  addcomsrg 6643 
Addition of signed reals is commutative. (Contributed by Jim Kingdon,
3Jan2020.)

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

Theorem  addasssrg 6644 
Addition of signed reals is associative. (Contributed by Jim Kingdon,
3Jan2020.)

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

Theorem  mulcomsrg 6645 
Multiplication of signed reals is commutative. (Contributed by Jim
Kingdon, 3Jan2020.)

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

Theorem  mulasssrg 6646 
Multiplication of signed reals is associative. (Contributed by Jim
Kingdon, 3Jan2020.)

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

Theorem  distrsrg 6647 
Multiplication of signed reals is distributive. (Contributed by Jim
Kingdon, 4Jan2020.)

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

Theorem  m1p1sr 6648 
Minus one plus one is zero for signed reals. (Contributed by NM,
5May1996.)

⊢ (1_{R}
+_{R} 1_{R}) =
0_{R} 

Theorem  m1m1sr 6649 
Minus one times minus one is plus one for signed reals. (Contributed by
NM, 14May1996.)

⊢ (1_{R}
·_{R} 1_{R}) =
1_{R} 

Theorem  lttrsr 6650* 
Signed real 'less than' is a transitive relation. (Contributed by Jim
Kingdon, 4Jan2019.)

⊢ ((f ∈ R ∧ g ∈ R ∧ ℎ
∈ R) → ((f <_{R} g ∧ g <_{R} ℎ) → f <_{R} ℎ)) 

Theorem  ltposr 6651 
Signed real 'less than' is a partial order. (Contributed by Jim
Kingdon, 4Jan2019.)

⊢ <_{R} Po
R 

Theorem  ltsosr 6652 
Signed real 'less than' is a strict ordering. (Contributed by NM,
19Feb1996.)

⊢ <_{R} Or
R 

Theorem  0lt1sr 6653 
0 is less than 1 for signed reals. (Contributed by NM, 26Mar1996.)

⊢ 0_{R}
<_{R} 1_{R} 

Theorem  1ne0sr 6654 
1 and 0 are distinct for signed reals. (Contributed by NM,
26Mar1996.)

⊢ ¬ 1_{R} =
0_{R} 

Theorem  0idsr 6655 
The signed real number 0 is an identity element for addition of signed
reals. (Contributed by NM, 10Apr1996.)

⊢ (A ∈ R → (A +_{R}
0_{R}) = A) 

Theorem  1idsr 6656 
1 is an identity element for multiplication. (Contributed by Jim
Kingdon, 5Jan2020.)

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

Theorem  00sr 6657 
A signed real times 0 is 0. (Contributed by NM, 10Apr1996.)

⊢ (A ∈ R → (A ·_{R}
0_{R}) = 0_{R}) 

Theorem  ltasrg 6658 
Ordering property of addition. (Contributed by NM, 10May1996.)

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

Theorem  pn0sr 6659 
A signed real plus its negative is zero. (Contributed by NM,
14May1996.)

⊢ (A ∈ R → (A +_{R} (A ·_{R}
1_{R})) = 0_{R}) 

Theorem  negexsr 6660* 
Existence of negative signed real. Part of Proposition 94.3 of
[Gleason] p. 126. (Contributed by NM,
2May1996.)

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

Theorem  recexgt0sr 6661* 
The reciprocal of a positive signed real exists and is positive.
(Contributed by Jim Kingdon, 6Feb2020.)

⊢ (0_{R}
<_{R} A →
∃x
∈ R
(0_{R} <_{R} x ∧ (A ·_{R} x) = 1_{R})) 

Theorem  recexsrlem 6662* 
The reciprocal of a positive signed real exists. Part of Proposition
94.3 of [Gleason] p. 126. (Contributed
by NM, 15May1996.)

⊢ (0_{R}
<_{R} A →
∃x
∈ R (A ·_{R} x) = 1_{R}) 

Theorem  addgt0sr 6663 
The sum of two positive signed reals is positive. (Contributed by NM,
14May1996.)

⊢ ((0_{R}
<_{R} A ∧ 0_{R}
<_{R} B) →
0_{R} <_{R} (A +_{R} B)) 

Theorem  mulgt0sr 6664 
The product of two positive signed reals is positive. (Contributed by
NM, 13May1996.)

⊢ ((0_{R}
<_{R} A ∧ 0_{R}
<_{R} B) →
0_{R} <_{R} (A ·_{R} B)) 

Theorem  aptisr 6665 
Apartness of signed reals is tight. (Contributed by Jim Kingdon,
29Jan2020.)

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

Theorem  mulextsr1lem 6666 
Lemma for mulextsr1 6667. (Contributed by Jim Kingdon, 17Feb2020.)

⊢ (((𝑋 ∈
P ∧ 𝑌 ∈
P) ∧ (𝑍 ∈
P ∧ 𝑊 ∈
P) ∧ (𝑈 ∈
P ∧ 𝑉 ∈
P)) → ((((𝑋 ·_{P} 𝑈) +_{P}
(𝑌
·_{P} 𝑉)) +_{P} ((𝑍
·_{P} 𝑉) +_{P} (𝑊
·_{P} 𝑈)))<_{P} (((𝑋
·_{P} 𝑉) +_{P} (𝑌
·_{P} 𝑈)) +_{P} ((𝑍
·_{P} 𝑈) +_{P} (𝑊
·_{P} 𝑉))) → ((𝑋 +_{P} 𝑊)<_{P}
(𝑌
+_{P} 𝑍) ∨ (𝑍 +_{P}
𝑌)<_{P} (𝑊 +_{P}
𝑋)))) 

Theorem  mulextsr1 6667 
Strong extensionality of multiplication of signed reals. (Contributed
by Jim Kingdon, 18Feb2020.)

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

Theorem  archsr 6668* 
For any signed real, there is an integer that is greater than it. This
is also known as the "archimedean property". The expression
[⟨(⟨{𝑙 ∣ 𝑙 <_{Q}
[⟨x, 1_{𝑜}⟩]
~_{Q} },
{u ∣
[⟨x, 1_{𝑜}⟩]
~_{Q} <_{Q} u}⟩ +_{P}
1_{P}), 1_{P}⟩]
~_{R} is the
embedding of the positive integer x into the signed reals.
(Contributed by Jim Kingdon, 23Apr2020.)

⊢ (A ∈ R → ∃x ∈ N A <_{R}
[⟨(⟨{𝑙 ∣
𝑙
<_{Q} [⟨x,
1_{𝑜}⟩] ~_{Q} }, {u ∣ [⟨x, 1_{𝑜}⟩]
~_{Q} <_{Q} u}⟩ +_{P}
1_{P}), 1_{P}⟩]
~_{R} ) 

Syntax  cc 6669 
Class of complex numbers.

class ℂ 

Syntax  cr 6670 
Class of real numbers.

class ℝ 

Syntax  cc0 6671 
Extend class notation to include the complex number 0.

class 0 

Syntax  c1 6672 
Extend class notation to include the complex number 1.

class 1 

Syntax  ci 6673 
Extend class notation to include the complex number i.

class i 

Syntax  caddc 6674 
Addition on complex numbers.

class + 

Syntax  cltrr 6675 
'Less than' predicate (defined over real subset of complex numbers).

class <_{ℝ} 

Syntax  cmul 6676 
Multiplication on complex numbers. The token ·
is a center dot.

class · 

Definition  dfc 6677 
Define the set of complex numbers. (Contributed by NM, 22Feb1996.)

⊢ ℂ = (R ×
R) 

Definition  df0 6678 
Define the complex number 0. (Contributed by NM, 22Feb1996.)

⊢ 0 = ⟨0_{R},
0_{R}⟩ 

Definition  df1 6679 
Define the complex number 1. (Contributed by NM, 22Feb1996.)

⊢ 1 = ⟨1_{R},
0_{R}⟩ 

Definition  dfi 6680 
Define the complex number i (the imaginary unit).
(Contributed by
NM, 22Feb1996.)

⊢ i = ⟨0_{R},
1_{R}⟩ 

Definition  dfr 6681 
Define the set of real numbers. (Contributed by NM, 22Feb1996.)

⊢ ℝ = (R ×
{0_{R}}) 

Definition  dfadd 6682* 
Define addition over complex numbers. (Contributed by NM,
28May1995.)

⊢ + = {⟨⟨x, y⟩,
z⟩ ∣ ((x ∈ ℂ ∧ y ∈ ℂ) ∧
∃w∃v∃u∃f((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨(w +_{R}
u), (v
+_{R} f)⟩))} 

Definition  dfmul 6683* 
Define multiplication over complex numbers. (Contributed by NM,
9Aug1995.)

⊢ · = {⟨⟨x, y⟩,
z⟩ ∣ ((x ∈ ℂ ∧ y ∈ ℂ) ∧
∃w∃v∃u∃f((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨((w
·_{R} u)
+_{R} (1_{R}
·_{R} (v
·_{R} f))),
((v ·_{R}
u) +_{R} (w ·_{R} f))⟩))} 

Definition  dflt 6684* 
Define 'less than' on the real subset of complex numbers. (Contributed
by NM, 22Feb1996.)

⊢ <_{ℝ} = {⟨x, y⟩
∣ ((x ∈ ℝ ∧
y ∈
ℝ) ∧ ∃z∃w((x = ⟨z,
0_{R}⟩ ∧ y = ⟨w,
0_{R}⟩) ∧ z <_{R} w))} 

Theorem  opelcn 6685 
Ordered pair membership in the class of complex numbers. (Contributed by
NM, 14May1996.)

⊢ (⟨A,
B⟩ ∈ ℂ ↔ (A ∈
R ∧ B ∈
R)) 

Theorem  opelreal 6686 
Ordered pair membership in class of real subset of complex numbers.
(Contributed by NM, 22Feb1996.)

⊢ (⟨A,
0_{R}⟩ ∈ ℝ
↔ A ∈ R) 

Theorem  elreal 6687* 
Membership in class of real numbers. (Contributed by NM,
31Mar1996.)

⊢ (A ∈ ℝ ↔ ∃x ∈ R ⟨x, 0_{R}⟩ = A) 

Theorem  elreal2 6688 
Ordered pair membership in the class of complex numbers. (Contributed
by Mario Carneiro, 15Jun2013.)

⊢ (A ∈ ℝ ↔ ((1^{st} ‘A) ∈
R ∧ A = ⟨(1^{st} ‘A),
0_{R}⟩)) 

Theorem  0ncn 6689 
The empty set is not a complex number. Note: do not use this after the
real number axioms are developed, since it is a constructiondependent
property. (Contributed by NM, 2May1996.)

⊢ ¬ ∅ ∈ ℂ 

Theorem  ltrelre 6690 
'Less than' is a relation on real numbers. (Contributed by NM,
22Feb1996.)

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

Theorem  addcnsr 6691 
Addition of complex numbers in terms of signed reals. (Contributed by
NM, 28May1995.)

⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈
R ∧ 𝐷 ∈
R)) → (⟨A,
B⟩ + ⟨𝐶, 𝐷⟩) = ⟨(A +_{R} 𝐶), (B
+_{R} 𝐷)⟩) 

Theorem  mulcnsr 6692 
Multiplication of complex numbers in terms of signed reals.
(Contributed by NM, 9Aug1995.)

⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈
R ∧ 𝐷 ∈
R)) → (⟨A,
B⟩ · ⟨𝐶, 𝐷⟩) = ⟨((A ·_{R} 𝐶) +_{R}
(1_{R} ·_{R} (B ·_{R} 𝐷))), ((B ·_{R} 𝐶) +_{R}
(A ·_{R}
𝐷))⟩) 

Theorem  eqresr 6693 
Equality of real numbers in terms of intermediate signed reals.
(Contributed by NM, 10May1996.)

⊢ A ∈ V ⇒ ⊢ (⟨A, 0_{R}⟩ =
⟨B, 0_{R}⟩
↔ A = B) 

Theorem  addresr 6694 
Addition of real numbers in terms of intermediate signed reals.
(Contributed by NM, 10May1996.)

⊢ ((A ∈ R ∧ B ∈ R) → (⟨A, 0_{R}⟩ +
⟨B,
0_{R}⟩) = ⟨(A +_{R} B),
0_{R}⟩) 

Theorem  mulresr 6695 
Multiplication of real numbers in terms of intermediate signed reals.
(Contributed by NM, 10May1996.)

⊢ ((A ∈ R ∧ B ∈ R) → (⟨A, 0_{R}⟩ ·
⟨B,
0_{R}⟩) = ⟨(A ·_{R} B),
0_{R}⟩) 

Theorem  ltresr 6696 
Ordering of real subset of complex numbers in terms of signed reals.
(Contributed by NM, 22Feb1996.)

⊢ (⟨A,
0_{R}⟩ <_{ℝ} ⟨B, 0_{R}⟩ ↔
A <_{R} B) 

Theorem  ltresr2 6697 
Ordering of real subset of complex numbers in terms of signed reals.
(Contributed by NM, 22Feb1996.)

⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A <_{ℝ}
B ↔ (1^{st} ‘A) <_{R} (1^{st}
‘B))) 

Theorem  dfcnqs 6698 
Technical trick to permit reuse of previous lemmas to prove arithmetic
operation laws in ℂ from those in R. The trick involves
qsid 6107, which shows that the coset of the converse
epsilon relation
(which is not an equivalence relation) acts as an identity divisor for the
quotient set operation. This lets us "pretend" that ℂ is a quotient
set, even though it is not (compare dfc 6677), and allows us to reuse some
of the equivalence class lemmas we developed for the transition from
positive reals to signed reals, etc. (Contributed by NM, 13Aug1995.)

⊢ ℂ = ((R ×
R) / ^{◡} E
) 

Theorem  addcnsrec 6699 
Technical trick to permit reuse of some equivalence class lemmas for
operation laws. See dfcnqs 6698 and mulcnsrec 6700. (Contributed by NM,
13Aug1995.)

⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈
R ∧ 𝐷 ∈
R)) → ([⟨A,
B⟩]^{◡} E + [⟨𝐶, 𝐷⟩]^{◡} E ) = [⟨(A +_{R} 𝐶), (B
+_{R} 𝐷)⟩]^{◡} E ) 

Theorem  mulcnsrec 6700 
Technical trick to permit reuse of some equivalence class lemmas for
operation laws. The trick involves ecidg 6106, which shows that the coset
of the converse epsilon relation (which is not an equivalence relation)
leaves a set unchanged. See also dfcnqs 6698. (Contributed by NM,
13Aug1995.)

⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈
R ∧ 𝐷 ∈
R)) → ([⟨A,
B⟩]^{◡} E · [⟨𝐶, 𝐷⟩]^{◡} E ) = [⟨((A ·_{R} 𝐶) +_{R}
(1_{R} ·_{R} (B ·_{R} 𝐷))), ((B ·_{R} 𝐶) +_{R}
(A ·_{R}
𝐷))⟩]^{◡} E ) 