P. 215 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21401-21500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnfldfun 21401	The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT 21402 by using cnfldstr 21389 and structn0fun 17198: in addition, it must be shown that ∅ ∉ ℂfld. (Contributed by AV, 18-Nov-2021.) Revise df-cnfld 21388. (Revised by GG, 31-Mar-2025.)
⊢ Fun ℂfld
Theorem	cnfldfunALT 21402	The field of complex numbers is a function. Alternate proof of cnfldfun 21401 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 21388. (Revised by GG, 31-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	dfcnfldOLD 21403	Obsolete version of df-cnfld 21388 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) (Proof modification is discouraged.) (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	cnfldstrOLD 21404	Obsolete version of cnfldstr 21389 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂfld Struct ⟨1, ;13⟩
Theorem	cnfldexOLD 21405	Obsolete version of cnfldex 21390 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂfld ∈ V
Theorem	cnfldbasOLD 21406	Obsolete version of cnfldbas 21391 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂ = (Base‘ℂfld)
Theorem	cnfldaddOLD 21407	Obsolete version of cnfldadd 21393 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ + = (+g‘ℂfld)
Theorem	cnfldmulOLD 21408	Obsolete version of cnfldmul 21395 as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ · = (.r‘ℂfld)
Theorem	cnfldcjOLD 21409	Obsolete version of cnfldcj 21396 as of 27-Apr-2025. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∗ = (*𝑟‘ℂfld)
Theorem	cnfldtsetOLD 21410	Obsolete version of cnfldtset 21397 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld)
Theorem	cnfldleOLD 21411	Obsolete version of cnfldle 21398 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ≤ = (le‘ℂfld)
Theorem	cnflddsOLD 21412	Obsolete version of cnfldds 21399 as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (abs ∘ − ) = (dist‘ℂfld)
Theorem	cnfldunifOLD 21413	Obsolete version of cnfldunif 21400 as of 27-Apr-2025. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld)
Theorem	cnfldfunOLD 21414	Obsolete version of cnfldfun 21401 as of 27-Apr-2025. (Contributed by AV, 18-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	cnfldfunALTOLD 21415	Obsolete version of cnfldfunALT 21402 as of 27-Apr-2025. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	cnfldfunALTOLDOLD 21416	Obsolete proof of cnfldfunALTOLD 21415 as of 10-Nov-2024. The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	xrsstr 21417	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 Struct ⟨1, ;12⟩
Theorem	xrsex 21418	The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 ∈ V
Theorem	xrsbas 21419	The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ* = (Base‘ℝ*𝑠)
Theorem	xrsadd 21420	The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ +𝑒 = (+g‘ℝ*𝑠)
Theorem	xrsmul 21421	The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e = (.r‘ℝ*𝑠)
Theorem	xrstset 21422	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠)
Theorem	xrsle 21423	The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ≤ = (le‘ℝ*𝑠)
Theorem	cncrng 21424	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) Avoid ax-mulf 11264. (Revised by GG, 31-Mar-2025.)
⊢ ℂfld ∈ CRing
Theorem	cncrngOLD 21425	Obsolete version of cncrng 21424 as of 30-Apr-2025. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂfld ∈ CRing
Theorem	cnring 21426	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ℂfld ∈ Ring
Theorem	xrsmcmn 21427	The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 21444.) (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd
Theorem	cnfld0 21428	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 0 = (0g‘ℂfld)
Theorem	cnfld1 21429	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11264. (Revised by GG, 31-Mar-2025.)
⊢ 1 = (1r‘ℂfld)
Theorem	cnfld1OLD 21430	Obsolete version of cnfld1 21429 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 1 = (1r‘ℂfld)
Theorem	cnfldneg 21431	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋)
Theorem	cnfldplusf 21432	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ + = (+𝑓‘ℂfld)
Theorem	cnfldsub 21433	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ − = (-g‘ℂfld)
Theorem	cndrng 21434	The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11264. (Revised by GG, 30-Apr-2025.)
⊢ ℂfld ∈ DivRing
Theorem	cndrngOLD 21435	Obsolete version of cndrng 21434 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂfld ∈ DivRing
Theorem	cnflddiv 21436	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 11264. (Revised by GG, 30-Apr-2025.)
⊢ / = (/r‘ℂfld)
Theorem	cnflddivOLD 21437	Obsolete version of cnflddiv 21436 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ / = (/r‘ℂfld)
Theorem	cnfldinv 21438	The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋))
Theorem	cnfldmulg 21439	The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))
Theorem	cnfldexp 21440	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 21441	The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ℂfld ∈ *-Ring
Theorem	xrsmgm 21442	The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ Mgm
Theorem	xrsnsgrp 21443	The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∉ Smgrp
Theorem	xrsmgmdifsgrp 21444	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 21427. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp)
Theorem	xrs1mnd 21445	The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 21444. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 𝑅 ∈ Mnd
Theorem	xrs10 21446	The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	xrs1cmn 21447	The extended real numbers restricted to ℝ* ∖ {-∞} form a commutative monoid. They are not a group because 1 + +∞ = 2 + +∞ even though 1 ≠ 2. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 𝑅 ∈ CMnd
Theorem	xrge0subm 21448	The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ (0[,]+∞) ∈ (SubMnd‘𝑅)
Theorem	xrge0cmn 21449	The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd
Theorem	xrsds 21450*	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
Theorem	xrsdsval 21451	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵)))
Theorem	xrsdsreval 21452	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 21453	Lemma for xrsdsreclb 21454. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
Theorem	xrsdsreclb 21454	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 21455*	Lemma for nn0subm 21463 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ 0 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubMnd‘ℂfld)
Theorem	cnsubglem 21456*	Lemma for resubdrg 21649 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 𝐵 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubGrp‘ℂfld)
Theorem	cnsubrglem 21457*	Lemma for resubdrg 21649 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) Avoid ax-mulf 11264. (Revised by GG, 30-Apr-2025.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubRing‘ℂfld)
Theorem	cnsubrglemOLD 21458*	Obsolete version of cnsubrglem 21457 as of 30-Apr-2025. (Contributed by Mario Carneiro, 4-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubRing‘ℂfld)
Theorem	cnsubdrglem 21459*	Lemma for resubdrg 21649 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing)
Theorem	qsubdrg 21460	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 21461	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ ∈ (SubRing‘ℂfld)
Theorem	gzsubrg 21462	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ[i] ∈ (SubRing‘ℂfld)
Theorem	nn0subm 21463	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ℕ0 ∈ (SubMnd‘ℂfld)
Theorem	rege0subm 21464	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
Theorem	absabv 21465	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 21466	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅)
Theorem	qsssubdrg 21467	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 21468	There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ})
Theorem	cnmgpabl 21469	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 21470	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 21471*	Lemma for rpmsubg 21472 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubGrp‘𝑀)
Theorem	rpmsubg 21472	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 21473	Lemma for gzrngunit 21474. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑍 = (ℂfld ↾s ℤ[i])    ⇒   ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴))
Theorem	gzrngunit 21474	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 21475*	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 21476*	Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 21475. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	expmhm 21477*	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 21478	The nonnegative integers form a semiring (commutative by subcmn 19879). (Contributed by Thierry Arnoux, 1-May-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ SRing
Theorem	rge0srg 21479	The nonnegative real numbers form a semiring (commutative by subcmn 19879). (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ (ℂfld ↾s (0[,)+∞)) ∈ SRing
10.8.2  Ring of integers According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring 𝑍." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (ℂfld ↾s ℤ), the field of complex numbers restricted to the integers. In zringring 21483 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 21501), and zringbas 21487 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 21481 of the ring of integers. Remark: Instead of using the symbol "ZZrng" analogous to ℂfld used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra) 21481).
Syntax	czring 21480	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 21481	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
⊢ ℤring = (ℂfld ↾s ℤ)
Theorem	zringcrng 21482	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ CRing
Theorem	zringring 21483	The ring of integers is a ring. (Contributed by AV, 20-May-2019.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 13-Jun-2019.)
⊢ ℤring ∈ Ring
Theorem	zringrng 21484	The ring of integers is a non-unital ring. (Contributed by AV, 17-Mar-2025.)
⊢ ℤring ∈ Rng
Theorem	zringabl 21485	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ Abel
Theorem	zringgrp 21486	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
⊢ ℤring ∈ Grp
Theorem	zringbas 21487	The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
⊢ ℤ = (Base‘ℤring)
Theorem	zringplusg 21488	The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ + = (+g‘ℤring)
Theorem	zringsub 21489	The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmulg 21490	The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴(.g‘ℤring)𝐵) = (𝐴 · 𝐵))
Theorem	zringmulr 21491	The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ · = (.r‘ℤring)
Theorem	zring0 21492	The zero element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 0 = (0g‘ℤring)
Theorem	zring1 21493	The unity element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 1 = (1r‘ℤring)
Theorem	zringnzr 21494	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ℤring ∈ NzRing
Theorem	dvdsrzring 21495	Ring divisibility in the ring of integers corresponds to ordinary divisibility in ℤ. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
⊢ ∥ = (∥r‘ℤring)
Theorem	zringlpirlem1 21496	Lemma for zringlpir 21501. A nonzero ideal of integers contains some positive integers. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring))    &   ⊢ (𝜑 → 𝐼 ≠ {0})    ⇒   ⊢ (𝜑 → (𝐼 ∩ ℕ) ≠ ∅)
Theorem	zringlpirlem2 21497	Lemma for zringlpir 21501. A nonzero ideal of integers contains the least positive element. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Revised by AV, 27-Sep-2020.)
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring))    &   ⊢ (𝜑 → 𝐼 ≠ {0})    &   ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < )    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐼)
Theorem	zringlpirlem3 21498	Lemma for zringlpir 21501. All elements of a nonzero ideal of integers are divided by the least one. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.)
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring))    &   ⊢ (𝜑 → 𝐼 ≠ {0})    &   ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < )    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝐺 ∥ 𝑋)
Theorem	zringinvg 21499	The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ (𝐴 ∈ ℤ → -𝐴 = ((invg‘ℤring)‘𝐴))
Theorem	zringunit 21500	The units of ℤ are the integers with norm 1, i.e. 1 and -1. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1))