P. 65 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6401-6500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nqprlu 6401*	The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ (A ∈ Q → ⟨{x ∣ x <Q A}, {x ∣ A <Q x}⟩ ∈ P)
Theorem	ltnqex 6402	The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {x ∣ x <Q A} ∈ V
Theorem	gtnqex 6403	The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {x ∣ A <Q x} ∈ V
Theorem	1pr 6404	The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
⊢ 1P ∈ P
Theorem	1prl 6405	The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (1st ‘1P) = {x ∣ x <Q 1Q}
Theorem	1pru 6406	The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (2nd ‘1P) = {x ∣ 1Q <Q x}
Theorem	appdivnq 6407*	Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where A and B 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.)
⊢ ((A <Q B ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q (A <Q (𝑚 ·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q B))
Theorem	appdiv0nq 6408*	Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6407 in which A 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.)
⊢ ((B ∈ Q ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q (𝑚 ·Q 𝐶) <Q B)
Theorem	prmuloclemcalc 6409	Calculations for prmuloc 6410. (Contributed by Jim Kingdon, 9-Dec-2019.)
⊢ (φ → 𝑅 <Q 𝑈)    &   ⊢ (φ → 𝑈 <Q (𝐷 +Q 𝑃))    &   ⊢ (φ → (A +Q 𝑋) = B)    &   ⊢ (φ → (𝑃 ·Q B) <Q (𝑅 ·Q 𝑋))    &   ⊢ (φ → A ∈ Q)    &   ⊢ (φ → B ∈ Q)    &   ⊢ (φ → 𝐷 ∈ Q)    &   ⊢ (φ → 𝑃 ∈ Q)    &   ⊢ (φ → 𝑋 ∈ Q)    ⇒   ⊢ (φ → (𝑈 ·Q A) <Q (𝐷 ·Q B))
Theorem	prmuloc 6410*	Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ A <Q B) → ∃𝑑 ∈ Q ∃u ∈ Q (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧ (u ·Q A) <Q (𝑑 ·Q B)))
Theorem	prmuloc2 6411*	Positive reals are multiplicatively located. This is a variation of prmuloc 6410 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio B, 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 B) → ∃x ∈ 𝐿 (x ·Q B) ∈ 𝑈)
Theorem	mulnqprl 6412	Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
⊢ ((((A ∈ P ∧ 𝐺 ∈ (1st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 <Q (𝐺 ·Q 𝐻) → 𝑋 ∈ (1st ‘(A ·P B))))
Theorem	mulnqpru 6413	Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
⊢ ((((A ∈ P ∧ 𝐺 ∈ (2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (2nd ‘B))) ∧ 𝑋 ∈ Q) → ((𝐺 ·Q 𝐻) <Q 𝑋 → 𝑋 ∈ (2nd ‘(A ·P B))))
Theorem	mullocprlem 6414	Calculations for mullocpr 6415. (Contributed by Jim Kingdon, 10-Dec-2019.)
⊢ (φ → (A ∈ P ∧ B ∈ P))    &   ⊢ (φ → (𝑈 ·Q 𝑄) <Q (𝐸 ·Q (𝐷 ·Q 𝑈)))    &   ⊢ (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈)))    &   ⊢ (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅))    &   ⊢ (φ → (𝑄 ∈ Q ∧ 𝑅 ∈ Q))    &   ⊢ (φ → (𝐷 ∈ Q ∧ 𝑈 ∈ Q))    &   ⊢ (φ → (𝐷 ∈ (1st ‘A) ∧ 𝑈 ∈ (2nd ‘A)))    &   ⊢ (φ → (𝐸 ∈ Q ∧ 𝑇 ∈ Q))    ⇒   ⊢ (φ → (𝑄 ∈ (1st ‘(A ·P B)) ∨ 𝑅 ∈ (2nd ‘(A ·P B))))
Theorem	mullocpr 6415*	Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both A and B are positive, not just A). (Contributed by Jim Kingdon, 8-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(A ·P B)) ∨ 𝑟 ∈ (2nd ‘(A ·P B)))))
Theorem	mulclpr 6416	Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.)
⊢ ((A ∈ P ∧ B ∈ P) → (A ·P B) ∈ P)
Theorem	addcomprg 6417	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P) → (A +P B) = (B +P A))
Theorem	addassprg 6418	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → ((A +P B) +P 𝐶) = (A +P (B +P 𝐶)))
Theorem	mulcomprg 6419	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P) → (A ·P B) = (B ·P A))
Theorem	mulassprg 6420	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → ((A ·P B) ·P 𝐶) = (A ·P (B ·P 𝐶)))
Theorem	distrlem1prl 6421	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (1st ‘(A ·P (B +P 𝐶))) ⊆ (1st ‘((A ·P B) +P (A ·P 𝐶))))
Theorem	distrlem1pru 6422	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (2nd ‘(A ·P (B +P 𝐶))) ⊆ (2nd ‘((A ·P B) +P (A ·P 𝐶))))
Theorem	distrlem4prl 6423*	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈ (1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((x ·Q y) +Q (f ·Q z)) ∈ (1st ‘(A ·P (B +P 𝐶))))
Theorem	distrlem4pru 6424*	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (2nd ‘A) ∧ y ∈ (2nd ‘B)) ∧ (f ∈ (2nd ‘A) ∧ z ∈ (2nd ‘𝐶)))) → ((x ·Q y) +Q (f ·Q z)) ∈ (2nd ‘(A ·P (B +P 𝐶))))
Theorem	distrlem5prl 6425	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (1st ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (1st ‘(A ·P (B +P 𝐶))))
Theorem	distrlem5pru 6426	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (2nd ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (2nd ‘(A ·P (B +P 𝐶))))
Theorem	distrprg 6427	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (A ·P (B +P 𝐶)) = ((A ·P B) +P (A ·P 𝐶)))
Theorem	ltprordil 6428	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.)
⊢ (A<P B → (1st ‘A) ⊆ (1st ‘B))
Theorem	1idprl 6429	Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ (A ∈ P → (1st ‘(A ·P 1P)) = (1st ‘A))
Theorem	1idpru 6430	Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ (A ∈ P → (2nd ‘(A ·P 1P)) = (2nd ‘A))
Theorem	1idpr 6431	1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.)
⊢ (A ∈ P → (A ·P 1P) = A)
Theorem	ltpopr 6432	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 6433. (Contributed by Jim Kingdon, 15-Dec-2019.)
⊢ <P Po P
Theorem	ltsopr 6433	Positive real 'less than' is a weak linear order (in the sense of df-iso 4008). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
⊢ <P Or P
Theorem	ltaddpr 6434	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.)
⊢ ((A ∈ P ∧ B ∈ P) → A<P (A +P B))
Theorem	ltexprlemell 6435*	Element in lower cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
Theorem	ltexprlemelu 6436*	Element in upper cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))))
Theorem	ltexprlemm 6437*	Our constructed difference is inhabited. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemopl 6438*	The lower cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)))
Theorem	ltexprlemlol 6439*	The lower cut of our constructed difference is lower. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)) → 𝑞 ∈ (1st ‘𝐶)))
Theorem	ltexprlemopu 6440*	The upper cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemupu 6441*	The upper cut of our constructed difference is upper. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) → 𝑟 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemrnd 6442*	Our constructed difference is rounded. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐶) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))))
Theorem	ltexprlemdisj 6443*	Our constructed difference is disjoint. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐶) ∧ 𝑞 ∈ (2nd ‘𝐶)))
Theorem	ltexprlemloc 6444*	Our constructed difference is located. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))
Theorem	ltexprlempr 6445*	Our constructed difference is a positive real. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → 𝐶 ∈ P)
Theorem	ltexprlemfl 6446*	Lemma for ltexpri 6450. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (1st ‘(A +P 𝐶)) ⊆ (1st ‘B))
Theorem	ltexprlemrl 6447*	Lemma for ltexpri 6450. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (1st ‘B) ⊆ (1st ‘(A +P 𝐶)))
Theorem	ltexprlemfu 6448*	Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (2nd ‘(A +P 𝐶)) ⊆ (2nd ‘B))
Theorem	ltexprlemru 6449*	Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (2nd ‘B) ⊆ (2nd ‘(A +P 𝐶)))
Theorem	ltexpri 6450*	Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.)
⊢ (A<P B → ∃x ∈ P (A +P x) = B)
Theorem	addcanprleml 6451	Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ (A +P B) = (A +P 𝐶)) → (1st ‘B) ⊆ (1st ‘𝐶))
Theorem	addcanprlemu 6452	Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ (A +P B) = (A +P 𝐶)) → (2nd ‘B) ⊆ (2nd ‘𝐶))
Theorem	addcanprg 6453	Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → ((A +P B) = (A +P 𝐶) → B = 𝐶))
Theorem	ltaprlem 6454	Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.)
⊢ (𝐶 ∈ P → (A<P B → (𝐶 +P A)<P (𝐶 +P B)))
Theorem	ltaprg 6455	Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. Part of Definition 11.2.7(vi) of [HoTT]], p. (varies). (Contributed by Jim Kingdon, 26-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (A<P B ↔ (𝐶 +P A)<P (𝐶 +P B)))
Theorem	recexprlemell 6456*	Membership in the lower cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (𝐶 ∈ (1st ‘B) ↔ ∃y(𝐶 <Q y ∧ (*Q‘y) ∈ (2nd ‘A)))
Theorem	recexprlemelu 6457*	Membership in the upper cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (𝐶 ∈ (2nd ‘B) ↔ ∃y(y <Q 𝐶 ∧ (*Q‘y) ∈ (1st ‘A)))
Theorem	recexprlemm 6458*	B is inhabited. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘B) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘B)))
Theorem	recexprlemopl 6459*	The lower cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘B)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘B)))
Theorem	recexprlemlol 6460*	The lower cut of B is lower. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘B)) → 𝑞 ∈ (1st ‘B)))
Theorem	recexprlemopu 6461*	The upper cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘B)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘B)))
Theorem	recexprlemupu 6462*	The upper cut of B is upper. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘B)) → 𝑟 ∈ (2nd ‘B)))
Theorem	recexprlemrnd 6463*	B is rounded. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘B))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘B) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘B)))))
Theorem	recexprlemdisj 6464*	B is disjoint. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)))
Theorem	recexprlemloc 6465*	B is located. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘B) ∨ 𝑟 ∈ (2nd ‘B))))
Theorem	recexprlempr 6466*	B is a positive real. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → B ∈ P)
Theorem	recexprlem1ssl 6467*	The lower cut of one is a subset of the lower cut of A ·P B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))
Theorem	recexprlem1ssu 6468*	The upper cut of one is a subset of the upper cut of A ·P B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
Theorem	recexprlemss1l 6469*	The lower cut of A ·P B is a subset of the lower cut of one. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))
Theorem	recexprlemss1u 6470*	The upper cut of A ·P B is a subset of the upper cut of one. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))
Theorem	recexprlemex 6471*	B is the reciprocal of A. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (A ·P B) = 1P)
Theorem	recexpr 6472*	The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
⊢ (A ∈ P → ∃x ∈ P (A ·P x) = 1P)
Definition	df-enr 6473*	Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
⊢ ~R = {⟨x, y⟩ ∣ ((x ∈ (P × P) ∧ y ∈ (P × P)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z +P u) = (w +P v)))}
Definition	df-nr 6474	Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
⊢ R = ((P × P) / ~R )
Definition	df-plr 6475*	Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
⊢ +R = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~R ∧ y = [⟨u, f⟩] ~R ) ∧ z = [⟨(w +P u), (v +P f)⟩] ~R ))}
Definition	df-mr 6476*	Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
⊢ ·R = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~R ∧ y = [⟨u, f⟩] ~R ) ∧ z = [⟨((w ·P u) +P (v ·P f)), ((w ·P f) +P (v ·P u))⟩] ~R ))}
Definition	df-ltr 6477*	Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.)
⊢ <R = {⟨x, y⟩ ∣ ((x ∈ R ∧ y ∈ R) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩] ~R ∧ y = [⟨v, u⟩] ~R ) ∧ (z +P u)<P (w +P v)))}
Definition	df-0r 6478	Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
⊢ 0R = [⟨1P, 1P⟩] ~R
Definition	df-1r 6479	Define signed 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. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
Definition	df-m1r 6480	Define signed 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 NM, 9-Aug-1995.)
⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
Theorem	enrbreq 6481	Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.)
⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → (⟨A, B⟩ ~R ⟨𝐶, 𝐷⟩ ↔ (A +P 𝐷) = (B +P 𝐶)))
Theorem	enrer 6482	The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
⊢ ~R Er (P × P)
Theorem	enreceq 6483	Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)
⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨A, B⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ↔ (A +P 𝐷) = (B +P 𝐶)))
Theorem	enrex 6484	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.)
⊢ ~R ∈ V
Theorem	ltrelsr 6485	Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.)
⊢ <R ⊆ (R × R)
Theorem	addcmpblnr 6486	Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.)
⊢ ((((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((A +P 𝐷) = (B +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨(A +P 𝐹), (B +P 𝐺)⟩ ~R ⟨(𝐶 +P 𝑅), (𝐷 +P 𝑆)⟩))
Theorem	mulcmpblnrlemg 6487	Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
⊢ ((((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((A +P 𝐷) = (B +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((A ·P 𝐹) +P (B ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((A ·P 𝐺) +P (B ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆))))))
Theorem	mulcmpblnr 6488	Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.)
⊢ ((((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((A +P 𝐷) = (B +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨((A ·P 𝐹) +P (B ·P 𝐺)), ((A ·P 𝐺) +P (B ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩))
Theorem	prsrlem1 6489*	Decomposing signed reals into positive reals. Lemma for addsrpr 6492 and mulsrpr 6493. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ (((A ∈ ((P × P) / ~R ) ∧ B ∈ ((P × P) / ~R )) ∧ ((A = [⟨w, v⟩] ~R ∧ B = [⟨u, 𝑡⟩] ~R ) ∧ (A = [⟨𝑠, f⟩] ~R ∧ B = [⟨g, ℎ⟩] ~R ))) → ((((w ∈ P ∧ v ∈ P) ∧ (𝑠 ∈ P ∧ f ∈ P)) ∧ ((u ∈ P ∧ 𝑡 ∈ P) ∧ (g ∈ P ∧ ℎ ∈ P))) ∧ ((w +P f) = (v +P 𝑠) ∧ (u +P ℎ) = (𝑡 +P g))))
Theorem	addsrmo 6490*	There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((A ∈ ((P × P) / ~R ) ∧ B ∈ ((P × P) / ~R )) → ∃*z∃w∃v∃u∃𝑡((A = [⟨w, v⟩] ~R ∧ B = [⟨u, 𝑡⟩] ~R ) ∧ z = [⟨(w +P u), (v +P 𝑡)⟩] ~R ))
Theorem	mulsrmo 6491*	There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((A ∈ ((P × P) / ~R ) ∧ B ∈ ((P × P) / ~R )) → ∃*z∃w∃v∃u∃𝑡((A = [⟨w, v⟩] ~R ∧ B = [⟨u, 𝑡⟩] ~R ) ∧ z = [⟨((w ·P u) +P (v ·P 𝑡)), ((w ·P 𝑡) +P (v ·P u))⟩] ~R ))
Theorem	addsrpr 6492	Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨A, B⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(A +P 𝐶), (B +P 𝐷)⟩] ~R )
Theorem	mulsrpr 6493	Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨A, B⟩] ~R ·R [⟨𝐶, 𝐷⟩] ~R ) = [⟨((A ·P 𝐶) +P (B ·P 𝐷)), ((A ·P 𝐷) +P (B ·P 𝐶))⟩] ~R )
Theorem	ltsrprg 6494	Ordering of signed reals in terms of positive reals. (Contributed by Jim Kingdon, 2-Jan-2019.)
⊢ (((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨A, B⟩] ~R <R [⟨𝐶, 𝐷⟩] ~R ↔ (A +P 𝐷)<P (B +P 𝐶)))
Theorem	gt0srpr 6495	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.)
⊢ (0R <R [⟨A, B⟩] ~R ↔ B<P A)
Theorem	0nsr 6496	The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.)
⊢ ¬ ∅ ∈ R
Theorem	0r 6497	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 0R ∈ R
Theorem	1sr 6498	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 1R ∈ R
Theorem	m1r 6499	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ -1R ∈ R
Theorem	addclsr 6500	Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.)
⊢ ((A ∈ R ∧ B ∈ R) → (A +R B) ∈ R)