P. 75 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7401-7500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulcomnq0 7401	Multiplication of nonnegative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.)
⊢ ((𝐴 ∈ Q0 ∧ 𝐵 ∈ Q0) → (𝐴 ·Q0 𝐵) = (𝐵 ·Q0 𝐴))
Theorem	addassnq0lemcl 7402	A natural number closure law. Lemma for addassnq0 7403. (Contributed by Jim Kingdon, 3-Dec-2019.)
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ N) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ N)) → (((𝐼 ·o 𝐿) +o (𝐽 ·o 𝐾)) ∈ ω ∧ (𝐽 ·o 𝐿) ∈ N))
Theorem	addassnq0 7403	Addition of nonnegative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ ((𝐴 ∈ Q0 ∧ 𝐵 ∈ Q0 ∧ 𝐶 ∈ Q0) → ((𝐴 +Q0 𝐵) +Q0 𝐶) = (𝐴 +Q0 (𝐵 +Q0 𝐶)))
Theorem	distnq0r 7404	Multiplication of nonnegative fractions is distributive. Version of distrnq0 7400 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ ((𝐴 ∈ Q0 ∧ 𝐵 ∈ Q0 ∧ 𝐶 ∈ Q0) → ((𝐵 +Q0 𝐶) ·Q0 𝐴) = ((𝐵 ·Q0 𝐴) +Q0 (𝐶 ·Q0 𝐴)))
Theorem	addpinq1 7405	Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.)
⊢ (𝐴 ∈ N → [⟨(𝐴 +N 1o), 1o⟩] ~Q = ([⟨𝐴, 1o⟩] ~Q +Q 1Q))
Theorem	nq02m 7406	Multiply a nonnegative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ (𝐴 ∈ Q0 → ([⟨2o, 1o⟩] ~Q0 ·Q0 𝐴) = (𝐴 +Q0 𝐴))
Definition	df-inp 7407*	Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. Here we follow the definition of a Dedekind cut from Definition 11.2.1 of [HoTT], p. (varies) with the one exception that we define it over positive rational numbers rather than all rational numbers. A Dedekind cut is an ordered pair of a lower set 𝑙 and an upper set 𝑢 which is inhabited (∃𝑞 ∈ Q𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q𝑟 ∈ 𝑢), rounded (∀𝑞 ∈ Q(𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q(𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) and likewise for 𝑢), disjoint (∀𝑞 ∈ Q¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢)) and located (∀𝑞 ∈ Q∀𝑟 ∈ Q(𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))). See HoTT for more discussion of those terms and different ways of defining Dedekind cuts. (Note: This is a "temporary" definition used in the construction of complex numbers, and is intended to be used only by the construction.) (Contributed by Jim Kingdon, 25-Sep-2019.)
⊢ P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))}
Definition	df-i1p 7408*	Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by Jim Kingdon, 25-Sep-2019.)
⊢ 1P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
Definition	df-iplp 7409*	Define addition on positive reals. From Section 11.2.1 of [HoTT], p. (varies). We write this definition to closely resemble the definition in HoTT although some of the conditions are redundant (for example, 𝑟 ∈ (1st ‘𝑥) implies 𝑟 ∈ Q) and can be simplified as shown at genpdf 7449. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 26-Sep-2019.)
⊢ +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
Definition	df-imp 7410*	Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7409 or the definition of multiplication on positive reals in Metamath Proof Explorer. This is as opposed to the more complicated definition of multiplication given in Section 11.2.1 of [HoTT], p. (varies), which appears to be motivated by handling negative numbers or handling modified Dedekind cuts in which locatedness is omitted. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 29-Sep-2019.)
⊢ ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
Definition	df-iltp 7411*	Define ordering on positive reals. We define 𝑥<P 𝑦 if there is a positive fraction 𝑞 which is an element of the upper cut of 𝑥 and the lower cut of 𝑦. From the definition of < in Section 11.2.1 of [HoTT], p. (varies). This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 29-Sep-2019.)
⊢ <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}
Theorem	npsspw 7412	Lemma for proving existence of reals. (Contributed by Jim Kingdon, 27-Sep-2019.)
⊢ P ⊆ (𝒫 Q × 𝒫 Q)
Theorem	preqlu 7413	Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 = 𝐵 ↔ ((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵))))
Theorem	npex 7414	The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.)
⊢ P ∈ V
Theorem	elinp 7415*	Membership in positive reals. (Contributed by Jim Kingdon, 27-Sep-2019.)
⊢ (⟨𝐿, 𝑈⟩ ∈ P ↔ (((𝐿 ⊆ Q ∧ 𝑈 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝐿 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑈)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝐿)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑈))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝐿 ∧ 𝑞 ∈ 𝑈) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))))
Theorem	prop 7416	A positive real is an ordered pair of a lower cut and an upper cut. (Contributed by Jim Kingdon, 27-Sep-2019.)
⊢ (𝐴 ∈ P → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P)
Theorem	elnp1st2nd 7417*	Membership in positive reals, using 1st and 2nd to refer to the lower and upper cut. (Contributed by Jim Kingdon, 3-Oct-2019.)
⊢ (𝐴 ∈ P ↔ ((𝐴 ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐴) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐴))) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ (1st ‘𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐴))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐴) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐴)))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴)) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐴) ∨ 𝑟 ∈ (2nd ‘𝐴))))))
Theorem	prml 7418*	A positive real's lower cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝐿)
Theorem	prmu 7419*	A positive real's upper cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝑈)
Theorem	prssnql 7420	The lower cut of a positive real is a subset of the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
⊢ (⟨𝐿, 𝑈⟩ ∈ P → 𝐿 ⊆ Q)
Theorem	prssnqu 7421	The upper cut of a positive real is a subset of the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
⊢ (⟨𝐿, 𝑈⟩ ∈ P → 𝑈 ⊆ Q)
Theorem	elprnql 7422	An element of a positive real's lower cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q)
Theorem	elprnqu 7423	An element of a positive real's upper cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝑈) → 𝐵 ∈ Q)
Theorem	0npr 7424	The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.)
⊢ ¬ ∅ ∈ P
Theorem	prcdnql 7425	A lower cut is closed downwards under the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝐶 <Q 𝐵 → 𝐶 ∈ 𝐿))
Theorem	prcunqu 7426	An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q 𝐵 → 𝐵 ∈ 𝑈))
Theorem	prubl 7427	A positive fraction not in a lower cut is an upper bound. (Contributed by Jim Kingdon, 29-Sep-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) ∧ 𝐶 ∈ Q) → (¬ 𝐶 ∈ 𝐿 → 𝐵 <Q 𝐶))
Theorem	prltlu 7428	An element of a lower cut is less than an element of the corresponding upper cut. (Contributed by Jim Kingdon, 15-Oct-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿 ∧ 𝐶 ∈ 𝑈) → 𝐵 <Q 𝐶)
Theorem	prnmaxl 7429*	A lower cut has no largest member. (Contributed by Jim Kingdon, 29-Sep-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝐵 <Q 𝑥)
Theorem	prnminu 7430*	An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 𝑥 <Q 𝐵)
Theorem	prnmaddl 7431*	A lower cut has no largest member. Addition version. (Contributed by Jim Kingdon, 29-Sep-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ Q (𝐵 +Q 𝑥) ∈ 𝐿)
Theorem	prloc 7432	A Dedekind cut is located. (Contributed by Jim Kingdon, 23-Oct-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 <Q 𝐵) → (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈))
Theorem	prdisj 7433	A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ Q) → ¬ (𝐴 ∈ 𝐿 ∧ 𝐴 ∈ 𝑈))
Theorem	prarloclemlt 7434	Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 7444. (Contributed by Jim Kingdon, 10-Nov-2019.)
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +Q ([⟨(𝑦 +o 1o), 1o⟩] ~Q ·Q 𝑃)) <Q (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)))
Theorem	prarloclemlo 7435*	Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 7444. (Contributed by Jim Kingdon, 10-Nov-2019.)
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q ([⟨(𝑦 +o 1o), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝐿 → (((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))))
Theorem	prarloclemup 7436	Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7444. (Contributed by Jim Kingdon, 10-Nov-2019.)
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈 → (((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))))
Theorem	prarloclem3step 7437*	Induction step for prarloclem3 7438. (Contributed by Jim Kingdon, 9-Nov-2019.)
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
Theorem	prarloclem3 7438*	Contracting an interval which straddles a Dedekind cut. Lemma for prarloc 7444. (Contributed by Jim Kingdon, 27-Oct-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑋 ∈ ω ∧ 𝑃 ∈ Q) ∧ ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑗 ∈ ω ((𝐴 +Q0 ([⟨𝑗, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨(𝑗 +o 2o), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
Theorem	prarloclem4 7439*	A slight rearrangement of prarloclem3 7438. Lemma for prarloc 7444. (Contributed by Jim Kingdon, 4-Nov-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ 𝑃 ∈ Q) → (∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑥), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈ ω ((𝐴 +Q0 ([⟨𝑗, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨(𝑗 +o 2o), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)))
Theorem	prarloclemn 7440*	Subtracting two from a positive integer. Lemma for prarloc 7444. (Contributed by Jim Kingdon, 5-Nov-2019.)
⊢ ((𝑁 ∈ N ∧ 1o <N 𝑁) → ∃𝑥 ∈ ω (2o +o 𝑥) = 𝑁)
Theorem	prarloclem5 7441*	A substitution of zero for 𝑦 and 𝑁 minus two for 𝑥. Lemma for prarloc 7444. (Contributed by Jim Kingdon, 4-Nov-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1o <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑥), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
Theorem	prarloclem 7442*	A special case of Lemma 6.16 from [BauerTaylor], p. 32. Given evenly spaced rational numbers from 𝐴 to 𝐴 +Q (𝑁 ·Q 𝑃) (which are in the lower and upper cuts, respectively, of a real number), there are a pair of numbers, two positions apart in the even spacing, which straddle the cut. (Contributed by Jim Kingdon, 22-Oct-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1o <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈ ω ((𝐴 +Q0 ([⟨𝑗, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨(𝑗 +o 2o), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
Theorem	prarloclemcalc 7443	Some calculations for prarloc 7444. (Contributed by Jim Kingdon, 26-Oct-2019.)
⊢ (((𝐴 = (𝑋 +Q0 ([⟨𝑀, 1o⟩] ~Q0 ·Q0 𝑄)) ∧ 𝐵 = (𝑋 +Q ([⟨(𝑀 +o 2o), 1o⟩] ~Q ·Q 𝑄))) ∧ ((𝑄 ∈ Q ∧ (𝑄 +Q 𝑄) <Q 𝑃) ∧ (𝑋 ∈ Q ∧ 𝑀 ∈ ω))) → 𝐵 <Q (𝐴 +Q 𝑃))
Theorem	prarloc 7444*	A Dedekind cut is arithmetically located. Part of Proposition 11.15 of [BauerTaylor], p. 52, slightly modified. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are within that tolerance of each other. Usually, proofs will be shorter if they use prarloc2 7445 instead. (Contributed by Jim Kingdon, 22-Oct-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q 𝑃))
Theorem	prarloc2 7445*	A Dedekind cut is arithmetically located. This is a variation of prarloc 7444 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 (𝑎 +Q 𝑃) ∈ 𝑈)
Theorem	ltrelpr 7446	Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.)
⊢ <P ⊆ (P × P)
Theorem	ltdfpr 7447*	More convenient form of df-iltp 7411. (Contributed by Jim Kingdon, 15-Dec-2019.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<P 𝐵 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝐴) ∧ 𝑞 ∈ (1st ‘𝐵))))
Theorem	genpdflem 7448*	Simplification of upper or lower cut expression. Lemma for genpdf 7449. (Contributed by Jim Kingdon, 30-Sep-2019.)
⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q)    ⇒   ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)})
Theorem	genpdf 7449*	Simplified definition of addition or multiplication on positive reals. (Contributed by Jim Kingdon, 30-Sep-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑤) ∧ 𝑠 ∈ (1st ‘𝑣) ∧ 𝑞 = (𝑟𝐺𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑤) ∧ 𝑠 ∈ (2nd ‘𝑣) ∧ 𝑞 = (𝑟𝐺𝑠))}⟩)    ⇒   ⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1st ‘𝑤)∃𝑠 ∈ (1st ‘𝑣)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2nd ‘𝑤)∃𝑠 ∈ (2nd ‘𝑣)𝑞 = (𝑟𝐺𝑠)}⟩)
Theorem	genipv 7450*	Value of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingon, 3-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1st ‘𝐴)∃𝑠 ∈ (1st ‘𝐵)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2nd ‘𝐴)∃𝑠 ∈ (2nd ‘𝐵)𝑞 = (𝑟𝐺𝑠)}⟩)
Theorem	genplt2i 7451*	Operating on both sides of two inequalities, when the operation is consistent with <Q. (Contributed by Jim Kingdon, 6-Oct-2019.)
⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))    &   ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    ⇒   ⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 <Q 𝐷) → (𝐴𝐺𝐶) <Q (𝐵𝐺𝐷))
Theorem	genpelxp 7452*	Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) ∈ (𝒫 Q × 𝒫 Q))
Theorem	genpelvl 7453*	Membership in lower cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐶 ∈ (1st ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (1st ‘𝐴)∃ℎ ∈ (1st ‘𝐵)𝐶 = (𝑔𝐺ℎ)))
Theorem	genpelvu 7454*	Membership in upper cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 15-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐶 ∈ (2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ)))
Theorem	genpprecll 7455*	Pre-closure law for general operation on lower cuts. (Contributed by Jim Kingdon, 2-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐶 ∈ (1st ‘𝐴) ∧ 𝐷 ∈ (1st ‘𝐵)) → (𝐶𝐺𝐷) ∈ (1st ‘(𝐴𝐹𝐵))))
Theorem	genppreclu 7456*	Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐶 ∈ (2nd ‘𝐴) ∧ 𝐷 ∈ (2nd ‘𝐵)) → (𝐶𝐺𝐷) ∈ (2nd ‘(𝐴𝐹𝐵))))
Theorem	genipdm 7457*	Domain of general operation on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ dom 𝐹 = (P × P)
Theorem	genpml 7458*	The lower cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (1st ‘(𝐴𝐹𝐵)))
Theorem	genpmu 7459*	The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (2nd ‘(𝐴𝐹𝐵)))
Theorem	genpcdl 7460*	Downward closure of an operation on positive reals. (Contributed by Jim Kingdon, 14-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1st ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (1st ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔𝐺ℎ) → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝑓 ∈ (1st ‘(𝐴𝐹𝐵)) → (𝑥 <Q 𝑓 → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵)))))
Theorem	genpcuu 7461*	Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (2nd ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑔𝐺ℎ) <Q 𝑥 → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝑓 ∈ (2nd ‘(𝐴𝐹𝐵)) → (𝑓 <Q 𝑥 → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))))
Theorem	genprndl 7462*	The lower cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))    &   ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    &   ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1st ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (1st ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔𝐺ℎ) → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q (𝑞 ∈ (1st ‘(𝐴𝐹𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘(𝐴𝐹𝐵)))))
Theorem	genprndu 7463*	The upper cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))    &   ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    &   ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (2nd ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑔𝐺ℎ) <Q 𝑥 → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘(𝐴𝐹𝐵)))))
Theorem	genpdisj 7464*	The lower and upper cuts produced by addition or multiplication on positive reals are disjoint. (Contributed by Jim Kingdon, 15-Oct-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))    &   ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘(𝐴𝐹𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴𝐹𝐵))))
Theorem	genpassl 7465*	Associativity of lower cuts. Lemma for genpassg 7467. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ dom 𝐹 = (P × P)    &   ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P)    &   ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ)))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1st ‘(𝐴𝐹(𝐵𝐹𝐶))))
Theorem	genpassu 7466*	Associativity of upper cuts. Lemma for genpassg 7467. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ dom 𝐹 = (P × P)    &   ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P)    &   ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ)))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (2nd ‘((𝐴𝐹𝐵)𝐹𝐶)) = (2nd ‘(𝐴𝐹(𝐵𝐹𝐶))))
Theorem	genpassg 7467*	Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ dom 𝐹 = (P × P)    &   ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P)    &   ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ)))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))
Theorem	addnqprllem 7468	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <Q 𝑆 → ((𝑋 ·Q (*Q‘𝑆)) ·Q 𝐺) ∈ 𝐿))
Theorem	addnqprulem 7469	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <Q 𝑋 → ((𝑋 ·Q (*Q‘𝑆)) ·Q 𝐺) ∈ 𝑈))
Theorem	addnqprl 7470	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 7471	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 7472	Lemma for addlocpr 7477. 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 7473	Lemma for addlocpr 7477. 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 7474	Lemma for addlocpr 7477. 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 7475	Lemma for addlocpr 7477. 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 7476	Lemma for addlocpr 7477. 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 7477*	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 7444 to both 𝐴 and 𝐵, and uses nqtri3or 7337 rather than prloc 7432 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 7478	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 7479*	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 7480*	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 7481	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.)
⊢ dom +P = (P × P)
Theorem	dmmp 7482	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.)
⊢ dom ·P = (P × P)
Theorem	nqprm 7483*	A cut produced from a rational is inhabited. Lemma for nqprlu 7488. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → (∃𝑞 ∈ Q 𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))
Theorem	nqprrnd 7484*	A cut produced from a rational is rounded. Lemma for nqprlu 7488. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → (∀𝑞 ∈ Q (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) ∧ ∀𝑟 ∈ Q (𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥} ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))))
Theorem	nqprdisj 7485*	A cut produced from a rational is disjoint. Lemma for nqprlu 7488. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ¬ (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))
Theorem	nqprloc 7486*	A cut produced from a rational is located. Lemma for nqprlu 7488. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})))
Theorem	nqprxx 7487*	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 7488*	The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈ P)
Theorem	recnnpr 7489*	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 7490	The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {𝑥 ∣ 𝑥 <Q 𝐴} ∈ V
Theorem	gtnqex 7491	The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {𝑥 ∣ 𝐴 <Q 𝑥} ∈ V
Theorem	nqprl 7492*	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 7493*	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 7494*	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 7495	The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
⊢ 1P ∈ P
Theorem	1prl 7496	The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (1st ‘1P) = {𝑥 ∣ 𝑥 <Q 1Q}
Theorem	1pru 7497	The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (2nd ‘1P) = {𝑥 ∣ 1Q <Q 𝑥}
Theorem	addnqprlemrl 7498*	Lemma for addnqpr 7502. 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 7499*	Lemma for addnqpr 7502. 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 7500*	Lemma for addnqpr 7502. 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 𝑢}⟩)))