P. 76 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	addnqprllem 7501	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <Q 𝑆 → ((𝑋 ·Q (*Q‘𝑆)) ·Q 𝐺) ∈ 𝐿))
Theorem	addnqprulem 7502	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <Q 𝑋 → ((𝑋 ·Q (*Q‘𝑆)) ·Q 𝐺) ∈ 𝑈))
Theorem	addnqprl 7503	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (1st ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (1st ‘𝐵))) ∧ 𝑋 ∈ Q) → (𝑋 <Q (𝐺 +Q 𝐻) → 𝑋 ∈ (1st ‘(𝐴 +P 𝐵))))
Theorem	addnqpru 7504	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (2nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (2nd ‘𝐵))) ∧ 𝑋 ∈ Q) → ((𝐺 +Q 𝐻) <Q 𝑋 → 𝑋 ∈ (2nd ‘(𝐴 +P 𝐵))))
Theorem	addlocprlemlt 7505	Lemma for addlocpr 7510. The 𝑄 <Q (𝐷 +Q 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ P)    &   ⊢ (𝜑 → 𝐵 ∈ P)    &   ⊢ (𝜑 → 𝑄 <Q 𝑅)    &   ⊢ (𝜑 → 𝑃 ∈ Q)    &   ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴))    &   ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q 𝑃))    &   ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵))    &   ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q 𝑃))    ⇒   ⊢ (𝜑 → (𝑄 <Q (𝐷 +Q 𝐸) → 𝑄 ∈ (1st ‘(𝐴 +P 𝐵))))
Theorem	addlocprlemeqgt 7506	Lemma for addlocpr 7510. This is a step used in both the 𝑄 = (𝐷 +Q 𝐸) and (𝐷 +Q 𝐸) <Q 𝑄 cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ P)    &   ⊢ (𝜑 → 𝐵 ∈ P)    &   ⊢ (𝜑 → 𝑄 <Q 𝑅)    &   ⊢ (𝜑 → 𝑃 ∈ Q)    &   ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴))    &   ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q 𝑃))    &   ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵))    &   ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q 𝑃))    ⇒   ⊢ (𝜑 → (𝑈 +Q 𝑇) <Q ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)))
Theorem	addlocprlemeq 7507	Lemma for addlocpr 7510. The 𝑄 = (𝐷 +Q 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ P)    &   ⊢ (𝜑 → 𝐵 ∈ P)    &   ⊢ (𝜑 → 𝑄 <Q 𝑅)    &   ⊢ (𝜑 → 𝑃 ∈ Q)    &   ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴))    &   ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q 𝑃))    &   ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵))    &   ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q 𝑃))    ⇒   ⊢ (𝜑 → (𝑄 = (𝐷 +Q 𝐸) → 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
Theorem	addlocprlemgt 7508	Lemma for addlocpr 7510. The (𝐷 +Q 𝐸) <Q 𝑄 case. (Contributed by Jim Kingdon, 6-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ P)    &   ⊢ (𝜑 → 𝐵 ∈ P)    &   ⊢ (𝜑 → 𝑄 <Q 𝑅)    &   ⊢ (𝜑 → 𝑃 ∈ Q)    &   ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴))    &   ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q 𝑃))    &   ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵))    &   ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q 𝑃))    ⇒   ⊢ (𝜑 → ((𝐷 +Q 𝐸) <Q 𝑄 → 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
Theorem	addlocprlem 7509	Lemma for addlocpr 7510. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ P)    &   ⊢ (𝜑 → 𝐵 ∈ P)    &   ⊢ (𝜑 → 𝑄 <Q 𝑅)    &   ⊢ (𝜑 → 𝑃 ∈ Q)    &   ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴))    &   ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q 𝑃))    &   ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵))    &   ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q 𝑃))    ⇒   ⊢ (𝜑 → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
Theorem	addlocpr 7510*	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 7477 to both 𝐴 and 𝐵, and uses nqtri3or 7370 rather than prloc 7465 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, 5-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)))))
Theorem	addclpr 7511	Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. Combination of Lemma 11.13 and Lemma 11.16 in [BauerTaylor], p. 53. (Contributed by NM, 13-Mar-1996.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) ∈ P)
Theorem	plpvlu 7512*	Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1st ‘𝐴)∃𝑧 ∈ (1st ‘𝐵)𝑥 = (𝑦 +Q 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2nd ‘𝐴)∃𝑧 ∈ (2nd ‘𝐵)𝑥 = (𝑦 +Q 𝑧)}⟩)
Theorem	mpvlu 7513*	Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1st ‘𝐴)∃𝑧 ∈ (1st ‘𝐵)𝑥 = (𝑦 ·Q 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2nd ‘𝐴)∃𝑧 ∈ (2nd ‘𝐵)𝑥 = (𝑦 ·Q 𝑧)}⟩)
Theorem	dmplp 7514	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.)
⊢ dom +P = (P × P)
Theorem	dmmp 7515	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.)
⊢ dom ·P = (P × P)
Theorem	nqprm 7516*	A cut produced from a rational is inhabited. Lemma for nqprlu 7521. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → (∃𝑞 ∈ Q 𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))
Theorem	nqprrnd 7517*	A cut produced from a rational is rounded. Lemma for nqprlu 7521. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → (∀𝑞 ∈ Q (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) ∧ ∀𝑟 ∈ Q (𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥} ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))))
Theorem	nqprdisj 7518*	A cut produced from a rational is disjoint. Lemma for nqprlu 7521. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ¬ (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))
Theorem	nqprloc 7519*	A cut produced from a rational is located. Lemma for nqprlu 7521. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})))
Theorem	nqprxx 7520*	The canonical embedding of the rationals into the reals, expressed with the same variable for the lower and upper cuts. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → ⟨{𝑥 ∣ 𝑥 <Q 𝐴}, {𝑥 ∣ 𝐴 <Q 𝑥}⟩ ∈ P)
Theorem	nqprlu 7521*	The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈ P)
Theorem	recnnpr 7522*	The reciprocal of a positive integer, as a positive real. (Contributed by Jim Kingdon, 27-Feb-2021.)
⊢ (𝐴 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝐴, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1o⟩] ~Q ) <Q 𝑢}⟩ ∈ P)
Theorem	ltnqex 7523	The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {𝑥 ∣ 𝑥 <Q 𝐴} ∈ V
Theorem	gtnqex 7524	The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {𝑥 ∣ 𝐴 <Q 𝑥} ∈ V
Theorem	nqprl 7525*	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, 8-Jul-2020.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) → (𝐴 ∈ (1st ‘𝐵) ↔ ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩<P 𝐵))
Theorem	nqpru 7526*	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, 29-Nov-2020.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) → (𝐴 ∈ (2nd ‘𝐵) ↔ 𝐵<P ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩))
Theorem	nnprlu 7527*	The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
⊢ (𝐴 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q [⟨𝐴, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐴, 1o⟩] ~Q <Q 𝑢}⟩ ∈ P)
Theorem	1pr 7528	The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
⊢ 1P ∈ P
Theorem	1prl 7529	The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (1st ‘1P) = {𝑥 ∣ 𝑥 <Q 1Q}
Theorem	1pru 7530	The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (2nd ‘1P) = {𝑥 ∣ 1Q <Q 𝑥}
Theorem	addnqprlemrl 7531*	Lemma for addnqpr 7535. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆ (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q 𝑢}⟩))
Theorem	addnqprlemru 7532*	Lemma for addnqpr 7535. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q 𝑢}⟩))
Theorem	addnqprlemfl 7533*	Lemma for addnqpr 7535. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q 𝑢}⟩) ⊆ (1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))
Theorem	addnqprlemfu 7534*	Lemma for addnqpr 7535. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q 𝑢}⟩) ⊆ (2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))
Theorem	addnqpr 7535*	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, 19-Aug-2020.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → ⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))
Theorem	addnqpr1 7536*	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 7535. (Contributed by Jim Kingdon, 26-Apr-2020.)
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q 1Q)}, {𝑢 ∣ (𝐴 +Q 1Q) <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ +P 1P))
Theorem	appdivnq 7537*	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, 8-Dec-2019.)
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q (𝐴 <Q (𝑚 ·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q 𝐵))
Theorem	appdiv0nq 7538*	Approximate division for positive rationals. This can be thought of as a variation of appdivnq 7537 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, 9-Dec-2019.)
⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q (𝑚 ·Q 𝐶) <Q 𝐵)
Theorem	prmuloclemcalc 7539	Calculations for prmuloc 7540. (Contributed by Jim Kingdon, 9-Dec-2019.)
⊢ (𝜑 → 𝑅 <Q 𝑈)    &   ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q 𝑃))    &   ⊢ (𝜑 → (𝐴 +Q 𝑋) = 𝐵)    &   ⊢ (𝜑 → (𝑃 ·Q 𝐵) <Q (𝑅 ·Q 𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Q)    &   ⊢ (𝜑 → 𝐵 ∈ Q)    &   ⊢ (𝜑 → 𝐷 ∈ Q)    &   ⊢ (𝜑 → 𝑃 ∈ Q)    &   ⊢ (𝜑 → 𝑋 ∈ Q)    ⇒   ⊢ (𝜑 → (𝑈 ·Q 𝐴) <Q (𝐷 ·Q 𝐵))
Theorem	prmuloc 7540*	Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 <Q 𝐵) → ∃𝑑 ∈ Q ∃𝑢 ∈ Q (𝑑 ∈ 𝐿 ∧ 𝑢 ∈ 𝑈 ∧ (𝑢 ·Q 𝐴) <Q (𝑑 ·Q 𝐵)))
Theorem	prmuloc2 7541*	Positive reals are multiplicatively located. This is a variation of prmuloc 7540 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, 28-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 1Q <Q 𝐵) → ∃𝑥 ∈ 𝐿 (𝑥 ·Q 𝐵) ∈ 𝑈)
Theorem	mulnqprl 7542	Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (1st ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (1st ‘𝐵))) ∧ 𝑋 ∈ Q) → (𝑋 <Q (𝐺 ·Q 𝐻) → 𝑋 ∈ (1st ‘(𝐴 ·P 𝐵))))
Theorem	mulnqpru 7543	Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (2nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (2nd ‘𝐵))) ∧ 𝑋 ∈ Q) → ((𝐺 ·Q 𝐻) <Q 𝑋 → 𝑋 ∈ (2nd ‘(𝐴 ·P 𝐵))))
Theorem	mullocprlem 7544	Calculations for mullocpr 7545. (Contributed by Jim Kingdon, 10-Dec-2019.)
⊢ (𝜑 → (𝐴 ∈ P ∧ 𝐵 ∈ P))    &   ⊢ (𝜑 → (𝑈 ·Q 𝑄) <Q (𝐸 ·Q (𝐷 ·Q 𝑈)))    &   ⊢ (𝜑 → (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈)))    &   ⊢ (𝜑 → (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅))    &   ⊢ (𝜑 → (𝑄 ∈ Q ∧ 𝑅 ∈ Q))    &   ⊢ (𝜑 → (𝐷 ∈ Q ∧ 𝑈 ∈ Q))    &   ⊢ (𝜑 → (𝐷 ∈ (1st ‘𝐴) ∧ 𝑈 ∈ (2nd ‘𝐴)))    &   ⊢ (𝜑 → (𝐸 ∈ Q ∧ 𝑇 ∈ Q))    ⇒   ⊢ (𝜑 → (𝑄 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 ·P 𝐵))))
Theorem	mullocpr 7545*	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, 8-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
Theorem	mulclpr 7546	Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) ∈ P)
Theorem	mulnqprlemrl 7547*	Lemma for mulnqpr 7551. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ·P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆ (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q 𝑢}⟩))
Theorem	mulnqprlemru 7548*	Lemma for mulnqpr 7551. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ·P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q 𝑢}⟩))
Theorem	mulnqprlemfl 7549*	Lemma for mulnqpr 7551. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q 𝑢}⟩) ⊆ (1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ·P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))
Theorem	mulnqprlemfu 7550*	Lemma for mulnqpr 7551. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q 𝑢}⟩) ⊆ (2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ·P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))
Theorem	mulnqpr 7551*	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, 18-Jul-2021.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → ⟨{𝑙 ∣ 𝑙 <Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ·P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))
Theorem	addcomprg 7552	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) = (𝐵 +P 𝐴))
Theorem	addassprg 7553	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 +P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P 𝐶)))
Theorem	mulcomprg 7554	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) = (𝐵 ·P 𝐴))
Theorem	mulassprg 7555	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 ·P 𝐵) ·P 𝐶) = (𝐴 ·P (𝐵 ·P 𝐶)))
Theorem	distrlem1prl 7556	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1st ‘(𝐴 ·P (𝐵 +P 𝐶))) ⊆ (1st ‘((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶))))
Theorem	distrlem1pru 7557	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (2nd ‘(𝐴 ·P (𝐵 +P 𝐶))) ⊆ (2nd ‘((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶))))
Theorem	distrlem4prl 7558*	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ ((𝑥 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (1st ‘𝐵)) ∧ (𝑓 ∈ (1st ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐶)))) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
Theorem	distrlem4pru 7559*	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ ((𝑥 ∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (2nd ‘(𝐴 ·P (𝐵 +P 𝐶))))
Theorem	distrlem5prl 7560	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1st ‘((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶))) ⊆ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
Theorem	distrlem5pru 7561	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (2nd ‘((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶))) ⊆ (2nd ‘(𝐴 ·P (𝐵 +P 𝐶))))
Theorem	distrprg 7562	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐴 ·P (𝐵 +P 𝐶)) = ((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶)))
Theorem	ltprordil 7563	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, 23-Dec-2019.)
⊢ (𝐴<P 𝐵 → (1st ‘𝐴) ⊆ (1st ‘𝐵))
Theorem	1idprl 7564	Lemma for 1idpr 7566. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ (𝐴 ∈ P → (1st ‘(𝐴 ·P 1P)) = (1st ‘𝐴))
Theorem	1idpru 7565	Lemma for 1idpr 7566. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ (𝐴 ∈ P → (2nd ‘(𝐴 ·P 1P)) = (2nd ‘𝐴))
Theorem	1idpr 7566	1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.)
⊢ (𝐴 ∈ P → (𝐴 ·P 1P) = 𝐴)
Theorem	ltnqpr 7567*	We can order fractions via <Q or <P. (Contributed by Jim Kingdon, 19-Jun-2021.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩<P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))
Theorem	ltnqpri 7568*	We can order fractions via <Q or <P. (Contributed by Jim Kingdon, 8-Jan-2021.)
⊢ (𝐴 <Q 𝐵 → ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩<P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)
Theorem	ltpopr 7569	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 7570. (Contributed by Jim Kingdon, 15-Dec-2019.)
⊢ <P Po P
Theorem	ltsopr 7570	Positive real 'less than' is a weak linear order (in the sense of df-iso 4291). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
⊢ <P Or P
Theorem	ltaddpr 7571	The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123. (Contributed by NM, 26-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → 𝐴<P (𝐴 +P 𝐵))
Theorem	ltexprlemell 7572*	Element in lower cut of the constructed difference. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st ‘𝐵))))
Theorem	ltexprlemelu 7573*	Element in upper cut of the constructed difference. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd ‘𝐵))))
Theorem	ltexprlemm 7574*	Our constructed difference is inhabited. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemopl 7575*	The lower cut of our constructed difference is open. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ ((𝐴<P 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)))
Theorem	ltexprlemlol 7576*	The lower cut of our constructed difference is lower. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ ((𝐴<P 𝐵 ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)) → 𝑞 ∈ (1st ‘𝐶)))
Theorem	ltexprlemopu 7577*	The upper cut of our constructed difference is open. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemupu 7578*	The upper cut of our constructed difference is upper. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) → 𝑟 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemrnd 7579*	Our constructed difference is rounded. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐶) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))))
Theorem	ltexprlemdisj 7580*	Our constructed difference is disjoint. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐶) ∧ 𝑞 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemloc 7581*	Our constructed difference is located. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))
Theorem	ltexprlempr 7582*	Our constructed difference is a positive real. Lemma for ltexpri 7587. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → 𝐶 ∈ P)
Theorem	ltexprlemfl 7583*	Lemma for ltexpri 7587. One direction of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → (1st ‘(𝐴 +P 𝐶)) ⊆ (1st ‘𝐵))
Theorem	ltexprlemrl 7584*	Lemma for ltexpri 7587. Reverse direction of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → (1st ‘𝐵) ⊆ (1st ‘(𝐴 +P 𝐶)))
Theorem	ltexprlemfu 7585*	Lemma for ltexpri 7587. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → (2nd ‘(𝐴 +P 𝐶)) ⊆ (2nd ‘𝐵))
Theorem	ltexprlemru 7586*	Lemma for ltexpri 7587. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩    ⇒   ⊢ (𝐴<P 𝐵 → (2nd ‘𝐵) ⊆ (2nd ‘(𝐴 +P 𝐶)))
Theorem	ltexpri 7587*	Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.)
⊢ (𝐴<P 𝐵 → ∃𝑥 ∈ P (𝐴 +P 𝑥) = 𝐵)
Theorem	addcanprleml 7588	Lemma for addcanprg 7590. (Contributed by Jim Kingdon, 25-Dec-2019.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (1st ‘𝐵) ⊆ (1st ‘𝐶))
Theorem	addcanprlemu 7589	Lemma for addcanprg 7590. (Contributed by Jim Kingdon, 25-Dec-2019.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (2nd ‘𝐵) ⊆ (2nd ‘𝐶))
Theorem	addcanprg 7590	Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 +P 𝐵) = (𝐴 +P 𝐶) → 𝐵 = 𝐶))
Theorem	lteupri 7591*	The difference from ltexpri 7587 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.)
⊢ (𝐴<P 𝐵 → ∃!𝑥 ∈ P (𝐴 +P 𝑥) = 𝐵)
Theorem	ltaprlem 7592	Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.)
⊢ (𝐶 ∈ P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
Theorem	ltaprg 7593	Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐴<P 𝐵 ↔ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
Theorem	prplnqu 7594*	Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ P)    &   ⊢ (𝜑 → 𝑄 ∈ Q)    &   ⊢ (𝜑 → 𝐴 ∈ (2nd ‘(𝑋 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩)))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (2nd ‘𝑋)(𝑦 +Q 𝑄) = 𝐴)
Theorem	addextpr 7595	Strong extensionality of addition (ordering version). This is similar to addext 8541 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → (𝐴<P 𝐶 ∨ 𝐵<P 𝐷)))
Theorem	recexprlemell 7596*	Membership in the lower cut of 𝐵. Lemma for recexpr 7612. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐶 ∈ (1st ‘𝐵) ↔ ∃𝑦(𝐶 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴)))
Theorem	recexprlemelu 7597*	Membership in the upper cut of 𝐵. Lemma for recexpr 7612. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐶 ∈ (2nd ‘𝐵) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴)))
Theorem	recexprlemm 7598*	𝐵 is inhabited. Lemma for recexpr 7612. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐴 ∈ P → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐵) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐵)))
Theorem	recexprlemopl 7599*	The lower cut of 𝐵 is open. Lemma for recexpr 7612. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘𝐵)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐵)))
Theorem	recexprlemlol 7600*	The lower cut of 𝐵 is lower. Lemma for recexpr 7612. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐵)) → 𝑞 ∈ (1st ‘𝐵)))