P. 112 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11101-11200   *Has distinct variable group(s)

Type	Label	Description
Statement
Axiom	ax-addass 11101	Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by Theorem axaddass 11077. Proofs should normally use addass 11123 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Axiom	ax-mulass 11102	Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by Theorem axmulass 11078. Proofs should normally use mulass 11124 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Axiom	ax-distr 11103	Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by Theorem axdistr 11079. Proofs should normally use adddi 11125 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Axiom	ax-i2m1 11104	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, justified by Theorem axi2m1 11080. (Contributed by NM, 29-Jan-1995.)
⊢ ((i · i) + 1) = 0
Axiom	ax-1ne0 11105	1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 11081. (Contributed by NM, 29-Jan-1995.)
⊢ 1 ≠ 0
Axiom	ax-1rid 11106	1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11082. Weakened from the original axiom in the form of statement in mulrid 11140, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Axiom	ax-rnegex 11107*	Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by Theorem axrnegex 11083. (Contributed by Eric Schmidt, 21-May-2007.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Axiom	ax-rrecex 11108*	Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by Theorem axrrecex 11084. (Contributed by Eric Schmidt, 11-Apr-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Axiom	ax-cnre 11109*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, justified by Theorem axcnre 11085. For naming consistency, use cnre 11139 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Axiom	ax-pre-lttri 11110	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by Theorem axpre-lttri 11086. Note: The more general version for extended reals is axlttri 11215. Normally new proofs would use xrlttri 13088. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Axiom	ax-pre-lttrn 11111	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by Theorem axpre-lttrn 11087. Note: The more general version for extended reals is axlttrn 11216. Normally new proofs would use lttr 11220. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Axiom	ax-pre-ltadd 11112	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by Theorem axpre-ltadd 11088. Normally new proofs would use axltadd 11217. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Axiom	ax-pre-mulgt0 11113	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by Theorem axpre-mulgt0 11089. Normally new proofs would use axmulgt0 11218. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Axiom	ax-pre-sup 11114*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup 11090. Note: Normally new proofs would use axsup 11219. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
Axiom	ax-addf 11115	Addition is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first-order or second-order statement (see https://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific addcl 11118 should be used. Note that uses of ax-addf 11115 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) in place of +, from which this axiom (with the defined operation in place of +) follows as a theorem. This axiom is justified by Theorem axaddf 11066. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ + :(ℂ × ℂ)⟶ℂ
Axiom	ax-mulf 11116	Multiplication is an operation on the complex numbers. This axiom tells us that · is defined only on complex numbers which is analogous to the way that other operations are defined, for example see subf 11393 or eff 16044. However, while Metamath can handle this axiom, if we wish to work with weaker complex number axioms, we can avoid it by using the less specific mulcl 11120. Note that uses of ax-mulf 11116 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11131. This axiom is justified by Theorem axmulf 11067. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ · :(ℂ × ℂ)⟶ℂ
5.2  Derive the basic properties from the field axioms
5.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 11117	Alias for ax-cnex 11092. See also cnexALT 12934. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℂ ∈ V
Theorem	addcl 11118	Alias for ax-addcl 11096, for naming consistency with addcli 11149. Use this theorem instead of ax-addcl 11096 or axaddcl 11072. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	readdcl 11119	Alias for ax-addrcl 11097, for naming consistency with readdcli 11158. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	mulcl 11120	Alias for ax-mulcl 11098, for naming consistency with mulcli 11150. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	remulcl 11121	Alias for ax-mulrcl 11099, for naming consistency with remulcli 11159. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	mulcom 11122	Alias for ax-mulcom 11100, for naming consistency with mulcomi 11151. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addass 11123	Alias for ax-addass 11101, for naming consistency with addassi 11153. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulass 11124	Alias for ax-mulass 11102, for naming consistency with mulassi 11154. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddi 11125	Alias for ax-distr 11103, for naming consistency with adddii 11155. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	recn 11126	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Theorem	reex 11127	The real numbers form a set. See also reexALT 12932. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℝ ∈ V
Theorem	reelprrecn 11128	Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℝ ∈ {ℝ, ℂ}
Theorem	cnelprrecn 11129	Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℂ ∈ {ℝ, ℂ}
Theorem	mpoaddf 11130*	Addition is an operation on complex numbers. Version of ax-addf 11115 using maps-to notation, proved from the axioms of set theory and ax-addcl 11096. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	mpomulf 11131*	Multiplication is an operation on complex numbers. Version of ax-mulf 11116 using maps-to notation, proved from the axioms of set theory and ax-mulcl 11098. (Contributed by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	elimne0 11132	Hypothesis for weak deduction theorem to eliminate 𝐴 ≠ 0. (Contributed by NM, 15-May-1999.)
⊢ if(𝐴 ≠ 0, 𝐴, 1) ≠ 0
Theorem	adddir 11133	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	0cn 11134	Zero is a complex number. See also 0cnALT 11379. (Contributed by NM, 19-Feb-2005.)
⊢ 0 ∈ ℂ
Theorem	0cnd 11135	Zero is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℂ)
Theorem	c0ex 11136	Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ∈ V
Theorem	1cnd 11137	One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℂ)
Theorem	1ex 11138	One is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 1 ∈ V
Theorem	cnre 11139*	Alias for ax-cnre 11109, for naming consistency. (Contributed by NM, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	mulrid 11140	The number 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Theorem	mullid 11141	Identity law for multiplication. See mulrid 11140 for commuted version. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	1re 11142	The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 11094, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ 1 ∈ ℝ
Theorem	1red 11143	The number 1 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℝ)
Theorem	0re 11144	The number 0 is real. Remark: the first step could also be ax-icn 11095. See also 0reALT 11489. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022.)
⊢ 0 ∈ ℝ
Theorem	0red 11145	The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℝ)
Theorem	pr01ssre 11146	The pair {0, 1} is a subset of ℝ. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ {0, 1} ⊆ ℝ
Theorem	mulridi 11147	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 1) = 𝐴
Theorem	mullidi 11148	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (1 · 𝐴) = 𝐴
Theorem	addcli 11149	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℂ
Theorem	mulcli 11150	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℂ
Theorem	mulcomi 11151	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	mulcomli 11152	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ (𝐵 · 𝐴) = 𝐶
Theorem	addassi 11153	Associative law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	mulassi 11154	Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	adddii 11155	Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Theorem	adddiri 11156	Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))
Theorem	recni 11157	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℂ
Theorem	readdcli 11158	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℝ
Theorem	remulcli 11159	Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℝ
Theorem	mulridd 11160	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐴)
Theorem	mullidd 11161	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	addcld 11162	Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Theorem	mulcld 11163	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Theorem	mulcomd 11164	Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addassd 11165	Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulassd 11166	Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddid 11167	Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	adddird 11168	Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	adddirp1d 11169	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
Theorem	joinlmuladdmuld 11170	Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
Theorem	recnd 11171	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	readdcld 11172	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Theorem	remulcld 11173	Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
5.2.2  Infinity and the extended real number system
Syntax	cpnf 11174	Plus infinity.
class +∞
Syntax	cmnf 11175	Minus infinity.
class -∞
Syntax	cxr 11176	The set of extended reals (includes plus and minus infinity).
class ℝ*
Syntax	clt 11177	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 11178	Extend wff notation to include the 'less than or equal to' relation.
class ≤
Definition	df-pnf 11179	Define plus infinity. Note that the definition is arbitrary, requiring only that +∞ be a set not in ℝ and different from -∞ (df-mnf 11180). We use 𝒫 ∪ ℂ to make it independent of the construction of ℂ, and Cantor's Theorem will show that it is different from any member of ℂ and therefore ℝ. See pnfnre 11184, mnfnre 11186, and pnfnemnf 11198. A simpler possibility is to define +∞ as ℂ and -∞ as {ℂ}, but that approach requires the Axiom of Regularity to show that +∞ and -∞ are different from each other and from all members of ℝ. (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
⊢ +∞ = 𝒫 ∪ ℂ
Definition	df-mnf 11180	Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -∞ be a set not in ℝ and different from +∞ (see mnfnre 11186 and pnfnemnf 11198). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
⊢ -∞ = 𝒫 +∞
Definition	df-xr 11181	Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.)
⊢ ℝ* = (ℝ ∪ {+∞, -∞})
Definition	df-ltxr 11182*	Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, <ℝ is primitive and not necessarily a relation on ℝ. (Contributed by NM, 13-Oct-2005.)
⊢ < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
Definition	df-le 11183	Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 11230 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.)
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
Theorem	pnfnre 11184	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ +∞ ∉ ℝ
Theorem	pnfnre2 11185	Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ¬ +∞ ∈ ℝ
Theorem	mnfnre 11186	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ -∞ ∉ ℝ
Theorem	ressxr 11187	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ℝ ⊆ ℝ*
Theorem	rexpssxrxp 11188	The Cartesian product of standard reals are a subset of the Cartesian product of extended reals. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
Theorem	rexr 11189	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
Theorem	0xr 11190	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 0 ∈ ℝ*
Theorem	renepnf 11191	No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Theorem	renemnf 11192	No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
Theorem	rexrd 11193	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	renepnfd 11194	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ +∞)
Theorem	renemnfd 11195	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ -∞)
Theorem	pnfex 11196	Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.) (Revised by Steven Nguyen, 7-Dec-2022.)
⊢ +∞ ∈ V
Theorem	pnfxr 11197	Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
⊢ +∞ ∈ ℝ*
Theorem	pnfnemnf 11198	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 11199	Minus and plus infinity are different. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	mnfxr 11200	Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ -∞ ∈ ℝ*