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 6486
to both A
and B, and uses nqtri3or 6380 rather than prloc 6474 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  nqprl 6533* 
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 6534* 
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 6535 
The positive real number 'one'. (Contributed by NM, 13Mar1996.)
(Revised by Mario Carneiro, 12Jun2013.)

⊢ 1_{P} ∈ P 

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

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

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

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

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

⊢ <_{P} Po
P 

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

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

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

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

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