Type  Label  Description 
Statement 

Theorem  ltrelpr 6601 
Positive real 'less than' is a relation on positive reals. (Contributed
by NM, 14Feb1996.)

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

Theorem  ltdfpr 6602* 
More convenient form of dfiltp 6566. (Contributed by Jim Kingdon,
15Dec2019.)

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴<_{P} 𝐵 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2^{nd}
‘𝐴) ∧ 𝑞 ∈ (1^{st}
‘𝐵)))) 

Theorem  genpdflem 6603* 
Simplification of upper or lower cut expression. Lemma for genpdf 6604.
(Contributed by Jim Kingdon, 30Sep2019.)

⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈
Q) ⇒ ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q
∃𝑠 ∈
Q (𝑟 ∈
𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)}) 

Theorem  genpdf 6604* 
Simplified definition of addition or multiplication on positive reals.
(Contributed by Jim Kingdon, 30Sep2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑞 ∈ Q ∣
∃𝑟 ∈
Q ∃𝑠
∈ Q (𝑟
∈ (1^{st} ‘𝑤) ∧ 𝑠 ∈ (1^{st} ‘𝑣) ∧ 𝑞 = (𝑟𝐺𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q
∃𝑠 ∈
Q (𝑟 ∈
(2^{nd} ‘𝑤)
∧ 𝑠 ∈
(2^{nd} ‘𝑣)
∧ 𝑞 = (𝑟𝐺𝑠))}⟩) ⇒ ⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑞 ∈ Q ∣
∃𝑟 ∈
(1^{st} ‘𝑤)∃𝑠 ∈ (1^{st} ‘𝑣)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^{nd}
‘𝑤)∃𝑠 ∈ (2^{nd}
‘𝑣)𝑞 = (𝑟𝐺𝑠)}⟩) 

Theorem  genipv 6605* 
Value of general operation (addition or multiplication) on positive
reals. (Contributed by Jim Kingon, 3Oct2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴𝐹𝐵) = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^{st}
‘𝐴)∃𝑠 ∈ (1^{st}
‘𝐵)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^{nd}
‘𝐴)∃𝑠 ∈ (2^{nd}
‘𝐵)𝑞 = (𝑟𝐺𝑠)}⟩) 

Theorem  genplt2i 6606* 
Operating on both sides of two inequalities, when the operation is
consistent with <_{Q}.
(Contributed by Jim Kingdon, 6Oct2019.)

⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑥
<_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ ((𝐴 <_{Q} 𝐵 ∧ 𝐶 <_{Q} 𝐷) → (𝐴𝐺𝐶) <_{Q} (𝐵𝐺𝐷)) 

Theorem  genpelxp 6607* 
Set containing the result of adding or multiplying positive reals.
(Contributed by Jim Kingdon, 5Dec2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴𝐹𝐵) ∈ (𝒫 Q ×
𝒫 Q)) 

Theorem  genpelvl 6608* 
Membership in lower cut of general operation (addition or
multiplication) on positive reals. (Contributed by Jim Kingdon,
2Oct2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐶 ∈ (1^{st}
‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (1^{st} ‘𝐴)∃ℎ ∈ (1^{st} ‘𝐵)𝐶 = (𝑔𝐺ℎ))) 

Theorem  genpelvu 6609* 
Membership in upper cut of general operation (addition or
multiplication) on positive reals. (Contributed by Jim Kingdon,
15Oct2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐶 ∈ (2^{nd}
‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2^{nd} ‘𝐴)∃ℎ ∈ (2^{nd} ‘𝐵)𝐶 = (𝑔𝐺ℎ))) 

Theorem  genpprecll 6610* 
Preclosure law for general operation on lower cuts. (Contributed by
Jim Kingdon, 2Oct2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
((𝐶 ∈ (1^{st}
‘𝐴) ∧ 𝐷 ∈ (1^{st}
‘𝐵)) → (𝐶𝐺𝐷) ∈ (1^{st} ‘(𝐴𝐹𝐵)))) 

Theorem  genppreclu 6611* 
Preclosure law for general operation on upper cuts. (Contributed by
Jim Kingdon, 7Nov2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
((𝐶 ∈ (2^{nd}
‘𝐴) ∧ 𝐷 ∈ (2^{nd}
‘𝐵)) → (𝐶𝐺𝐷) ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) 

Theorem  genipdm 6612* 
Domain of general operation on positive reals. (Contributed by Jim
Kingdon, 2Oct2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ dom 𝐹 = (P ×
P) 

Theorem  genpml 6613* 
The lower cut produced by addition or multiplication on positive reals
is inhabited. (Contributed by Jim Kingdon, 5Oct2019.)

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∃𝑞 ∈
Q 𝑞 ∈
(1^{st} ‘(𝐴𝐹𝐵))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∃𝑞 ∈
Q 𝑞 ∈
(2^{nd} ‘(𝐴𝐹𝐵))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ (1^{st}
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (1^{st}
‘𝐵))) ∧ 𝑥 ∈ Q) →
(𝑥
<_{Q} (𝑔𝐺ℎ) → 𝑥 ∈ (1^{st} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝑓 ∈ (1^{st}
‘(𝐴𝐹𝐵)) → (𝑥 <_{Q} 𝑓 → 𝑥 ∈ (1^{st} ‘(𝐴𝐹𝐵))))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ (2^{nd}
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (2^{nd}
‘𝐵))) ∧ 𝑥 ∈ Q) →
((𝑔𝐺ℎ) <_{Q} 𝑥 → 𝑥 ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝑓 ∈ (2^{nd}
‘(𝐴𝐹𝐵)) → (𝑓 <_{Q} 𝑥 → 𝑥 ∈ (2^{nd} ‘(𝐴𝐹𝐵))))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1^{st}
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (1^{st}
‘𝐵))) ∧ 𝑥 ∈ Q) →
(𝑥
<_{Q} (𝑔𝐺ℎ) → 𝑥 ∈ (1^{st} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑞 ∈
Q (𝑞 ∈
(1^{st} ‘(𝐴𝐹𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘(𝐴𝐹𝐵))))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2^{nd}
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (2^{nd}
‘𝐵))) ∧ 𝑥 ∈ Q) →
((𝑔𝐺ℎ) <_{Q} 𝑥 → 𝑥 ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑟 ∈
Q (𝑟 ∈
(2^{nd} ‘(𝐴𝐹𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘(𝐴𝐹𝐵))))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑞 ∈
Q ¬ (𝑞
∈ (1^{st} ‘(𝐴𝐹𝐵)) ∧ 𝑞 ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) →
(𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (1^{st} ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1^{st} ‘(𝐴𝐹(𝐵𝐹𝐶)))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) →
(𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (2^{nd} ‘((𝐴𝐹𝐵)𝐹𝐶)) = (2^{nd} ‘(𝐴𝐹(𝐵𝐹𝐶)))) 

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

⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2^{nd} ‘𝑤)
∧ 𝑧 ∈
(2^{nd} ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) →
(𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  addlocpr 6632* 
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 6599
to both 𝐴 and 𝐵, and uses nqtri3or 6492 rather than prloc 6587 to
decide whether 𝑞 is too big to be in the lower cut of
𝐴
+_{P} 𝐵
(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.)

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

Theorem  addclpr 6633 
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.)

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
+_{P} 𝐵) ∈ P) 

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
+_{P} 𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝐵)𝑥 = (𝑦 +_{Q} 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝐵)𝑥 = (𝑦 +_{Q} 𝑧)}⟩) 

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
·_{P} 𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st}
‘𝐴)∃𝑧 ∈ (1^{st}
‘𝐵)𝑥 = (𝑦 ·_{Q} 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd}
‘𝐴)∃𝑧 ∈ (2^{nd}
‘𝐵)𝑥 = (𝑦 ·_{Q} 𝑧)}⟩) 

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

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

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

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

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

⊢ (𝐴 ∈ Q →
(∃𝑞 ∈
Q 𝑞 ∈
{𝑥 ∣ 𝑥 <_{Q}
𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) 

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

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

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

⊢ (𝐴 ∈ Q →
∀𝑞 ∈
Q ¬ (𝑞
∈ {𝑥 ∣ 𝑥 <_{Q}
𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) 

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

⊢ (𝐴 ∈ Q →
∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<_{Q} 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥}))) 

Theorem  nqprxx 6642* 
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.)

⊢ (𝐴 ∈ Q → ⟨{𝑥 ∣ 𝑥 <_{Q} 𝐴}, {𝑥 ∣ 𝐴 <_{Q} 𝑥}⟩ ∈
P) 

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

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

Theorem  recnnpr 6644* 
The reciprocal of a positive integer, as a positive real. (Contributed
by Jim Kingdon, 27Feb2021.)

⊢ (𝐴 ∈ N → ⟨{𝑙 ∣ 𝑙 <_{Q}
(*_{Q}‘[⟨𝐴, 1_{𝑜}⟩]
~_{Q} )}, {𝑢 ∣
(*_{Q}‘[⟨𝐴, 1_{𝑜}⟩]
~_{Q} ) <_{Q} 𝑢}⟩ ∈
P) 

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

⊢ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∈ V 

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

⊢ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ∈ V 

Theorem  nqprl 6647* 
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.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) →
(𝐴 ∈ (1^{st}
‘𝐵) ↔
⟨{𝑙 ∣ 𝑙 <_{Q}
𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩<_{P} 𝐵)) 

Theorem  nqpru 6648* 
Comparing a fraction to a real can be done by whether it is an element
of the upper cut, or by <_{P}. (Contributed by Jim Kingdon,
29Nov2020.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) →
(𝐴 ∈ (2^{nd}
‘𝐵) ↔ 𝐵<_{P}
⟨{𝑙 ∣ 𝑙 <_{Q}
𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩)) 

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

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

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

⊢ 1_{P} ∈
P 

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

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

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

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

Theorem  addnqprlemrl 6653* 
Lemma for addnqpr 6657. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 19Aug2020.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1^{st} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
+_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆
(1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q}
𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵)
<_{Q} 𝑢}⟩)) 

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

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2^{nd} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
+_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆
(2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q}
𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵)
<_{Q} 𝑢}⟩)) 

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

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q}
𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵)
<_{Q} 𝑢}⟩) ⊆ (1^{st}
‘(⟨{𝑙 ∣
𝑙
<_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
+_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) 

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

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q}
𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵)
<_{Q} 𝑢}⟩) ⊆ (2^{nd}
‘(⟨{𝑙 ∣
𝑙
<_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
+_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) 

Theorem  addnqpr 6657* 
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.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
⟨{𝑙 ∣ 𝑙 <_{Q}
(𝐴
+_{Q} 𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵)
<_{Q} 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
+_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) 

Theorem  addnqpr1 6658* 
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 6657. (Contributed by Jim Kingdon, 26Apr2020.)

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

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

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

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

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

Theorem  prmuloclemcalc 6661 
Calculations for prmuloc 6662. (Contributed by Jim Kingdon,
9Dec2019.)

⊢ (𝜑 → 𝑅 <_{Q} 𝑈) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q}
𝑃)) & ⊢ (𝜑 → (𝐴 +_{Q} 𝑋) = 𝐵)
& ⊢ (𝜑 → (𝑃 ·_{Q} 𝐵)
<_{Q} (𝑅 ·_{Q} 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Q) & ⊢ (𝜑 → 𝐵 ∈ Q) & ⊢ (𝜑 → 𝐷 ∈ Q) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → 𝑋 ∈
Q) ⇒ ⊢ (𝜑 → (𝑈 ·_{Q} 𝐴)
<_{Q} (𝐷 ·_{Q} 𝐵)) 

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

⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 <_{Q}
𝐵) → ∃𝑑 ∈ Q
∃𝑢 ∈
Q (𝑑 ∈
𝐿 ∧ 𝑢 ∈ 𝑈 ∧ (𝑢 ·_{Q} 𝐴)
<_{Q} (𝑑 ·_{Q} 𝐵))) 

Theorem  prmuloc2 6663* 
Positive reals are multiplicatively located. This is a variation of
prmuloc 6662 which only constructs one (named) point and
is therefore often
easier to work with. It states that given a ratio 𝐵, 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} 𝐵) → ∃𝑥 ∈ 𝐿 (𝑥 ·_{Q} 𝐵) ∈ 𝑈) 

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

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

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

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

Theorem  mullocprlem 6666 
Calculations for mullocpr 6667. (Contributed by Jim Kingdon,
10Dec2019.)

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

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

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

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
·_{P} 𝐵) ∈ P) 

Theorem  mulnqprlemrl 6669* 
Lemma for mulnqpr 6673. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 18Jul2021.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1^{st} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆
(1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴
·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵)
<_{Q} 𝑢}⟩)) 

Theorem  mulnqprlemru 6670* 
Lemma for mulnqpr 6673. The reverse subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 18Jul2021.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2^{nd} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆
(2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴
·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵)
<_{Q} 𝑢}⟩)) 

Theorem  mulnqprlemfl 6671* 
Lemma for mulnqpr 6673. The forward subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 18Jul2021.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴
·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵)
<_{Q} 𝑢}⟩) ⊆ (1^{st}
‘(⟨{𝑙 ∣
𝑙
<_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) 

Theorem  mulnqprlemfu 6672* 
Lemma for mulnqpr 6673. The forward subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 18Jul2021.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴
·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵)
<_{Q} 𝑢}⟩) ⊆ (2^{nd}
‘(⟨{𝑙 ∣
𝑙
<_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) 

Theorem  mulnqpr 6673* 
Multiplication of fractions embedded into positive reals. One can
either multiply the fractions as fractions, or embed them into positive
reals and multiply them as positive reals, and get the same result.
(Contributed by Jim Kingdon, 18Jul2021.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
⟨{𝑙 ∣ 𝑙 <_{Q}
(𝐴
·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵)
<_{Q} 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩
·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) 

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
+_{P} 𝐵) = (𝐵 +_{P} 𝐴)) 

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝐴
+_{P} 𝐵) +_{P} 𝐶) = (𝐴 +_{P} (𝐵 +_{P}
𝐶))) 

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
·_{P} 𝐵) = (𝐵 ·_{P} 𝐴)) 

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝐴
·_{P} 𝐵) ·_{P} 𝐶) = (𝐴 ·_{P} (𝐵
·_{P} 𝐶))) 

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

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

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

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

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

⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
∧ ((𝑥 ∈
(1^{st} ‘𝐴)
∧ 𝑦 ∈
(1^{st} ‘𝐵))
∧ (𝑓 ∈
(1^{st} ‘𝐴)
∧ 𝑧 ∈
(1^{st} ‘𝐶)))) → ((𝑥 ·_{Q} 𝑦) +_{Q}
(𝑓
·_{Q} 𝑧)) ∈ (1^{st} ‘(𝐴
·_{P} (𝐵 +_{P} 𝐶)))) 

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

⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
∧ ((𝑥 ∈
(2^{nd} ‘𝐴)
∧ 𝑦 ∈
(2^{nd} ‘𝐵))
∧ (𝑓 ∈
(2^{nd} ‘𝐴)
∧ 𝑧 ∈
(2^{nd} ‘𝐶)))) → ((𝑥 ·_{Q} 𝑦) +_{Q}
(𝑓
·_{Q} 𝑧)) ∈ (2^{nd} ‘(𝐴
·_{P} (𝐵 +_{P} 𝐶)))) 

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

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

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

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

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

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐴
·_{P} (𝐵 +_{P} 𝐶)) = ((𝐴 ·_{P} 𝐵) +_{P}
(𝐴
·_{P} 𝐶))) 

Theorem  ltprordil 6685 
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.)

⊢ (𝐴<_{P} 𝐵 → (1^{st}
‘𝐴) ⊆
(1^{st} ‘𝐵)) 

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

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

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

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

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

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

Theorem  ltnqpr 6689* 
We can order fractions via <_{Q} or <_{P}. (Contributed by Jim
Kingdon, 19Jun2021.)

⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<_{Q} 𝐵 ↔ ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩<_{P}
⟨{𝑙 ∣ 𝑙 <_{Q}
𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) 

Theorem  ltnqpri 6690* 
We can order fractions via <_{Q} or <_{P}. (Contributed by Jim
Kingdon, 8Jan2021.)

⊢ (𝐴 <_{Q} 𝐵 → ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩<_{P}
⟨{𝑙 ∣ 𝑙 <_{Q}
𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩) 

Theorem  ltpopr 6691 
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 6692. (Contributed by Jim Kingdon,
15Dec2019.)

⊢ <_{P} Po
P 

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

⊢ <_{P} Or
P 

Theorem  ltaddpr 6693 
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.)

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
𝐴<_{P} (𝐴 +_{P}
𝐵)) 

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

⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st}
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1^{st}
‘𝐴) ∧ (𝑦 +_{Q}
𝑥) ∈ (2^{nd}
‘𝐵))}⟩ ⇒ ⊢ (𝑞 ∈ (1^{st} ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑞) ∈ (1^{st}
‘𝐵)))) 

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

⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st}
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1^{st}
‘𝐴) ∧ (𝑦 +_{Q}
𝑥) ∈ (2^{nd}
‘𝐵))}⟩ ⇒ ⊢ (𝑟 ∈ (2^{nd} ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (1^{st} ‘𝐴) ∧ (𝑦 +_{Q} 𝑟) ∈ (2^{nd}
‘𝐵)))) 

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

⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st}
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1^{st}
‘𝐴) ∧ (𝑦 +_{Q}
𝑥) ∈ (2^{nd}
‘𝐵))}⟩ ⇒ ⊢ (𝐴<_{P} 𝐵 → (∃𝑞 ∈ Q 𝑞 ∈ (1^{st}
‘𝐶) ∧
∃𝑟 ∈
Q 𝑟 ∈
(2^{nd} ‘𝐶))) 

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

⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st}
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1^{st}
‘𝐴) ∧ (𝑦 +_{Q}
𝑥) ∈ (2^{nd}
‘𝐵))}⟩ ⇒ ⊢ ((𝐴<_{P} 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^{st}
‘𝐶)) →
∃𝑟 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐶))) 

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

⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st}
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1^{st}
‘𝐴) ∧ (𝑦 +_{Q}
𝑥) ∈ (2^{nd}
‘𝐵))}⟩ ⇒ ⊢ ((𝐴<_{P} 𝐵 ∧ 𝑞 ∈ Q) →
(∃𝑟 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐶)) → 𝑞 ∈ (1^{st} ‘𝐶))) 

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

⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st}
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1^{st}
‘𝐴) ∧ (𝑦 +_{Q}
𝑥) ∈ (2^{nd}
‘𝐵))}⟩ ⇒ ⊢ ((𝐴<_{P} 𝐵 ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2^{nd}
‘𝐶)) →
∃𝑞 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘𝐶))) 

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

⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st}
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1^{st}
‘𝐴) ∧ (𝑦 +_{Q}
𝑥) ∈ (2^{nd}
‘𝐵))}⟩ ⇒ ⊢ ((𝐴<_{P} 𝐵 ∧ 𝑟 ∈ Q) →
(∃𝑞 ∈
Q (𝑞
<_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘𝐶)) → 𝑟 ∈ (2^{nd} ‘𝐶))) 