Type  Label  Description 
Statement 

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

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

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

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

Theorem  nqprl 6803* 
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 6804* 
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 6805* 
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 6806 
The positive real number 'one'. (Contributed by NM, 13Mar1996.)
(Revised by Mario Carneiro, 12Jun2013.)

⊢ 1_{P} ∈
P 

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

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

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

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

Theorem  addnqprlemrl 6809* 
Lemma for addnqpr 6813. 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 6810* 
Lemma for addnqpr 6813. 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 6811* 
Lemma for addnqpr 6813. 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 6812* 
Lemma for addnqpr 6813. 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 6813* 
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 6814* 
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 6813.
(Contributed by Jim Kingdon, 26Apr2020.)

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

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

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

Theorem  prmuloc 6818* 
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 6819* 
Positive reals are multiplicatively located. This is a variation of
prmuloc 6818 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 6820 
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 6821 
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 6822 
Calculations for mullocpr 6823. (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 6823* 
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 6824 
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 6825* 
Lemma for mulnqpr 6829. 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 6826* 
Lemma for mulnqpr 6829. 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 6827* 
Lemma for mulnqpr 6829. 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 6828* 
Lemma for mulnqpr 6829. 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 6829* 
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 6830 
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 6831 
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 6832 
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 6833 
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 6834 
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 6835 
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 6836* 
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 6837* 
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 6838 
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 6839 
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 6840 
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 6841 
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 6842 
Lemma for 1idpr 6844. (Contributed by Jim Kingdon, 13Dec2019.)

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

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

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

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

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

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

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

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

⊢ <_{P} Po
P 

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

⊢ <_{P} Or
P 

Theorem  ltaddpr 6849 
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 6850* 
Element in lower cut of the constructed difference. Lemma for
ltexpri 6865. (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 6851* 
Element in upper cut of the constructed difference. Lemma for
ltexpri 6865. (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 6852* 
Our constructed difference is inhabited. Lemma for ltexpri 6865.
(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 6853* 
The lower cut of our constructed difference is open. Lemma for
ltexpri 6865. (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 6854* 
The lower cut of our constructed difference is lower. Lemma for
ltexpri 6865. (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 6855* 
The upper cut of our constructed difference is open. Lemma for
ltexpri 6865. (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 6856* 
The upper cut of our constructed difference is upper. Lemma for
ltexpri 6865. (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 6857* 
Our constructed difference is rounded. Lemma for ltexpri 6865.
(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 6858* 
Our constructed difference is disjoint. Lemma for ltexpri 6865.
(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 6859* 
Our constructed difference is located. Lemma for ltexpri 6865.
(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 6860* 
Our constructed difference is a positive real. Lemma for ltexpri 6865.
(Contributed by Jim Kingdon, 17Dec2019.)

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

Theorem  ltexprlemfl 6861* 
Lemma for ltexpri 6865. 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 6862* 
Lemma for ltexpri 6865. 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 6863* 
Lemma for ltexpri 6865. 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 6864* 
Lemma for ltexpri 6865. 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 6865* 
Proposition 93.5(iv) of [Gleason] p. 123.
(Contributed by NM,
13May1996.) (Revised by Mario Carneiro, 14Jun2013.)

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

Theorem  addcanprleml 6866 
Lemma for addcanprg 6868. (Contributed by Jim Kingdon, 25Dec2019.)

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

Theorem  addcanprlemu 6867 
Lemma for addcanprg 6868. (Contributed by Jim Kingdon, 25Dec2019.)

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

Theorem  addcanprg 6868 
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 6869* 
The difference from ltexpri 6865 is unique. (Contributed by Jim Kingdon,
7Jul2021.)

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

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

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

Theorem  ltaprg 6871 
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 6872* 
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 6873 
Strong extensionality of addition (ordering version). This is similar
to addext 7777 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 6874* 
Membership in the lower cut of 𝐵. Lemma for recexpr 6890.
(Contributed by Jim Kingdon, 27Dec2019.)

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  recexprlemrnd 6881* 
𝐵
is rounded. Lemma for recexpr 6890. (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 6882* 
𝐵
is disjoint. Lemma for recexpr 6890. (Contributed by Jim Kingdon,
27Dec2019.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  recexpr 6890* 
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}) 

Theorem  aptiprleml 6891 
Lemma for aptipr 6893. (Contributed by Jim Kingdon, 28Jan2020.)

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

Theorem  aptiprlemu 6892 
Lemma for aptipr 6893. (Contributed by Jim Kingdon, 28Jan2020.)

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
¬ 𝐵<_{P} 𝐴) → (2^{nd}
‘𝐵) ⊆
(2^{nd} ‘𝐴)) 

Theorem  aptipr 6893 
Apartness of positive reals is tight. (Contributed by Jim Kingdon,
28Jan2020.)

⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
¬ (𝐴<_{P} 𝐵 ∨ 𝐵<_{P} 𝐴)) → 𝐴 = 𝐵) 

Theorem  ltmprr 6894 
Ordering property of multiplication. (Contributed by Jim Kingdon,
18Feb2020.)

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

Theorem  archpr 6895* 
For any positive real, there is an integer that is greater than it.
This is also known as the "archimedean property". The integer
𝑥
is
embedded into the reals as described at nnprlu 6805. (Contributed by Jim
Kingdon, 22Apr2020.)

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

Theorem  caucvgprlemcanl 6896* 
Lemma for cauappcvgprlemladdrl 6909. Cancelling a term from both sides.
(Contributed by Jim Kingdon, 15Aug2020.)

⊢ (𝜑 → 𝐿 ∈ P) & ⊢ (𝜑 → 𝑆 ∈ Q) & ⊢ (𝜑 → 𝑅 ∈ Q) & ⊢ (𝜑 → 𝑄 ∈
Q) ⇒ ⊢ (𝜑 → ((𝑅 +_{Q} 𝑄) ∈ (1^{st}
‘(𝐿
+_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} (𝑆 +_{Q}
𝑄)}, {𝑢 ∣ (𝑆 +_{Q} 𝑄)
<_{Q} 𝑢}⟩)) ↔ 𝑅 ∈ (1^{st} ‘(𝐿 +_{P}
⟨{𝑙 ∣ 𝑙 <_{Q}
𝑆}, {𝑢 ∣ 𝑆 <_{Q} 𝑢}⟩)))) 

Theorem  cauappcvgprlemm 6897* 
Lemma for cauappcvgpr 6914. The putative limit is inhabited.
(Contributed by Jim Kingdon, 18Jul2020.)

⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <_{Q} ((𝐹‘𝑞) +_{Q} (𝑝 +_{Q} 𝑞)) ∧ (𝐹‘𝑞) <_{Q} ((𝐹‘𝑝) +_{Q} (𝑝 +_{Q} 𝑞))))
& ⊢ (𝜑
→ ∀𝑝 ∈
Q 𝐴
<_{Q} (𝐹‘𝑝))
& ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +_{Q} 𝑞) <_{Q} (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +_{Q} 𝑞) <_{Q} 𝑢}⟩ ⇒ ⊢ (𝜑
→ (∃𝑠 ∈
Q 𝑠 ∈
(1^{st} ‘𝐿) ∧
∃𝑟 ∈ Q
𝑟 ∈ (2^{nd}
‘𝐿))) 

Theorem  cauappcvgprlemopl 6898* 
Lemma for cauappcvgpr 6914. The lower cut of the putative limit is
open. (Contributed by Jim Kingdon, 4Aug2020.)

⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <_{Q} ((𝐹‘𝑞) +_{Q} (𝑝 +_{Q} 𝑞)) ∧ (𝐹‘𝑞) <_{Q} ((𝐹‘𝑝) +_{Q} (𝑝 +_{Q} 𝑞))))
& ⊢ (𝜑
→ ∀𝑝 ∈
Q 𝐴
<_{Q} (𝐹‘𝑝))
& ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +_{Q} 𝑞) <_{Q} (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +_{Q} 𝑞) <_{Q} 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 ∈ (1^{st} ‘𝐿)) → ∃𝑟 ∈ Q (𝑠 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐿))) 

Theorem  cauappcvgprlemlol 6899* 
Lemma for cauappcvgpr 6914. The lower cut of the putative limit is
lower. (Contributed by Jim Kingdon, 4Aug2020.)

⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <_{Q} ((𝐹‘𝑞) +_{Q} (𝑝 +_{Q} 𝑞)) ∧ (𝐹‘𝑞) <_{Q} ((𝐹‘𝑝) +_{Q} (𝑝 +_{Q} 𝑞))))
& ⊢ (𝜑
→ ∀𝑝 ∈
Q 𝐴
<_{Q} (𝐹‘𝑝))
& ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +_{Q} 𝑞) <_{Q} (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +_{Q} 𝑞) <_{Q} 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐿)) → 𝑠 ∈ (1^{st} ‘𝐿)) 

Theorem  cauappcvgprlemopu 6900* 
Lemma for cauappcvgpr 6914. The upper cut of the putative limit is
open. (Contributed by Jim Kingdon, 4Aug2020.)

⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <_{Q} ((𝐹‘𝑞) +_{Q} (𝑝 +_{Q} 𝑞)) ∧ (𝐹‘𝑞) <_{Q} ((𝐹‘𝑝) +_{Q} (𝑝 +_{Q} 𝑞))))
& ⊢ (𝜑
→ ∀𝑝 ∈
Q 𝐴
<_{Q} (𝐹‘𝑝))
& ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +_{Q} 𝑞) <_{Q} (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +_{Q} 𝑞) <_{Q} 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑟 ∈ (2^{nd} ‘𝐿)) → ∃𝑠 ∈ Q (𝑠 <_{Q} 𝑟 ∧ 𝑠 ∈ (2^{nd} ‘𝐿))) 