P. 99 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9801-9900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulclprlem 9801*	Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 14-Mar-1996.) (New usage is discouraged.)
⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔 ·Q ℎ) → 𝑥 ∈ (𝐴 ·P 𝐵)))
Theorem	mulclpr 9802	Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) ∈ P)
Theorem	addcompr 9803	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 +P 𝐵) = (𝐵 +P 𝐴)
Theorem	addasspr 9804	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 +P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P 𝐶))
Theorem	mulcompr 9805	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ·P 𝐵) = (𝐵 ·P 𝐴)
Theorem	mulasspr 9806	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ·P 𝐵) ·P 𝐶) = (𝐴 ·P (𝐵 ·P 𝐶))
Theorem	distrlem1pr 9807	Lemma for distributive law for positive reals. (Contributed by NM, 1-May-1996.) (Revised by Mario Carneiro, 13-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐴 ·P (𝐵 +P 𝐶)) ⊆ ((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶)))
Theorem	distrlem4pr 9808*	Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P 𝐶)))
Theorem	distrlem5pr 9809	Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶)) ⊆ (𝐴 ·P (𝐵 +P 𝐶)))
Theorem	distrpr 9810	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ·P (𝐵 +P 𝐶)) = ((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶))
Theorem	1idpr 9811	1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ P → (𝐴 ·P 1P) = 𝐴)
Theorem	ltprord 9812	Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<P 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	psslinpr 9813	Proper subset is a linear ordering on positive reals. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
Theorem	ltsopr 9814	Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
⊢ <P Or P
Theorem	prlem934 9815*	Lemma 9-3.4 of [Gleason] p. 122. (Contributed by NM, 25-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ P → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴)
Theorem	ltaddpr 9816	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.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → 𝐴<P (𝐴 +P 𝐵))
Theorem	ltaddpr2 9817	The sum of two positive reals is greater than one of them. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ P → ((𝐴 +P 𝐵) = 𝐶 → 𝐴<P 𝐶))
Theorem	ltexprlem1 9818*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → (𝐴 ⊊ 𝐵 → 𝐶 ≠ ∅))
Theorem	ltexprlem2 9819*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → 𝐶 ⊊ Q)
Theorem	ltexprlem3 9820*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → (𝑥 ∈ 𝐶 → ∀𝑧(𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶)))
Theorem	ltexprlem4 9821*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → (𝑥 ∈ 𝐶 → ∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧)))
Theorem	ltexprlem5 9822*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ ((𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵) → 𝐶 ∈ P)
Theorem	ltexprlem6 9823*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ 𝐴 ⊊ 𝐵) → (𝐴 +P 𝐶) ⊆ 𝐵)
Theorem	ltexprlem7 9824*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ 𝐴 ⊊ 𝐵) → 𝐵 ⊆ (𝐴 +P 𝐶))
Theorem	ltexpri 9825*	Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ (𝐴<P 𝐵 → ∃𝑥 ∈ P (𝐴 +P 𝑥) = 𝐵)
Theorem	ltaprlem 9826	Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
Theorem	ltapr 9827	Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ P → (𝐴<P 𝐵 ↔ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
Theorem	addcanpr 9828	Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by NM, 9-Apr-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐴 +P 𝐵) = (𝐴 +P 𝐶) → 𝐵 = 𝐶))
Theorem	prlem936 9829*	Lemma 9-3.6 of [Gleason] p. 124. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 1Q <Q 𝐵) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝐵) ∈ 𝐴)
Theorem	reclem2pr 9830*	Lemma for Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬ (*Q‘𝑦) ∈ 𝐴)}    ⇒   ⊢ (𝐴 ∈ P → 𝐵 ∈ P)
Theorem	reclem3pr 9831*	Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬ (*Q‘𝑦) ∈ 𝐴)}    ⇒   ⊢ (𝐴 ∈ P → 1P ⊆ (𝐴 ·P 𝐵))
Theorem	reclem4pr 9832*	Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬ (*Q‘𝑦) ∈ 𝐴)}    ⇒   ⊢ (𝐴 ∈ P → (𝐴 ·P 𝐵) = 1P)
Theorem	recexpr 9833*	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.) (New usage is discouraged.)
⊢ (𝐴 ∈ P → ∃𝑥 ∈ P (𝐴 ·P 𝑥) = 1P)
Theorem	suplem1pr 9834*	The union of a nonempty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∪ 𝐴 ∈ P)
Theorem	suplem2pr 9835*	The union of a set of positive reals (if a positive real) is its supremum (the least upper bound). Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ (𝐴 ⊆ P → ((𝑦 ∈ 𝐴 → ¬ ∪ 𝐴<P 𝑦) ∧ (𝑦<P ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
Theorem	supexpr 9836*	The union of a nonempty, bounded set of positive reals has a supremum. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∃𝑥 ∈ P (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
Definition	df-enr 9837*	Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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.) (New usage is discouraged.)
⊢ ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
Definition	df-nr 9838	Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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.) (New usage is discouraged.)
⊢ R = ((P × P) / ~R )
Definition	df-plr 9839*	Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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.) (New usage is discouraged.)
⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
Definition	df-mr 9840*	Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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.) (New usage is discouraged.)
⊢ ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
Definition	df-ltr 9841*	Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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.) (New usage is discouraged.)
⊢ <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
Definition	df-0r 9842	Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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.) (New usage is discouraged.)
⊢ 0R = [⟨1P, 1P⟩] ~R
Definition	df-1r 9843	Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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.) (New usage is discouraged.)
⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
Definition	df-m1r 9844	Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 9902, and is intended to be used only by the construction. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
Theorem	enrbreq 9845	Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → (⟨𝐴, 𝐵⟩ ~R ⟨𝐶, 𝐷⟩ ↔ (𝐴 +P 𝐷) = (𝐵 +P 𝐶)))
Theorem	enrer 9846	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.) (New usage is discouraged.)
⊢ ~R Er (P × P)
Theorem	enreceq 9847	Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ↔ (𝐴 +P 𝐷) = (𝐵 +P 𝐶)))
Theorem	enrex 9848	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
⊢ ~R ∈ V
Theorem	ltrelsr 9849	Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
⊢ <R ⊆ (R × R)
Theorem	addcmpblnr 9850	Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨(𝐴 +P 𝐹), (𝐵 +P 𝐺)⟩ ~R ⟨(𝐶 +P 𝑅), (𝐷 +P 𝑆)⟩))
Theorem	mulcmpblnrlem 9851	Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995.) (New usage is discouraged.)
⊢ (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))))
Theorem	mulcmpblnr 9852	Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.) (New usage is discouraged.)
⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)), ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩))
Theorem	prsrlem1 9853*	Decomposing signed reals into positive reals. Lemma for addsrpr 9856 and mulsrpr 9857. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ (((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) ∧ ((𝐴 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝐵 = [⟨𝑢, 𝑡⟩] ~R ) ∧ (𝐴 = [⟨𝑠, 𝑓⟩] ~R ∧ 𝐵 = [⟨𝑔, ℎ⟩] ~R ))) → ((((𝑤 ∈ P ∧ 𝑣 ∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧ ((𝑢 ∈ P ∧ 𝑡 ∈ P) ∧ (𝑔 ∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P 𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔))))
Theorem	addsrmo 9854*	There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝐵 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
Theorem	mulsrmo 9855*	There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝐵 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))⟩] ~R ))
Theorem	addsrpr 9856	Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
Theorem	mulsrpr 9857	Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R ·R [⟨𝐶, 𝐷⟩] ~R ) = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R )
Theorem	ltsrpr 9858	Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
⊢ ([⟨𝐴, 𝐵⟩] ~R <R [⟨𝐶, 𝐷⟩] ~R ↔ (𝐴 +P 𝐷)<P (𝐵 +P 𝐶))
Theorem	gt0srpr 9859	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (0R <R [⟨𝐴, 𝐵⟩] ~R ↔ 𝐵<P 𝐴)
Theorem	0nsr 9860	The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ R
Theorem	0r 9861	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
⊢ 0R ∈ R
Theorem	1sr 9862	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
⊢ 1R ∈ R
Theorem	m1r 9863	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
⊢ -1R ∈ R
Theorem	addclsr 9864	Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) ∈ R)
Theorem	mulclsr 9865	Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) ∈ R)
Theorem	dmaddsr 9866	Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
⊢ dom +R = (R × R)
Theorem	dmmulsr 9867	Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
⊢ dom ·R = (R × R)
Theorem	addcomsr 9868	Addition of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ (𝐴 +R 𝐵) = (𝐵 +R 𝐴)
Theorem	addasssr 9869	Addition of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ ((𝐴 +R 𝐵) +R 𝐶) = (𝐴 +R (𝐵 +R 𝐶))
Theorem	mulcomsr 9870	Multiplication of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ (𝐴 ·R 𝐵) = (𝐵 ·R 𝐴)
Theorem	mulasssr 9871	Multiplication of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ ((𝐴 ·R 𝐵) ·R 𝐶) = (𝐴 ·R (𝐵 ·R 𝐶))
Theorem	distrsr 9872	Multiplication of signed reals is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ (𝐴 ·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R (𝐴 ·R 𝐶))
Theorem	m1p1sr 9873	Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
⊢ (-1R +R 1R) = 0R
Theorem	m1m1sr 9874	Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
⊢ (-1R ·R -1R) = 1R
Theorem	ltsosr 9875	Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.) (New usage is discouraged.)
⊢ <R Or R
Theorem	0lt1sr 9876	0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.)
⊢ 0R <R 1R
Theorem	1ne0sr 9877	1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.)
⊢ ¬ 1R = 0R
Theorem	0idsr 9878	The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ R → (𝐴 +R 0R) = 𝐴)
Theorem	1idsr 9879	1 is an identity element for multiplication. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ R → (𝐴 ·R 1R) = 𝐴)
Theorem	00sr 9880	A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ R → (𝐴 ·R 0R) = 0R)
Theorem	ltasr 9881	Ordering property of addition. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ R → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
Theorem	pn0sr 9882	A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ R → (𝐴 +R (𝐴 ·R -1R)) = 0R)
Theorem	negexsr 9883*	Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ R → ∃𝑥 ∈ R (𝐴 +R 𝑥) = 0R)
Theorem	recexsrlem 9884*	The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ (0R <R 𝐴 → ∃𝑥 ∈ R (𝐴 ·R 𝑥) = 1R)
Theorem	addgt0sr 9885	The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵))
Theorem	mulgt0sr 9886	The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 ·R 𝐵))
Theorem	sqgt0sr 9887	The square of a nonzero signed real is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ R ∧ 𝐴 ≠ 0R) → 0R <R (𝐴 ·R 𝐴))
Theorem	recexsr 9888*	The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ R ∧ 𝐴 ≠ 0R) → ∃𝑥 ∈ R (𝐴 ·R 𝑥) = 1R)
Theorem	mappsrpr 9889	Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
⊢ 𝐶 ∈ R    ⇒   ⊢ ((𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ) ↔ 𝐴 ∈ P)
Theorem	ltpsrpr 9890	Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
⊢ 𝐶 ∈ R    ⇒   ⊢ ((𝐶 +R [⟨𝐴, 1P⟩] ~R ) <R (𝐶 +R [⟨𝐵, 1P⟩] ~R ) ↔ 𝐴<P 𝐵)
Theorem	map2psrpr 9891*	Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
⊢ 𝐶 ∈ R    ⇒   ⊢ ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
Theorem	supsrlem 9892*	Lemma for supremum theorem. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
⊢ 𝐵 = {𝑤 ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   ⊢ 𝐶 ∈ R    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
Theorem	supsr 9893*	A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
Syntax	cc 9894	Class of complex numbers.
class ℂ
Syntax	cr 9895	Class of real numbers.
class ℝ
Syntax	cc0 9896	Extend class notation to include the complex number 0.
class 0
Syntax	c1 9897	Extend class notation to include the complex number 1.
class 1
Syntax	ci 9898	Extend class notation to include the complex number i.
class i
Syntax	caddc 9899	Addition on complex numbers.
class +
Syntax	cltrr 9900	'Less than' predicate (defined over real subset of complex numbers).
class <ℝ