P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnfldadd 20801	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.)
⊢ + = (+g‘ℂfld)
Theorem	cnfldmul 20802	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.)
⊢ · = (.r‘ℂfld)
Theorem	cnfldcj 20803	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.)
⊢ ∗ = (*𝑟‘ℂfld)
Theorem	cnfldtset 20804	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.)
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld)
Theorem	cnfldle 20805	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.)
⊢ ≤ = (le‘ℂfld)
Theorem	cnfldds 20806	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.)
⊢ (abs ∘ − ) = (dist‘ℂfld)
Theorem	cnfldunif 20807	The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld)
Theorem	cnfldfun 20808	The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT 20809 by using cnfldstr 20798 and structn0fun 17023: in addition, it must be shown that ∅ ∉ ℂfld. (Contributed by AV, 18-Nov-2021.)
⊢ Fun ℂfld
Theorem	cnfldfunALT 20809	The field of complex numbers is a function. Alternate proof of cnfldfun 20808 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.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Fun ℂfld
Theorem	cnfldfunALTOLD 20810	Obsolete proof of cnfldfunALT 20809 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 20811	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 Struct ⟨1, ;12⟩
Theorem	xrsex 20812	The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 ∈ V
Theorem	xrsbas 20813	The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ* = (Base‘ℝ*𝑠)
Theorem	xrsadd 20814	The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ +𝑒 = (+g‘ℝ*𝑠)
Theorem	xrsmul 20815	The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e = (.r‘ℝ*𝑠)
Theorem	xrstset 20816	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠)
Theorem	xrsle 20817	The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ≤ = (le‘ℝ*𝑠)
Theorem	cncrng 20818	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
⊢ ℂfld ∈ CRing
Theorem	cnring 20819	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ℂfld ∈ Ring
Theorem	xrsmcmn 20820	The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 20834.) (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd
Theorem	cnfld0 20821	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 0 = (0g‘ℂfld)
Theorem	cnfld1 20822	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 1 = (1r‘ℂfld)
Theorem	cnfldneg 20823	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋)
Theorem	cnfldplusf 20824	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ + = (+𝑓‘ℂfld)
Theorem	cnfldsub 20825	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ − = (-g‘ℂfld)
Theorem	cndrng 20826	The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ℂfld ∈ DivRing
Theorem	cnflddiv 20827	The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ / = (/r‘ℂfld)
Theorem	cnfldinv 20828	The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋))
Theorem	cnfldmulg 20829	The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))
Theorem	cnfldexp 20830	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 20831	The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ℂfld ∈ *-Ring
Theorem	xrsmgm 20832	The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ Mgm
Theorem	xrsnsgrp 20833	The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∉ Smgrp
Theorem	xrsmgmdifsgrp 20834	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 20820. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp)
Theorem	xrs1mnd 20835	The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 20834. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 𝑅 ∈ Mnd
Theorem	xrs10 20836	The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	xrs1cmn 20837	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 20838	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 20839	The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd
Theorem	xrsds 20840*	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
Theorem	xrsdsval 20841	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵)))
Theorem	xrsdsreval 20842	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 20843	Lemma for xrsdsreclb 20844. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
Theorem	xrsdsreclb 20844	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 20845*	Lemma for nn0subm 20852 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ 0 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubMnd‘ℂfld)
Theorem	cnsubglem 20846*	Lemma for resubdrg 21012 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 𝐵 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubGrp‘ℂfld)
Theorem	cnsubrglem 20847*	Lemma for resubdrg 21012 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubRing‘ℂfld)
Theorem	cnsubdrglem 20848*	Lemma for resubdrg 21012 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing)
Theorem	qsubdrg 20849	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 20850	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ ∈ (SubRing‘ℂfld)
Theorem	gzsubrg 20851	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ[i] ∈ (SubRing‘ℂfld)
Theorem	nn0subm 20852	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ℕ0 ∈ (SubMnd‘ℂfld)
Theorem	rege0subm 20853	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
Theorem	absabv 20854	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 20855	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅)
Theorem	qsssubdrg 20856	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 20857	There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ})
Theorem	cnmgpabl 20858	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 20859	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 20860*	Lemma for rpmsubg 20861 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubGrp‘𝑀)
Theorem	rpmsubg 20861	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 20862	Lemma for gzrngunit 20863. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑍 = (ℂfld ↾s ℤ[i])    ⇒   ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴))
Theorem	gzrngunit 20863	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 20864*	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 20865*	Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 20864. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	expmhm 20866*	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 20867	The nonnegative integers form a semiring (commutative by subcmn 19615). (Contributed by Thierry Arnoux, 1-May-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ SRing
Theorem	rge0srg 20868	The nonnegative real numbers form a semiring (commutative by subcmn 19615). (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 20872 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 20888), and zringbas 20875 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 20870 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) 20870).
Syntax	czring 20869	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 20870	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
⊢ ℤring = (ℂfld ↾s ℤ)
Theorem	zringcrng 20871	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ CRing
Theorem	zringring 20872	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	zringabl 20873	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ Abel
Theorem	zringgrp 20874	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
⊢ ℤring ∈ Grp
Theorem	zringbas 20875	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 20876	The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ + = (+g‘ℤring)
Theorem	zringmulg 20877	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 20878	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 20879	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 20880	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 20881	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ℤring ∈ NzRing
Theorem	dvdsrzring 20882	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 20883	Lemma for zringlpir 20888. 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 20884	Lemma for zringlpir 20888. 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 20885	Lemma for zringlpir 20888. 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 20886	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 20887	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))
Theorem	zringlpir 20888	The integers are a principal ideal ring. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.)
⊢ ℤring ∈ LPIR
Theorem	zringndrg 20889	The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.)
⊢ ℤring ∉ DivRing
Theorem	zringcyg 20890	The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.)
⊢ ℤring ∈ CycGrp
Theorem	zringsubgval 20891	Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmpg 20892	The multiplication group of the ring of integers is the restriction of the multiplication group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.)
⊢ ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring)
Theorem	prmirredlem 20893	A positive integer is irreducible over ℤ iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ 𝐼 = (Irred‘ℤring)    ⇒   ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ))
Theorem	dfprm2 20894	The positive irreducible elements of ℤ are the prime numbers. This is an alternative way to define ℙ. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ 𝐼 = (Irred‘ℤring)    ⇒   ⊢ ℙ = (ℕ ∩ 𝐼)
Theorem	prmirred 20895	The irreducible elements of ℤ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ 𝐼 = (Irred‘ℤring)    ⇒   ⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈ ℙ))
Theorem	expghm 20896*	Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ 𝑈 = (𝑀 ↾s (ℂ ∖ {0}))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈))
Theorem	mulgghm2 20897*	The powers of a group element give a homomorphism from ℤ to a group. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅))
Theorem	mulgrhm 20898*	The powers of the element 1 give a ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐹 ∈ (ℤring RingHom 𝑅))
Theorem	mulgrhm2 20899*	The powers of the element 1 give the unique ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (ℤring RingHom 𝑅) = {𝐹})
10.8.3  Algebraic constructions based on the complex numbers
Syntax	czrh 20900	Map the rationals into a field, or the integers into a ring.
class ℤRHom