Type  Label  Description 
Statement 

Theorem  genpmu 6501* 
The upper cut produced by addition or multiplication on positive reals
is inhabited. (Contributed by Jim Kingdon, 5Dec2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → ∃𝑞 ∈
Q 𝑞 ∈ (2^{nd} ‘(A𝐹B))) 

Theorem  genpcdl 6502* 
Downward closure of an operation on positive reals. (Contributed by
Jim Kingdon, 14Oct2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ ((((A ∈ P ∧ g ∈ (1^{st} ‘A)) ∧ (B ∈
P ∧ ℎ ∈
(1^{st} ‘B))) ∧ x ∈ Q) → (x <_{Q} (g𝐺ℎ) → x ∈
(1^{st} ‘(A𝐹B)))) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → (f ∈ (1^{st} ‘(A𝐹B))
→ (x <_{Q}
f → x ∈
(1^{st} ‘(A𝐹B))))) 

Theorem  genpcuu 6503* 
Upward closure of an operation on positive reals. (Contributed by Jim
Kingdon, 8Nov2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ ((((A ∈ P ∧ g ∈ (2^{nd} ‘A)) ∧ (B ∈
P ∧ ℎ ∈
(2^{nd} ‘B))) ∧ x ∈ Q) → ((g𝐺ℎ) <_{Q} x → x
∈ (2^{nd} ‘(A𝐹B)))) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → (f ∈ (2^{nd} ‘(A𝐹B))
→ (f <_{Q}
x → x ∈
(2^{nd} ‘(A𝐹B))))) 

Theorem  genprndl 6504* 
The lower cut produced by addition or multiplication on positive reals
is rounded. (Contributed by Jim Kingdon, 7Oct2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ ((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (x <_{Q} y ↔ (z𝐺x)
<_{Q} (z𝐺y)))
& ⊢ ((x ∈ Q ∧ y ∈ Q) → (x𝐺y) =
(y𝐺x))
& ⊢ ((((A ∈ P ∧ g ∈ (1^{st} ‘A)) ∧ (B ∈
P ∧ ℎ ∈
(1^{st} ‘B))) ∧ x ∈ Q) → (x <_{Q} (g𝐺ℎ) → x ∈
(1^{st} ‘(A𝐹B)))) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → ∀𝑞 ∈
Q (𝑞 ∈ (1^{st} ‘(A𝐹B))
↔ ∃𝑟 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘(A𝐹B))))) 

Theorem  genprndu 6505* 
The upper cut produced by addition or multiplication on positive reals
is rounded. (Contributed by Jim Kingdon, 7Oct2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ ((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (x <_{Q} y ↔ (z𝐺x)
<_{Q} (z𝐺y)))
& ⊢ ((x ∈ Q ∧ y ∈ Q) → (x𝐺y) =
(y𝐺x))
& ⊢ ((((A ∈ P ∧ g ∈ (2^{nd} ‘A)) ∧ (B ∈
P ∧ ℎ ∈
(2^{nd} ‘B))) ∧ x ∈ Q) → ((g𝐺ℎ) <_{Q} x → x
∈ (2^{nd} ‘(A𝐹B)))) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → ∀𝑟 ∈
Q (𝑟 ∈ (2^{nd} ‘(A𝐹B))
↔ ∃𝑞 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘(A𝐹B))))) 

Theorem  genpdisj 6506* 
The lower and upper cuts produced by addition or multiplication on
positive reals are disjoint. (Contributed by Jim Kingdon,
15Oct2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ ((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (x <_{Q} y ↔ (z𝐺x)
<_{Q} (z𝐺y)))
& ⊢ ((x ∈ Q ∧ y ∈ Q) → (x𝐺y) =
(y𝐺x)) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → ∀𝑞 ∈
Q ¬ (𝑞
∈ (1^{st} ‘(A𝐹B))
∧ 𝑞 ∈
(2^{nd} ‘(A𝐹B)))) 

Theorem  genpassl 6507* 
Associativity of lower cuts. Lemma for genpassg 6509. (Contributed by
Jim Kingdon, 11Dec2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((f ∈ P ∧ g ∈ P) → (f𝐹g)
∈ P) & ⊢ ((f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ))) ⇒ ⊢ ((A ∈
P ∧ B ∈
P ∧ 𝐶 ∈
P) → (1^{st} ‘((A𝐹B)𝐹𝐶)) = (1^{st} ‘(A𝐹(B𝐹𝐶)))) 

Theorem  genpassu 6508* 
Associativity of upper cuts. Lemma for genpassg 6509. (Contributed by
Jim Kingdon, 11Dec2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((f ∈ P ∧ g ∈ P) → (f𝐹g)
∈ P) & ⊢ ((f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ))) ⇒ ⊢ ((A ∈
P ∧ B ∈
P ∧ 𝐶 ∈
P) → (2^{nd} ‘((A𝐹B)𝐹𝐶)) = (2^{nd} ‘(A𝐹(B𝐹𝐶)))) 

Theorem  genpassg 6509* 
Associativity of an operation on reals. (Contributed by Jim Kingdon,
11Dec2019.)

⊢ 𝐹 = (w
∈ P, v ∈
P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1^{st} ‘w) ∧ z ∈ (1^{st} ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(2^{nd} ‘w) ∧ z ∈ (2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) & ⊢ ((y ∈
Q ∧ z ∈
Q) → (y𝐺z) ∈
Q)
& ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((f ∈ P ∧ g ∈ P) → (f𝐹g)
∈ P) & ⊢ ((f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ))) ⇒ ⊢ ((A ∈
P ∧ B ∈
P ∧ 𝐶 ∈
P) → ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶))) 

Theorem  addnqprllem 6510 
Lemma to prove downward closure in positive real addition. (Contributed
by Jim Kingdon, 7Dec2019.)

⊢ (((⟨𝐿, 𝑈⟩ ∈
P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) → (𝑋
<_{Q} 𝑆 → ((𝑋 ·_{Q}
(*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝐿)) 

Theorem  addnqprulem 6511 
Lemma to prove upward closure in positive real addition. (Contributed
by Jim Kingdon, 7Dec2019.)

⊢ (((⟨𝐿, 𝑈⟩ ∈
P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈
Q) → (𝑆
<_{Q} 𝑋 → ((𝑋 ·_{Q}
(*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝑈)) 

Theorem  addnqprl 6512 
Lemma to prove downward closure in positive real addition. (Contributed
by Jim Kingdon, 5Dec2019.)

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

Theorem  addnqpru 6513 
Lemma to prove upward closure in positive real addition. (Contributed
by Jim Kingdon, 5Dec2019.)

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

Theorem  addlocprlemlt 6514 
Lemma for addlocpr 6519. The 𝑄 <_{Q} (𝐷 +_{Q}
𝐸) case.
(Contributed by
Jim Kingdon, 6Dec2019.)

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

Theorem  addlocprlemeqgt 6515 
Lemma for addlocpr 6519. This is a step used in both the
𝑄 =
(𝐷
+_{Q} 𝐸) and (𝐷 +_{Q}
𝐸)
<_{Q} 𝑄 cases. (Contributed by Jim
Kingdon, 7Dec2019.)

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

Theorem  addlocprlemeq 6516 
Lemma for addlocpr 6519. The 𝑄 = (𝐷 +_{Q} 𝐸) case. (Contributed by
Jim Kingdon, 6Dec2019.)

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

Theorem  addlocprlemgt 6517 
Lemma for addlocpr 6519. The (𝐷 +_{Q} 𝐸) <_{Q}
𝑄 case.
(Contributed by
Jim Kingdon, 6Dec2019.)

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

Theorem  addlocprlem 6518 
Lemma for addlocpr 6519. The result, in deduction form.
(Contributed by
Jim Kingdon, 6Dec2019.)

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

Theorem  addlocpr 6519* 
Locatedness of addition on positive reals. Lemma 11.16 in
[BauerTaylor], p. 53. The proof in
BauerTaylor relies on signed
rationals, so we replace it with another proof which applies prarloc 6485
to both A
and B, and uses nqtri3or 6380 rather than prloc 6473 to
decide whether 𝑞 is too big to be in the lower cut of
A
+_{P} B
(and deduce that if it is, then 𝑟 must be in the upper cut). What
the two proofs have in common is that they take the difference between
𝑞 and 𝑟 to determine how tight a range they
need around the real
numbers. (Contributed by Jim Kingdon, 5Dec2019.)

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

Theorem  addclpr 6520 
Closure of addition on positive reals. First statement of Proposition
93.5 of [Gleason] p. 123. Combination
of Lemma 11.13 and Lemma 11.16
in [BauerTaylor], p. 53.
(Contributed by NM, 13Mar1996.)

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

Theorem  plpvlu 6521* 
Value of addition on positive reals. (Contributed by Jim Kingdon,
8Dec2019.)

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

Theorem  mpvlu 6522* 
Value of multiplication on positive reals. (Contributed by Jim Kingdon,
8Dec2019.)

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

Theorem  dmplp 6523 
Domain of addition on positive reals. (Contributed by NM,
18Nov1995.)

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

Theorem  dmmp 6524 
Domain of multiplication on positive reals. (Contributed by NM,
18Nov1995.)

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

Theorem  nqprm 6525* 
A cut produced from a rational is inhabited. Lemma for nqprlu 6530.
(Contributed by Jim Kingdon, 8Dec2019.)

⊢ (A ∈ Q → (∃𝑞 ∈
Q 𝑞 ∈ {x ∣
x <_{Q} A} ∧ ∃𝑟 ∈
Q 𝑟 ∈ {x ∣
A <_{Q} x})) 

Theorem  nqprrnd 6526* 
A cut produced from a rational is rounded. Lemma for nqprlu 6530.
(Contributed by Jim Kingdon, 8Dec2019.)

⊢ (A ∈ Q → (∀𝑞 ∈
Q (𝑞 ∈ {x ∣
x <_{Q} A} ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈
{x ∣ x <_{Q} A})) ∧ ∀𝑟 ∈
Q (𝑟 ∈ {x ∣
A <_{Q} x} ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈
{x ∣ A <_{Q} x})))) 

Theorem  nqprdisj 6527* 
A cut produced from a rational is disjoint. Lemma for nqprlu 6530.
(Contributed by Jim Kingdon, 8Dec2019.)

⊢ (A ∈ Q → ∀𝑞 ∈
Q ¬ (𝑞
∈ {x
∣ x <_{Q}
A} ∧
𝑞 ∈ {x ∣
A <_{Q} x})) 

Theorem  nqprloc 6528* 
A cut produced from a rational is located. Lemma for nqprlu 6530.
(Contributed by Jim Kingdon, 8Dec2019.)

⊢ (A ∈ Q → ∀𝑞 ∈
Q ∀𝑟 ∈
Q (𝑞
<_{Q} 𝑟 → (𝑞 ∈
{x ∣ x <_{Q} A} ∨ 𝑟 ∈ {x ∣
A <_{Q} x}))) 

Theorem  nqprxx 6529* 
The canonical embedding of the rationals into the reals, expressed with
the same variable for the lower and upper cuts. (Contributed by Jim
Kingdon, 8Dec2019.)

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

Theorem  nqprlu 6530* 
The canonical embedding of the rationals into the reals. (Contributed
by Jim Kingdon, 24Jun2020.)

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

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

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

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

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

Theorem  nnprlu 6533* 
The canonical embedding of positive integers into the positive reals.
(Contributed by Jim Kingdon, 23Apr2020.)

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

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

⊢ 1_{P} ∈ P 

Theorem  1prl 6535 
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 6536 
The upper cut of the positive real number 'one'. (Contributed by Jim
Kingdon, 28Dec2019.)

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

Theorem  addnqpr1lemrl 6537* 
Lemma for addnqpr1 6541. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 28Apr2020.)

⊢ (A ∈ Q → (1^{st}
‘(⟨{𝑙 ∣
𝑙
<_{Q} A},
{u ∣ A <_{Q} u}⟩ +_{P}
1_{P})) ⊆ (1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (A +_{Q}
1_{Q})}, {u ∣
(A +_{Q}
1_{Q}) <_{Q} u}⟩)) 

Theorem  addnqpr1lemru 6538* 
Lemma for addnqpr1 6541. The reverse subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 28Apr2020.)

⊢ (A ∈ Q → (2^{nd}
‘(⟨{𝑙 ∣
𝑙
<_{Q} A},
{u ∣ A <_{Q} u}⟩ +_{P}
1_{P})) ⊆ (2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (A +_{Q}
1_{Q})}, {u ∣
(A +_{Q}
1_{Q}) <_{Q} u}⟩)) 

Theorem  addnqpr1lemil 6539* 
Lemma for addnqpr1 6541. The forward subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 28Apr2020.)

⊢ (A ∈ Q → (1^{st}
‘⟨{𝑙 ∣ 𝑙 <_{Q}
(A +_{Q}
1_{Q})}, {u ∣
(A +_{Q}
1_{Q}) <_{Q} u}⟩) ⊆ (1^{st}
‘(⟨{𝑙 ∣
𝑙
<_{Q} A},
{u ∣ A <_{Q} u}⟩ +_{P}
1_{P}))) 

Theorem  addnqpr1lemiu 6540* 
Lemma for addnqpr1 6541. The forward subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 28Apr2020.)

⊢ (A ∈ Q → (2^{nd}
‘⟨{𝑙 ∣ 𝑙 <_{Q}
(A +_{Q}
1_{Q})}, {u ∣
(A +_{Q}
1_{Q}) <_{Q} u}⟩) ⊆ (2^{nd}
‘(⟨{𝑙 ∣
𝑙
<_{Q} A},
{u ∣ A <_{Q} u}⟩ +_{P}
1_{P}))) 

Theorem  addnqpr1 6541* 
Addition of one to a fraction embedded into a positive real. One can
either add the fraction one to the fraction, or the positive real one to
the positive real, and get the same result. (Contributed by Jim
Kingdon, 26Apr2020.)

⊢ (A ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} (A +_{Q}
1_{Q})}, {u ∣
(A +_{Q}
1_{Q}) <_{Q} u}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} A}, {u ∣
A <_{Q} u}⟩ +_{P}
1_{P})) 

Theorem  appdivnq 6542* 
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 6543* 
Approximate division for positive rationals. This can be thought of as
a variation of appdivnq 6542 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 6544 
Calculations for prmuloc 6545. (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 6545* 
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 6546* 
Positive reals are multiplicatively located. This is a variation of
prmuloc 6545 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 6547 
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 6548 
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 6549 
Calculations for mullocpr 6550. (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 6550* 
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 6551 
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 6552 
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 6553 
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 6554 
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 6555 
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 6556 
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 6557 
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 6558* 
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 6559* 
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 6560 
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 6561 
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 6562 
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 6563 
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 6564 
Lemma for 1idpr 6566. (Contributed by Jim Kingdon, 13Dec2019.)

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

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

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

Theorem  1idpr 6566 
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 6567 
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 6568. (Contributed by Jim Kingdon,
15Dec2019.)

⊢ <_{P} Po
P 

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

⊢ <_{P} Or
P 

Theorem  ltaddpr 6569 
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 6570* 
Element in lower cut of the constructed difference. Lemma for
ltexpri 6585. (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 6571* 
Element in upper cut of the constructed difference. Lemma for
ltexpri 6585. (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 6572* 
Our constructed difference is inhabited. Lemma for ltexpri 6585.
(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 6573* 
The lower cut of our constructed difference is open. Lemma for
ltexpri 6585. (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 6574* 
The lower cut of our constructed difference is lower. Lemma for
ltexpri 6585. (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 6575* 
The upper cut of our constructed difference is open. Lemma for
ltexpri 6585. (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 6576* 
The upper cut of our constructed difference is upper. Lemma for
ltexpri 6585. (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 6577* 
Our constructed difference is rounded. Lemma for ltexpri 6585.
(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 6578* 
Our constructed difference is disjoint. Lemma for ltexpri 6585.
(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 6579* 
Our constructed difference is located. Lemma for ltexpri 6585.
(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 6580* 
Our constructed difference is a positive real. Lemma for ltexpri 6585.
(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 6581* 
Lemma for ltexpri 6585. 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 6582* 
Lemma for ltexpri 6585. 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 6583* 
Lemma for ltexpri 6585. 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 6584* 
Lemma for ltexpri 6585. 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 6585* 
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 6586 
Lemma for addcanprg 6588. (Contributed by Jim Kingdon, 25Dec2019.)

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

Theorem  addcanprlemu 6587 
Lemma for addcanprg 6588. (Contributed by Jim Kingdon, 25Dec2019.)

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

Theorem  addcanprg 6588 
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 6589 
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 6590 
Ordering property of addition. Proposition 93.5(v) of [Gleason]
p. 123. (Contributed by Jim Kingdon, 26Dec2019.)

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

Theorem  addextpr 6591 
Strong extensionality of addition (ordering version). This is similar
to addext 7354 but for positive reals and based on lessthan
rather than
apartness. (Contributed by Jim Kingdon, 17Feb2020.)

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

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

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

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

Theorem  recexprlemopl 6595* 
The lower cut of B
is open. Lemma for recexpr 6608. (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 6596* 
The lower cut of B
is lower. Lemma for recexpr 6608. (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 6597* 
The upper cut of B
is open. Lemma for recexpr 6608. (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 6598* 
The upper cut of B
is upper. Lemma for recexpr 6608. (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 6599* 
B is rounded.
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 (𝑞 ∈ (1^{st} ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈
(1^{st} ‘B))) ∧ ∀𝑟 ∈ Q (𝑟 ∈
(2^{nd} ‘B) ↔ ∃𝑞 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘B))))) 

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