Type  Label  Description 
Statement 

Theorem  nqprlu 6401* 
The canonical embedding of the rationals into the reals. (Contributed
by Jim Kingdon, 8Dec2019.)

⊢ (A ∈ Q → ⟨{x ∣ x
<_{Q} A},
{x ∣ A <_{Q} x}⟩ ∈
P) 

Theorem  ltnqex 6402 
The class of rationals less than a given rational is a set.
(Contributed by Jim Kingdon, 13Dec2019.)

⊢ {x ∣
x <_{Q} A} ∈
V 

Theorem  gtnqex 6403 
The class of rationals greater than a given rational is a set.
(Contributed by Jim Kingdon, 13Dec2019.)

⊢ {x ∣
A <_{Q} x} ∈
V 

Theorem  1pr 6404 
The positive real number 'one'. (Contributed by NM, 13Mar1996.)
(Revised by Mario Carneiro, 12Jun2013.)

⊢ 1_{P} ∈ P 

Theorem  1prl 6405 
The lower cut of the positive real number 'one'. (Contributed by Jim
Kingdon, 28Dec2019.)

⊢ (1^{st}
‘1_{P}) = {x
∣ x <_{Q}
1_{Q}} 

Theorem  1pru 6406 
The upper cut of the positive real number 'one'. (Contributed by Jim
Kingdon, 28Dec2019.)

⊢ (2^{nd}
‘1_{P}) = {x
∣ 1_{Q} <_{Q} x} 

Theorem  appdivnq 6407* 
Approximate division for positive rationals. Proposition 12.7 of
[BauerTaylor], p. 55 (a special case
where A and B are positive,
as well as 𝐶). Our proof is simpler than the one
in BauerTaylor
because we have reciprocals. (Contributed by Jim Kingdon,
8Dec2019.)

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

Theorem  appdiv0nq 6408* 
Approximate division for positive rationals. This can be thought of as
a variation of appdivnq 6407 in which A is zero, although it can be
stated and proved in terms of positive rationals alone, without zero as
such. (Contributed by Jim Kingdon, 9Dec2019.)

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

Theorem  prmuloclemcalc 6409 
Calculations for prmuloc 6410. (Contributed by Jim Kingdon,
9Dec2019.)

⊢ (φ
→ 𝑅
<_{Q} 𝑈)
& ⊢ (φ
→ 𝑈
<_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (φ → (A +_{Q} 𝑋) = B)
& ⊢ (φ
→ (𝑃
·_{Q} B)
<_{Q} (𝑅 ·_{Q} 𝑋)) & ⊢ (φ → A ∈
Q)
& ⊢ (φ
→ B ∈ Q) & ⊢ (φ → 𝐷 ∈
Q)
& ⊢ (φ
→ 𝑃 ∈ Q) & ⊢ (φ → 𝑋 ∈
Q) ⇒ ⊢ (φ → (𝑈 ·_{Q}
A) <_{Q} (𝐷
·_{Q} B)) 

Theorem  prmuloc 6410* 
Positive reals are multiplicatively located. Lemma 12.8 of
[BauerTaylor], p. 56. (Contributed
by Jim Kingdon, 8Dec2019.)

⊢ ((⟨𝐿, 𝑈⟩ ∈
P ∧ A <_{Q} B) → ∃𝑑 ∈ Q ∃u ∈ Q (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·_{Q}
A) <_{Q} (𝑑
·_{Q} B))) 

Theorem  prmuloc2 6411* 
Positive reals are multiplicatively located. This is a variation of
prmuloc 6410 which only constructs one (named) point and
is therefore often
easier to work with. It states that given a ratio B, there are
elements of the lower and upper cut which have exactly that ratio
between them. (Contributed by Jim Kingdon, 28Dec2019.)

⊢ ((⟨𝐿, 𝑈⟩ ∈
P ∧ 1_{Q}
<_{Q} B) →
∃x
∈ 𝐿 (x
·_{Q} B)
∈ 𝑈) 

Theorem  mulnqprl 6412 
Lemma to prove downward closure in positive real multiplication.
(Contributed by Jim Kingdon, 10Dec2019.)

⊢ ((((A ∈ P ∧ 𝐺 ∈
(1^{st} ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(1^{st} ‘B))) ∧ 𝑋 ∈
Q) → (𝑋
<_{Q} (𝐺 ·_{Q} 𝐻) → 𝑋 ∈
(1^{st} ‘(A
·_{P} B)))) 

Theorem  mulnqpru 6413 
Lemma to prove upward closure in positive real multiplication.
(Contributed by Jim Kingdon, 10Dec2019.)

⊢ ((((A ∈ P ∧ 𝐺 ∈
(2^{nd} ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2^{nd} ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺 ·_{Q} 𝐻)
<_{Q} 𝑋 → 𝑋 ∈
(2^{nd} ‘(A
·_{P} B)))) 

Theorem  mullocprlem 6414 
Calculations for mullocpr 6415. (Contributed by Jim Kingdon,
10Dec2019.)

⊢ (φ
→ (A ∈ P ∧ B ∈ P)) & ⊢ (φ → (𝑈 ·_{Q} 𝑄)
<_{Q} (𝐸 ·_{Q} (𝐷
·_{Q} 𝑈))) & ⊢ (φ → (𝐸 ·_{Q} (𝐷
·_{Q} 𝑈)) <_{Q} (𝑇
·_{Q} (𝐷 ·_{Q} 𝑈))) & ⊢ (φ → (𝑇 ·_{Q} (𝐷
·_{Q} 𝑈)) <_{Q} (𝐷
·_{Q} 𝑅)) & ⊢ (φ → (𝑄 ∈
Q ∧ 𝑅 ∈
Q))
& ⊢ (φ
→ (𝐷 ∈ Q ∧ 𝑈 ∈
Q))
& ⊢ (φ
→ (𝐷 ∈ (1^{st} ‘A) ∧ 𝑈 ∈ (2^{nd} ‘A)))
& ⊢ (φ
→ (𝐸 ∈ Q ∧ 𝑇 ∈
Q)) ⇒ ⊢ (φ → (𝑄 ∈
(1^{st} ‘(A
·_{P} B))
∨ 𝑅 ∈
(2^{nd} ‘(A
·_{P} B)))) 

Theorem  mullocpr 6415* 
Locatedness of multiplication on positive reals. Lemma 12.9 in
[BauerTaylor], p. 56 (but where both
A and B are positive, not
just A).
(Contributed by Jim Kingdon, 8Dec2019.)

⊢ ((A ∈ P ∧ B ∈ P) → ∀𝑞 ∈
Q ∀𝑟 ∈
Q (𝑞
<_{Q} 𝑟 → (𝑞 ∈
(1^{st} ‘(A
·_{P} B))
∨ 𝑟 ∈
(2^{nd} ‘(A
·_{P} B))))) 

Theorem  mulclpr 6416 
Closure of multiplication on positive reals. First statement of
Proposition 93.7 of [Gleason] p. 124.
(Contributed by NM,
13Mar1996.)

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

Theorem  addcomprg 6417 
Addition of positive reals is commutative. Proposition 93.5(ii) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 11Dec2019.)

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

Theorem  addassprg 6418 
Addition of positive reals is associative. Proposition 93.5(i) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 11Dec2019.)

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

Theorem  mulcomprg 6419 
Multiplication of positive reals is commutative. Proposition 93.7(ii)
of [Gleason] p. 124. (Contributed by
Jim Kingdon, 11Dec2019.)

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

Theorem  mulassprg 6420 
Multiplication of positive reals is associative. Proposition 93.7(i)
of [Gleason] p. 124. (Contributed by
Jim Kingdon, 11Dec2019.)

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

Theorem  distrlem1prl 6421 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))) ⊆ (1^{st}
‘((A
·_{P} B)
+_{P} (A
·_{P} 𝐶)))) 

Theorem  distrlem1pru 6422 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (2^{nd} ‘(A ·_{P} (B +_{P} 𝐶))) ⊆ (2^{nd}
‘((A
·_{P} B)
+_{P} (A
·_{P} 𝐶)))) 

Theorem  distrlem4prl 6423* 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((x ·_{Q} y) +_{Q} (f ·_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) 

Theorem  distrlem4pru 6424* 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(2^{nd} ‘A) ∧ y ∈ (2^{nd} ‘B)) ∧ (f ∈
(2^{nd} ‘A) ∧ z ∈ (2^{nd} ‘𝐶)))) → ((x ·_{Q} y) +_{Q} (f ·_{Q} z)) ∈
(2^{nd} ‘(A
·_{P} (B
+_{P} 𝐶)))) 

Theorem  distrlem5prl 6425 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (1^{st} ‘((A ·_{P} B) +_{P} (A ·_{P} 𝐶))) ⊆ (1^{st}
‘(A
·_{P} (B
+_{P} 𝐶)))) 

Theorem  distrlem5pru 6426 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)

⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (2^{nd} ‘((A ·_{P} B) +_{P} (A ·_{P} 𝐶))) ⊆ (2^{nd}
‘(A
·_{P} (B
+_{P} 𝐶)))) 

Theorem  distrprg 6427 
Multiplication of positive reals is distributive. Proposition
93.7(iii) of [Gleason] p. 124.
(Contributed by Jim Kingdon,
12Dec2019.)

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

Theorem  ltprordil 6428 
If a positive real is less than a second positive real, its lower cut is
a subset of the second's lower cut. (Contributed by Jim Kingdon,
23Dec2019.)

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

Theorem  1idprl 6429 
Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13Dec2019.)

⊢ (A ∈ P → (1^{st}
‘(A
·_{P} 1_{P})) =
(1^{st} ‘A)) 

Theorem  1idpru 6430 
Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13Dec2019.)

⊢ (A ∈ P → (2^{nd}
‘(A
·_{P} 1_{P})) =
(2^{nd} ‘A)) 

Theorem  1idpr 6431 
1 is an identity element for positive real multiplication. Theorem
93.7(iv) of [Gleason] p. 124.
(Contributed by NM, 2Apr1996.)

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

Theorem  ltpopr 6432 
Positive real 'less than' is a partial ordering. Remark ("< is
transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p.
(varies). Lemma for ltsopr 6433. (Contributed by Jim Kingdon,
15Dec2019.)

⊢ <_{P} Po
P 

Theorem  ltsopr 6433 
Positive real 'less than' is a weak linear order (in the sense of
dfiso 4008). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed
by Jim Kingdon, 16Dec2019.)

⊢ <_{P} Or
P 

Theorem  ltaddpr 6434 
The sum of two positive reals is greater than one of them. Proposition
93.5(iii) of [Gleason] p. 123.
(Contributed by NM, 26Mar1996.)
(Revised by Mario Carneiro, 12Jun2013.)

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

Theorem  ltexprlemell 6435* 
Element in lower cut of the constructed difference. Lemma for
ltexpri 6450. (Contributed by Jim Kingdon, 21Dec2019.)

⊢ 𝐶 = ⟨{x ∈
Q ∣ ∃y(y ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈
(1^{st} ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈
(2^{nd} ‘B))}⟩ ⇒ ⊢ (𝑞 ∈
(1^{st} ‘𝐶)
↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2^{nd} ‘A) ∧ (y +_{Q} 𝑞) ∈
(1^{st} ‘B)))) 

Theorem  ltexprlemelu 6436* 
Element in upper cut of the constructed difference. Lemma for
ltexpri 6450. (Contributed by Jim Kingdon, 21Dec2019.)

⊢ 𝐶 = ⟨{x ∈
Q ∣ ∃y(y ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈
(1^{st} ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈
(2^{nd} ‘B))}⟩ ⇒ ⊢ (𝑟 ∈
(2^{nd} ‘𝐶)
↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} 𝑟) ∈
(2^{nd} ‘B)))) 

Theorem  ltexprlemm 6437* 
Our constructed difference is inhabited. Lemma for ltexpri 6450.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemopl 6438* 
The lower cut of our constructed difference is open. Lemma for
ltexpri 6450. (Contributed by Jim Kingdon, 21Dec2019.)

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

Theorem  ltexprlemlol 6439* 
The lower cut of our constructed difference is lower. Lemma for
ltexpri 6450. (Contributed by Jim Kingdon, 21Dec2019.)

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

Theorem  ltexprlemopu 6440* 
The upper cut of our constructed difference is open. Lemma for
ltexpri 6450. (Contributed by Jim Kingdon, 21Dec2019.)

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

Theorem  ltexprlemupu 6441* 
The upper cut of our constructed difference is upper. Lemma for
ltexpri 6450. (Contributed by Jim Kingdon, 21Dec2019.)

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

Theorem  ltexprlemrnd 6442* 
Our constructed difference is rounded. Lemma for ltexpri 6450.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemdisj 6443* 
Our constructed difference is disjoint. Lemma for ltexpri 6450.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemloc 6444* 
Our constructed difference is located. Lemma for ltexpri 6450.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlempr 6445* 
Our constructed difference is a positive real. Lemma for ltexpri 6450.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemfl 6446* 
Lemma for ltexpri 6450. One directon of our result for lower cuts.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemrl 6447* 
Lemma for ltexpri 6450. Reverse directon of our result for lower
cuts.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemfu 6448* 
Lemma for ltexpri 6450. One direction of our result for upper cuts.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemru 6449* 
Lemma for ltexpri 6450. One direction of our result for upper cuts.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexpri 6450* 
Proposition 93.5(iv) of [Gleason] p. 123.
(Contributed by NM,
13May1996.) (Revised by Mario Carneiro, 14Jun2013.)

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

Theorem  addcanprleml 6451 
Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25Dec2019.)

⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (A +_{P} B) = (A
+_{P} 𝐶)) → (1^{st} ‘B) ⊆ (1^{st} ‘𝐶)) 

Theorem  addcanprlemu 6452 
Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25Dec2019.)

⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ (A +_{P} B) = (A
+_{P} 𝐶)) → (2^{nd} ‘B) ⊆ (2^{nd} ‘𝐶)) 

Theorem  addcanprg 6453 
Addition cancellation law for positive reals. Proposition 93.5(vi) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 24Dec2019.)

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

Theorem  ltaprlem 6454 
Lemma for Proposition 93.5(v) of [Gleason] p.
123. (Contributed by NM,
8Apr1996.)

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

Theorem  ltaprg 6455 
Ordering property of addition. Proposition 93.5(v) of [Gleason]
p. 123. Part of Definition 11.2.7(vi) of [HoTT]], p. (varies).
(Contributed by Jim Kingdon, 26Dec2019.)

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

Theorem  recexprlemell 6456* 
Membership in the lower cut of B. Lemma for recexpr 6472.
(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))}⟩ ⇒ ⊢ (𝐶 ∈
(1^{st} ‘B) ↔ ∃y(𝐶 <_{Q}
y ∧
(*_{Q}‘y)
∈ (2^{nd} ‘A))) 

Theorem  recexprlemelu 6457* 
Membership in the upper cut of B. Lemma for recexpr 6472.
(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))}⟩ ⇒ ⊢ (𝐶 ∈
(2^{nd} ‘B) ↔ ∃y(y <_{Q} 𝐶 ∧
(*_{Q}‘y)
∈ (1^{st} ‘A))) 

Theorem  recexprlemm 6458* 
B is inhabited.
Lemma for recexpr 6472. (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 𝑞 ∈ (1^{st} ‘B) ∧ ∃𝑟 ∈
Q 𝑟 ∈ (2^{nd} ‘B))) 

Theorem  recexprlemopl 6459* 
The lower cut of B
is open. Lemma for recexpr 6472. (Contributed by
Jim Kingdon, 28Dec2019.)

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

Theorem  recexprlemlol 6460* 
The lower cut of B
is lower. Lemma for recexpr 6472. (Contributed by
Jim Kingdon, 28Dec2019.)

⊢ 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)) → 𝑞 ∈
(1^{st} ‘B))) 

Theorem  recexprlemopu 6461* 
The upper cut of B
is open. Lemma for recexpr 6472. (Contributed by
Jim Kingdon, 28Dec2019.)

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

Theorem  recexprlemupu 6462* 
The upper cut of B
is upper. Lemma for recexpr 6472. (Contributed by
Jim Kingdon, 28Dec2019.)

⊢ 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} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘B)) → 𝑟 ∈
(2^{nd} ‘B))) 

Theorem  recexprlemrnd 6463* 
B is rounded.
Lemma for recexpr 6472. (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 (𝑞 ∈ (1^{st} ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈
(1^{st} ‘B))) ∧ ∀𝑟 ∈ Q (𝑟 ∈
(2^{nd} ‘B) ↔ ∃𝑞 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘B))))) 

Theorem  recexprlemdisj 6464* 
B is disjoint.
Lemma for recexpr 6472. (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 ¬ (𝑞
∈ (1^{st} ‘B) ∧ 𝑞 ∈ (2^{nd} ‘B))) 

Theorem  recexprlemloc 6465* 
B is located.
Lemma for recexpr 6472. (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 6466* 
B is a positive
real. Lemma for recexpr 6472. (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 6467* 
The lower cut of one is a subset of the lower cut of A ·_{P} B.
Lemma for recexpr 6472. (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 6468* 
The upper cut of one is a subset of the upper cut of A ·_{P} B.
Lemma for recexpr 6472. (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 6469* 
The lower cut of A
·_{P} B
is a subset of the lower cut of one. Lemma
for recexpr 6472. (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 6470* 
The upper cut of A
·_{P} B
is a subset of the upper cut of one. Lemma
for recexpr 6472. (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 6471* 
B is the reciprocal
of A. Lemma for recexpr 6472. (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 6472* 
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}) 

Definition  dfenr 6473* 
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 6474 
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 6475* 
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 6476* 
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 6477* 
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 6478 
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 6479 
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 6480 
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 6481 
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 6482 
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 6483 
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 6484 
The equivalence relation for signed reals exists. (Contributed by NM,
25Jul1995.)

⊢ ~_{R} ∈ V 

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

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

Theorem  addcmpblnr 6486 
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 6487 
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 6488 
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 6489* 
Decomposing signed reals into positive reals. Lemma for addsrpr 6492 and
mulsrpr 6493. (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 6490* 
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 6491* 
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 6492 
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 6493 
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 6494 
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 6495 
Greater than zero in terms of positive reals. (Contributed by NM,
13May1996.)

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

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

⊢ ¬ ∅ ∈ R 

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

⊢ 0_{R} ∈ R 

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

⊢ 1_{R} ∈ R 

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

⊢ 1_{R} ∈ R 

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

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