Type  Label  Description 
Statement 

Theorem  genpcdl 6501* 
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 6502* 
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 6503* 
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 6504* 
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 6505* 
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 6506* 
Associativity of lower cuts. Lemma for genpassg 6508. (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 6507* 
Associativity of upper cuts. Lemma for genpassg 6508. (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 6508* 
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 6509 
Lemma to prove downward closure in positive real addition. (Contributed
by Jim Kingdon, 7Dec2019.)

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

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

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

Theorem  addnqprl 6511 
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 6512 
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 6513 
Lemma for addlocpr 6518. 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 6514 
Lemma for addlocpr 6518. 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 6515 
Lemma for addlocpr 6518. 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 6516 
Lemma for addlocpr 6518. 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 6517 
Lemma for addlocpr 6518. 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 6518* 
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 6519 
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 6520* 
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 6521* 
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 6522 
Domain of addition on positive reals. (Contributed by NM,
18Nov1995.)

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

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

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

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

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

Theorem  nqprrnd 6525* 
A cut produced from a rational is rounded. Lemma for nqprlu 6529.
(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 6526* 
A cut produced from a rational is disjoint. Lemma for nqprlu 6529.
(Contributed by Jim Kingdon, 8Dec2019.)

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

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

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

Theorem  nqprxx 6528* 
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 6529* 
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 6530 
The class of rationals less than a given rational is a set.
(Contributed by Jim Kingdon, 13Dec2019.)

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

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

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

Theorem  nqprl 6532* 
Comparing a fraction to a real can be done by whether it is an element
of the lower cut, or by <_{P}. (Contributed by Jim Kingdon,
8Jul2020.)

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

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  addnqprlemrl 6537* 
Lemma for addnqpr 6541. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 19Aug2020.)

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

Theorem  addnqprlemru 6538* 
Lemma for addnqpr 6541. The reverse subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 19Aug2020.)

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

Theorem  addnqprlemfl 6539* 
Lemma for addnqpr 6541. The forward subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 19Aug2020.)

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

Theorem  addnqprlemfu 6540* 
Lemma for addnqpr 6541. The forward subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 19Aug2020.)

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

Theorem  addnqpr 6541* 
Addition of fractions embedded into positive reals. One can either add
the fractions as fractions, or embed them into positive reals and add
them as positive reals, and get the same result. (Contributed by Jim
Kingdon, 19Aug2020.)

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

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

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

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

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

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

⊢ <_{P} Po
P 

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

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

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

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

Theorem  addcanprg 6589 
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 6590 
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 6591 
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 6592 
Strong extensionality of addition (ordering version). This is similar
to addext 7374 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 6593* 
Membership in the lower cut of B. Lemma for recexpr 6609.
(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 6594* 
Membership in the upper cut of B. Lemma for recexpr 6609.
(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 6595* 
B is inhabited.
Lemma for recexpr 6609. (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 6596* 
The lower cut of B
is open. Lemma for recexpr 6609. (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 6597* 
The lower cut of B
is lower. Lemma for recexpr 6609. (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 6598* 
The upper cut of B
is open. Lemma for recexpr 6609. (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 6599* 
The upper cut of B
is upper. Lemma for recexpr 6609. (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 6600* 
B is rounded.
Lemma for recexpr 6609. (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))))) 