P. 203 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20201-20300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	qsssubdrg 20201	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 20202	There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ})
Theorem	cnmgpabl 20203	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 20204	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 20205*	Lemma for rpmsubg 20206 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubGrp‘𝑀)
Theorem	rpmsubg 20206	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 20207	Lemma for gzrngunit 20208. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑍 = (ℂfld ↾s ℤ[i])    ⇒   ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴))
Theorem	gzrngunit 20208	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 20209*	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 20210*	Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 20209. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	expmhm 20211*	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 20212	The nonnegative integers form a semiring (commutative by subcmn 18628). (Contributed by Thierry Arnoux, 1-May-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ SRing
Theorem	rge0srg 20213	The nonnegative real numbers form a semiring (commutative by subcmn 18628). (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ (ℂfld ↾s (0[,)+∞)) ∈ SRing
10.11.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 20217 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 20233), and zringbas 20220 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as definition df-zring 20215 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)).
Syntax	zring 20214	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 20215	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
⊢ ℤring = (ℂfld ↾s ℤ)
Theorem	zringcrng 20216	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ CRing
Theorem	zringring 20217	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 20218	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ Abel
Theorem	zringgrp 20219	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
⊢ ℤring ∈ Grp
Theorem	zringbas 20220	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 20221	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 20222	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 20223	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 20224	The neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 0 = (0g‘ℤring)
Theorem	zring1 20225	The multiplicative neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 1 = (1r‘ℤring)
Theorem	zringnzr 20226	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ℤring ∈ NzRing
Theorem	dvdsrzring 20227	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 20228	Lemma for zringlpir 20233. 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 20229	Lemma for zringlpir 20233. 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 20230	Lemma for zringlpir 20233. 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 20231	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 20232	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 20233	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 20234	The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.)
⊢ ℤring ∉ DivRing
Theorem	zringcyg 20235	The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.)
⊢ ℤring ∈ CycGrp
Theorem	zringmpg 20236	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 20237	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 20238	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 20239	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 20240*	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 20241*	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 20242*	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 20243*	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.11.3  Algebraic constructions based on the complex numbers
Syntax	czrh 20244	Map the rationals into a field, or the integers into a ring.
class ℤRHom
Syntax	czlm 20245	Augment an abelian group with vector space operations to turn it into a ℤ-module.
class ℤMod
Syntax	cchr 20246	Syntax for ring characteristic.
class chr
Syntax	czn 20247	The ring of integers modulo 𝑛.
class ℤ/nℤ
Definition	df-zrh 20248	Define the unique homomorphism from the integers into a ring. This encodes the usual notation of 𝑛 = 1r + 1r + ... + 1r for integers (see also df-mulg 17928). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
Definition	df-zlm 20249	Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝑔)⟩))
Definition	df-chr 20250	The characteristic of a ring is the smallest positive integer which is equal to 0 when interpreted in the ring, or 0 if there is no such positive integer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ chr = (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔)))
Definition	df-zn 20251*	Define the ring of integers mod 𝑛. This is literally the quotient ring of ℤ by the ideal 𝑛ℤ, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))
Theorem	zrhval 20252	Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ 𝐿 = ∪ (ℤring RingHom 𝑅)
Theorem	zrhval2 20253*	Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )))
Theorem	zrhmulg 20254	Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 ))
Theorem	zrhrhmb 20255	The ℤRHom homomorphism is the unique ring homomorphism from 𝑍. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐹 ∈ (ℤring RingHom 𝑅) ↔ 𝐹 = 𝐿))
Theorem	zrhrhm 20256	The ℤRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅))
Theorem	zrh1 20257	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 )
Theorem	zrh0 20258	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 )
Theorem	zrhpropd 20259*	The ℤ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (ℤRHom‘𝐾) = (ℤRHom‘𝐿))
Theorem	zlmval 20260	Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑊 = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
Theorem	zlmlem 20261	Lemma for zlmbas 20262 and zlmplusg 20263. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 < 5    ⇒   ⊢ (𝐸‘𝐺) = (𝐸‘𝑊)
Theorem	zlmbas 20262	Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (Base‘𝑊)
Theorem	zlmplusg 20263	Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (+g‘𝑊)
Theorem	zlmmulr 20264	Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ · = (.r‘𝑊)
Theorem	zlmsca 20265	Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊))
Theorem	zlmvsca 20266	Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ · = ( ·𝑠 ‘𝑊)
Theorem	zlmlmod 20267	The ℤ-module operation turns an arbitrary abelian group into a left module over ℤ. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ LMod)
Theorem	zlmassa 20268	The ℤ-module operation turns a ring into an associative algebra over ℤ. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ Ring ↔ 𝑊 ∈ AssAlg)
Theorem	chrval 20269	Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑂 = (od‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐶 = (chr‘𝑅)    ⇒   ⊢ (𝑂‘ 1 ) = 𝐶
Theorem	chrcl 20270	Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝐶 = (chr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐶 ∈ ℕ0)
Theorem	chrid 20271	The canonical ℤ ring homomorphism applied to a ring's characteristic is zero. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝐶 = (chr‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘𝐶) = 0 )
Theorem	chrdvds 20272	The ℤ ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝐶 = (chr‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐶 ∥ 𝑁 ↔ (𝐿‘𝑁) = 0 ))
Theorem	chrcong 20273	If two integers are congruent relative to the ring characteristic, their images in the ring are the same. (Contributed by Mario Carneiro, 24-Sep-2015.)
⊢ 𝐶 = (chr‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐶 ∥ (𝑀 − 𝑁) ↔ (𝐿‘𝑀) = (𝐿‘𝑁)))
Theorem	chrnzr 20274	Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ (chr‘𝑅) ≠ 1))
Theorem	chrrhm 20275	The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅))
Theorem	domnchr 20276	The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝑅 ∈ Domn → ((chr‘𝑅) = 0 ∨ (chr‘𝑅) ∈ ℙ))
Theorem	znlidl 20277	The set 𝑛ℤ is an ideal in ℤ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    ⇒   ⊢ (𝑁 ∈ ℤ → (𝑆‘{𝑁}) ∈ (LIdeal‘ℤring))
Theorem	zncrng2 20278	The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    ⇒   ⊢ (𝑁 ∈ ℤ → 𝑈 ∈ CRing)
Theorem	znval 20279	The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet ⟨(le‘ndx), ≤ ⟩))
Theorem	znle 20280	The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹))
Theorem	znval2 20281	Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet ⟨(le‘ndx), ≤ ⟩))
Theorem	znbaslem 20282	Lemma for znbas 20287. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐸 = Slot 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐾 < ;10    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐸‘𝑈) = (𝐸‘𝑌))
Theorem	znbas2 20283	The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (Base‘𝑈) = (Base‘𝑌))
Theorem	znadd 20284	The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (+g‘𝑈) = (+g‘𝑌))
Theorem	znmul 20285	The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (.r‘𝑈) = (.r‘𝑌))
Theorem	znzrh 20286	The ℤ ring homomorphism of ℤ/nℤ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (ℤRHom‘𝑈) = (ℤRHom‘𝑌))
Theorem	znbas 20287	The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑅 = (ℤring ~QG (𝑆‘{𝑁}))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (ℤ / 𝑅) = (Base‘𝑌))
Theorem	zncrng 20288	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)
Theorem	znzrh2 20289*	The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁}))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐿 = (𝑥 ∈ ℤ ↦ [𝑥] ∼ ))
Theorem	znzrhval 20290	The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁}))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) = [𝐴] ∼ )
Theorem	znzrhfo 20291	The ℤ ring homomorphism is a surjection onto ℤ / 𝑛ℤ. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→𝐵)
Theorem	zncyg 20292	The group ℤ / 𝑛ℤ is cyclic for all 𝑛 (including 𝑛 = 0). (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CycGrp)
Theorem	zndvds 20293	Express equality of equivalence classes in ℤ / 𝑛ℤ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ 𝑁 ∥ (𝐴 − 𝐵)))
Theorem	zndvds0 20294	Special case of zndvds 20293 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴))
Theorem	znf1o 20295	The function 𝐹 enumerates all equivalence classes in ℤ/nℤ for each 𝑛. When 𝑛 = 0, ℤ / 0ℤ = ℤ / {0} ≈ ℤ so we let 𝑊 = ℤ; otherwise 𝑊 = {0, ..., 𝑛 − 1} enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊–1-1-onto→𝐵)
Theorem	zzngim 20296	The ℤ ring homomorphism is an isomorphism for 𝑁 = 0. (We only show group isomorphism here, but ring isomorphism follows, since it is a bijective ring homomorphism.) (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘0)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ 𝐿 ∈ (ℤring GrpIso 𝑌)
Theorem	znle2 20297	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹))
Theorem	znleval 20298	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))))
Theorem	znleval2 20299	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))
Theorem	zntoslem 20300	Lemma for zntos 20301. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset)