Type  Label  Description 
Statement 

Theorem  mpvlu 7001* 
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 7002 
Domain of addition on positive reals. (Contributed by NM,
18Nov1995.)

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

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

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

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

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

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

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

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

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

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

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

Theorem  nqprxx 7008* 
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 7009* 
The canonical embedding of the rationals into the reals. (Contributed
by Jim Kingdon, 24Jun2020.)

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

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

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

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

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

Theorem  nqprl 7013* 
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 7014* 
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 7015* 
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 7016 
The positive real number 'one'. (Contributed by NM, 13Mar1996.)
(Revised by Mario Carneiro, 12Jun2013.)

⊢ 1_{P} ∈
P 

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

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

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

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

Theorem  addnqprlemrl 7019* 
Lemma for addnqpr 7023. 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 7020* 
Lemma for addnqpr 7023. 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 7021* 
Lemma for addnqpr 7023. 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 7022* 
Lemma for addnqpr 7023. 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 7023* 
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 7024* 
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 7023.
(Contributed by Jim Kingdon, 26Apr2020.)

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

Theorem  appdivnq 7025* 
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 7026* 
Approximate division for positive rationals. This can be thought of as
a variation of appdivnq 7025 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 7027 
Calculations for prmuloc 7028. (Contributed by Jim Kingdon,
9Dec2019.)

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

Theorem  prmuloc 7028* 
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 7029* 
Positive reals are multiplicatively located. This is a variation of
prmuloc 7028 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 7030 
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 7031 
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 7032 
Calculations for mullocpr 7033. (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 7033* 
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 7034 
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 7035* 
Lemma for mulnqpr 7039. 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 7036* 
Lemma for mulnqpr 7039. 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 7037* 
Lemma for mulnqpr 7039. 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 7038* 
Lemma for mulnqpr 7039. 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 7039* 
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 7040 
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 7041 
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 7042 
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 7043 
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 7044 
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 7045 
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 7046* 
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 7047* 
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 7048 
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 7049 
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 7050 
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 7051 
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 7052 
Lemma for 1idpr 7054. (Contributed by Jim Kingdon, 13Dec2019.)

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

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

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

Theorem  1idpr 7054 
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 7055* 
We can order fractions via <_{Q} or <_{P}. (Contributed by Jim
Kingdon, 19Jun2021.)

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

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

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

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

⊢ <_{P} Po
P 

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

⊢ <_{P} Or
P 

Theorem  ltaddpr 7059 
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 7060* 
Element in lower cut of the constructed difference. Lemma for
ltexpri 7075. (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 7061* 
Element in upper cut of the constructed difference. Lemma for
ltexpri 7075. (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 7062* 
Our constructed difference is inhabited. Lemma for ltexpri 7075.
(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 7063* 
The lower cut of our constructed difference is open. Lemma for
ltexpri 7075. (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 7064* 
The lower cut of our constructed difference is lower. Lemma for
ltexpri 7075. (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 7065* 
The upper cut of our constructed difference is open. Lemma for
ltexpri 7075. (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 7066* 
The upper cut of our constructed difference is upper. Lemma for
ltexpri 7075. (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} ‘𝐶))) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ (𝐴<_{P} 𝐵 → ∃𝑥 ∈ P (𝐴 +_{P}
𝑥) = 𝐵) 

Theorem  addcanprleml 7076 
Lemma for addcanprg 7078. (Contributed by Jim Kingdon, 25Dec2019.)

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

Theorem  addcanprlemu 7077 
Lemma for addcanprg 7078. (Contributed by Jim Kingdon, 25Dec2019.)

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

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

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

Theorem  lteupri 7079* 
The difference from ltexpri 7075 is unique. (Contributed by Jim Kingdon,
7Jul2021.)

⊢ (𝐴<_{P} 𝐵 → ∃!𝑥 ∈ P (𝐴 +_{P}
𝑥) = 𝐵) 

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

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

Theorem  ltaprg 7081 
Ordering property of addition. Proposition 93.5(v) of [Gleason]
p. 123. (Contributed by Jim Kingdon, 26Dec2019.)

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

Theorem  prplnqu 7082* 
Membership in the upper cut of a sum of a positive real and a fraction.
(Contributed by Jim Kingdon, 16Jun2021.)

⊢ (𝜑 → 𝑋 ∈ P) & ⊢ (𝜑 → 𝑄 ∈ Q) & ⊢ (𝜑 → 𝐴 ∈ (2^{nd} ‘(𝑋 +_{P}
⟨{𝑙 ∣ 𝑙 <_{Q}
𝑄}, {𝑢 ∣ 𝑄 <_{Q} 𝑢}⟩))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (2^{nd} ‘𝑋)(𝑦 +_{Q} 𝑄) = 𝐴) 

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

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

Theorem  recexprlemell 7084* 
Membership in the lower cut of 𝐵. Lemma for recexpr 7100.
(Contributed by Jim Kingdon, 27Dec2019.)

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

Theorem  recexprlemelu 7085* 
Membership in the upper cut of 𝐵. Lemma for recexpr 7100.
(Contributed by Jim Kingdon, 27Dec2019.)

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

Theorem  recexprlemm 7086* 
𝐵
is inhabited. Lemma for recexpr 7100. (Contributed by Jim Kingdon,
27Dec2019.)

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

Theorem  recexprlemopl 7087* 
The lower cut of 𝐵 is open. Lemma for recexpr 7100. (Contributed by
Jim Kingdon, 28Dec2019.)

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

Theorem  recexprlemlol 7088* 
The lower cut of 𝐵 is lower. Lemma for recexpr 7100. (Contributed by
Jim Kingdon, 28Dec2019.)

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

Theorem  recexprlemopu 7089* 
The upper cut of 𝐵 is open. Lemma for recexpr 7100. (Contributed by
Jim Kingdon, 28Dec2019.)

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

Theorem  recexprlemupu 7090* 
The upper cut of 𝐵 is upper. Lemma for recexpr 7100. (Contributed by
Jim Kingdon, 28Dec2019.)

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

Theorem  recexprlemrnd 7091* 
𝐵
is rounded. Lemma for recexpr 7100. (Contributed by Jim Kingdon,
27Dec2019.)

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

Theorem  recexprlemdisj 7092* 
𝐵
is disjoint. Lemma for recexpr 7100. (Contributed by Jim Kingdon,
27Dec2019.)

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

Theorem  recexprlemloc 7093* 
𝐵
is located. Lemma for recexpr 7100. (Contributed by Jim Kingdon,
27Dec2019.)

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

Theorem  recexprlempr 7094* 
𝐵
is a positive real. Lemma for recexpr 7100. (Contributed by Jim
Kingdon, 27Dec2019.)

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

Theorem  recexprlem1ssl 7095* 
The lower cut of one is a subset of the lower cut of 𝐴
·_{P} 𝐵.
Lemma for recexpr 7100. (Contributed by Jim Kingdon, 27Dec2019.)

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

Theorem  recexprlem1ssu 7096* 
The upper cut of one is a subset of the upper cut of 𝐴
·_{P} 𝐵.
Lemma for recexpr 7100. (Contributed by Jim Kingdon, 27Dec2019.)

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

Theorem  recexprlemss1l 7097* 
The lower cut of 𝐴 ·_{P} 𝐵 is a subset of the lower
cut of one. Lemma
for recexpr 7100. (Contributed by Jim Kingdon, 27Dec2019.)

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

Theorem  recexprlemss1u 7098* 
The upper cut of 𝐴 ·_{P} 𝐵 is a subset of the upper
cut of one. Lemma
for recexpr 7100. (Contributed by Jim Kingdon, 27Dec2019.)

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

Theorem  recexprlemex 7099* 
𝐵
is the reciprocal of 𝐴. Lemma for recexpr 7100. (Contributed
by Jim Kingdon, 27Dec2019.)

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

Theorem  recexpr 7100* 
The reciprocal of a positive real exists. Part of Proposition 93.7(v)
of [Gleason] p. 124. (Contributed by
NM, 15May1996.) (Revised by
Mario Carneiro, 12Jun2013.)

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