P. 216 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21501-21600   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-lpidl 21501*	Define the class of left principal ideals of a ring, which are ideals with a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ LPIdeal = (𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
Definition	df-lpir 21502	Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ LPIR = {𝑤 ∈ Ring ∣ (LIdeal‘𝑤) = (LPIdeal‘𝑤)}
Theorem	lpival 21503*	Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})})
Theorem	islpidl 21504*	Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔})))
Theorem	lpi0 21505	The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃)
Theorem	lpi1 21506	The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃)
Theorem	islpir 21507	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃))
Theorem	lpiss 21508	Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈)
Theorem	islpir2 21509	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃))
Theorem	lpirring 21510	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring)
Theorem	drnglpir 21511	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR)
Theorem	rspsn 21512*	Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐾‘{𝐺}) = {𝑥 ∣ 𝐺 ∥ 𝑥})
Theorem	lidldvgen 21513*	An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵) → (𝐼 = (𝐾‘{𝐺}) ↔ (𝐺 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 𝐺 ∥ 𝑥)))
Theorem	lpigen 21514*	An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐼 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 𝑥 ∥ 𝑦))
10.7.5  Principal ideal domains
Syntax	cpid 21515	Class of principal ideal domains.
class PID
Definition	df-pid 21516	A principal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ PID = (IDomn ∩ LPIR)
10.8  The complex numbers as an algebraic extensible structure
10.8.1  Definition and basic properties
Syntax	cpsmet 21517	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 21518	Extend class notation with the class of all extended metric spaces.
class ∞Met
Syntax	cmet 21519	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 21520	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 21521	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 21522	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 21523	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 21524	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 21525*	Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Definition	df-xmet 21526*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 21527, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Definition	df-met 21527*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 24489. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. The 4 properties in Gleason's definition are shown by met0 24511, metgt0 24527, metsym 24518, and mettri 24520. (Contributed by NM, 25-Aug-2006.)
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
Definition	df-bl 21528*	Define the metric space ball function. See blval 24554 for its value. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
Definition	df-mopn 21529	Define a function whose value is the family of open sets of a metric space. See elmopn 24610 for its main property. (Contributed by NM, 1-Sep-2006.)
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
Definition	df-fbas 21530*	Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)})
Definition	df-fg 21531*	Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
Definition	df-metu 21532*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))
Syntax	ccnfld 21533	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 21534*	The field of complex numbers. Other number fields and rings can be constructed by applying the ↾s restriction operator, for instance (ℂfld ↾ 𝔸) is the field of algebraic numbers. The contract of this set is defined entirely by cnfldex 21536, cnfldadd 21539, cnfldmul 21541, cnfldcj 21542, cnfldtset 21543, cnfldle 21544, cnfldds 21545, and cnfldbas 21537. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.)
⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
Theorem	cnfldstr 21535	The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ ℂfld Struct ⟨1, ;13⟩
Theorem	cnfldex 21536	The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Avoid complex number axioms and ax-pow 5335. (Revised by GG, 16-Mar-2025.)
⊢ ℂfld ∈ V
Theorem	cnfldbas 21537	The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ ℂ = (Base‘ℂfld)
Theorem	mpocnfldadd 21538*	The addition operation of the field of complex numbers. Version of cnfldadd 21539 using maps-to notation, which does not require ax-addf 11185. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld)
Theorem	cnfldadd 21539	The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 27-Apr-2025.)
⊢ + = (+g‘ℂfld)
Theorem	mpocnfldmul 21540*	The multiplication operation of the field of complex numbers. Version of cnfldmul 21541 using maps-to notation, which does not require ax-mulf 11186. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (.r‘ℂfld)
Theorem	cnfldmul 21541	The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 27-Apr-2025.)
⊢ · = (.r‘ℂfld)
Theorem	cnfldcj 21542	The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ ∗ = (*𝑟‘ℂfld)
Theorem	cnfldtset 21543	The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld)
Theorem	cnfldle 21544	The ordering of the field of complex numbers. Note that this is not actually an ordering on ℂ, but we put it in the structure anyway because restricting to ℝ does not affect this component, so that (ℂfld ↾s ℝ) is an ordered field even though ℂfld itself is not. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ ≤ = (le‘ℂfld)
Theorem	cnfldds 21545	The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ (abs ∘ − ) = (dist‘ℂfld)
Theorem	cnfldunif 21546	The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld)
Theorem	cnfldfun 21547	The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT 21548 by using cnfldstr 21535 and structn0fun 17217: in addition, it must be shown that ∅ ∉ ℂfld. (Contributed by AV, 18-Nov-2021.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.)
⊢ Fun ℂfld
Theorem	cnfldfunALT 21548	The field of complex numbers is a function. Alternate proof of cnfldfun 21547 not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) Revise df-cnfld 21534. (Revised by GG, 31-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	xrsstr 21549	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 Struct ⟨1, ;12⟩
Theorem	xrsex 21550	The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 ∈ V
Theorem	xrsadd 21551	The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ +𝑒 = (+g‘ℝ*𝑠)
Theorem	xrsmul 21552	The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e = (.r‘ℝ*𝑠)
Theorem	xrstset 21553	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠)
Theorem	cncrng 21554	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) Avoid ax-mulf 11186. (Revised by GG, 31-Mar-2025.)
⊢ ℂfld ∈ CRing
Theorem	cnring 21555	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ℂfld ∈ Ring
Theorem	xrsmcmn 21556	The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 21570.) (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd
Theorem	cnfld0 21557	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 0 = (0g‘ℂfld)
Theorem	cnfld1 21558	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11186. (Revised by GG, 31-Mar-2025.)
⊢ 1 = (1r‘ℂfld)
Theorem	cnfldneg 21559	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋)
Theorem	cnfldplusf 21560	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ + = (+𝑓‘ℂfld)
Theorem	cnfldsub 21561	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ − = (-g‘ℂfld)
Theorem	cndrng 21562	The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11186. (Revised by GG, 30-Apr-2025.)
⊢ ℂfld ∈ DivRing
Theorem	cnflddiv 21563	The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) Avoid ax-mulf 11186. (Revised by GG, 30-Apr-2025.)
⊢ / = (/r‘ℂfld)
Theorem	cnfldinv 21564	The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋))
Theorem	cnfldmulg 21565	The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))
Theorem	cnfldexp 21566	The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐵(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑𝐵))
Theorem	cnsrng 21567	The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ℂfld ∈ *-Ring
Theorem	xrsmgm 21568	The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ Mgm
Theorem	xrsnsgrp 21569	The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∉ Smgrp
Theorem	xrsmgmdifsgrp 21570	The "additive group" of the extended reals is a magma but not a semigroup, and therefore also not a monoid nor a group, in contrast to the "multiplicative group", see xrsmcmn 21556. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp)
Theorem	xrsds 21571*	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
Theorem	xrsdsval 21572	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵)))
Theorem	xrsdsreval 21573	The metric of the extended real number structure coincides with the real number metric on the reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	xrsdsreclblem 21574	Lemma for xrsdsreclb 21575. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
Theorem	xrsdsreclb 21575	The metric of the extended real number structure is only real when both arguments are real. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) → ((𝐴𝐷𝐵) ∈ ℝ ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
Theorem	cnsubmlem 21576*	Lemma for nn0subm 21583 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ 0 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubMnd‘ℂfld)
Theorem	cnsubglem 21577*	Lemma for resubdrg 21769 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 𝐵 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubGrp‘ℂfld)
Theorem	cnsubrglem 21578*	Lemma for resubdrg 21769 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) Avoid ax-mulf 11186. (Revised by GG, 30-Apr-2025.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubRing‘ℂfld)
Theorem	cnsubdrglem 21579*	Lemma for resubdrg 21769 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing)
Theorem	qsubdrg 21580	The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
Theorem	zsubrg 21581	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ ∈ (SubRing‘ℂfld)
Theorem	gzsubrg 21582	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ[i] ∈ (SubRing‘ℂfld)
Theorem	nn0subm 21583	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ℕ0 ∈ (SubMnd‘ℂfld)
Theorem	rege0subm 21584	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
Theorem	absabv 21585	The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ abs ∈ (AbsVal‘ℂfld)
Theorem	zsssubrg 21586	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅)
Theorem	qsssubdrg 21587	The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝑅) ∈ DivRing) → ℚ ⊆ 𝑅)
Theorem	cnsubrg 21588	There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ})
Theorem	cnmgpabl 21589	The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    ⇒   ⊢ 𝑀 ∈ Abel
Theorem	cnmgpid 21590	The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.) (Revised by AV, 26-Aug-2021.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    ⇒   ⊢ (0g‘𝑀) = 1
Theorem	cnmsubglem 21591*	Lemma for rpmsubg 21592 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubGrp‘𝑀)
Theorem	rpmsubg 21592	The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    ⇒   ⊢ ℝ+ ∈ (SubGrp‘𝑀)
Theorem	gzrngunitlem 21593	Lemma for gzrngunit 21594. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑍 = (ℂfld ↾s ℤ[i])    ⇒   ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴))
Theorem	gzrngunit 21594	The units on ℤ[i] are the gaussian integers with norm 1. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑍 = (ℂfld ↾s ℤ[i])    ⇒   ⊢ (𝐴 ∈ (Unit‘𝑍) ↔ (𝐴 ∈ ℤ[i] ∧ (abs‘𝐴) = 1))
Theorem	gsumfsum 21595*	Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	regsumfsum 21596*	Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 21595. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	expmhm 21597*	Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑁 = (ℂfld ↾s ℕ0)    &   ⊢ 𝑀 = (mulGrp‘ℂfld)    ⇒   ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀))
Theorem	nn0srg 21598	The nonnegative integers form a semiring (commutative by subcmn 19913). (Contributed by Thierry Arnoux, 1-May-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ SRing
Theorem	rge0srg 21599	The nonnegative real numbers form a semiring (commutative by subcmn 19913). (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ (ℂfld ↾s (0[,)+∞)) ∈ SRing
Theorem	xrge0plusg 21600	The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ +𝑒 = (+g‘(ℝ*𝑠 ↾s (0[,]+∞)))