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
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 21404 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 21422), and zringbas 21408 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 21402 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) 21402).
Syntax	czring 21401	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 21402	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
⊢ ℤring = (ℂfld ↾s ℤ)
Theorem	zringcrng 21403	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ CRing
Theorem	zringring 21404	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 21405	The ring of integers is a non-unital ring. (Contributed by AV, 17-Mar-2025.)
⊢ ℤring ∈ Rng
Theorem	zringabl 21406	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ Abel
Theorem	zringgrp 21407	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
⊢ ℤring ∈ Grp
Theorem	zringbas 21408	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 21409	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 21410	The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmulg 21411	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 21412	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 21413	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 21414	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 21415	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ℤring ∈ NzRing
Theorem	dvdsrzring 21416	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 21417	Lemma for zringlpir 21422. 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 21418	Lemma for zringlpir 21422. 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 21419	Lemma for zringlpir 21422. 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 21420	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 21421	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 21422	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 21423	The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.)
⊢ ℤring ∉ DivRing
Theorem	zringcyg 21424	The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.)
⊢ ℤring ∈ CycGrp
Theorem	zringsubgval 21425	Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmpg 21426	The multiplicative group of the ring of integers is the restriction of the multiplicative group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.)
⊢ ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring)
Theorem	prmirredlem 21427	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 21428	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 21429	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 21430*	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 21431*	The powers of a group element give a homomorphism from ℤ to a group. The name 1 should not be taken as a constraint as it may be any group element. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅))
Theorem	mulgrhm 21432*	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 21433*	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 𝑅) = {𝐹})
Theorem	irinitoringc 21434	The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ℤring ∈ 𝑈)    &   ⊢ 𝐶 = (RingCat‘𝑈)    ⇒   ⊢ (𝜑 → ℤring ∈ (InitO‘𝐶))
Theorem	nzerooringczr 21435	There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → ℤring ∈ 𝑈)    ⇒   ⊢ (𝜑 → (ZeroO‘𝐶) = ∅)
10.8.2.1  Example for a condition for a non-unital ring to be unital In this subsubsection, an example is given for a condition for a non-unital ring to be unital. This example is already mentioned in the comment for df-subrg 20503: " The subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity ⟨1, 0⟩ which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring." The theorems in this subsubsection do not assume that 𝑅 = (ℤring ×s ℤring) is a ring (which can be proven directly very easily, see pzriprng 21452), but provide the prerequisites for ring2idlqusb 21265 to show that 𝑅 is a unital ring, and for ring2idlqus1 21274 to show that ⟨1, 1⟩ is its ring unity.
Theorem	pzriprnglem1 21436	Lemma 1 for pzriprng 21452: 𝑅 is a non-unital (actually a unital!) ring. (Contributed by AV, 17-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	pzriprnglem2 21437	Lemma 2 for pzriprng 21452: The base set of 𝑅 is the cartesian product of the integers. (Contributed by AV, 17-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    ⇒   ⊢ (Base‘𝑅) = (ℤ × ℤ)
Theorem	pzriprnglem3 21438*	Lemma 3 for pzriprng 21452: An element of 𝐼 is an ordered pair. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑥 ∈ ℤ 𝑋 = ⟨𝑥, 0⟩)
Theorem	pzriprnglem4 21439	Lemma 4 for pzriprng 21452: 𝐼 is a subgroup of 𝑅. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ 𝐼 ∈ (SubGrp‘𝑅)
Theorem	pzriprnglem5 21440	Lemma 5 for pzriprng 21452: 𝐼 is a subring of the non-unital ring 𝑅. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ 𝐼 ∈ (SubRng‘𝑅)
Theorem	pzriprnglem6 21441	Lemma 6 for pzriprng 21452: 𝐽 has a ring unity. (Contributed by AV, 19-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ (𝑋 ∈ 𝐼 → ((⟨1, 0⟩(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)⟨1, 0⟩) = 𝑋))
Theorem	pzriprnglem7 21442	Lemma 7 for pzriprng 21452: 𝐽 is a unital ring. (Contributed by AV, 19-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ 𝐽 ∈ Ring
Theorem	pzriprnglem8 21443	Lemma 8 for pzriprng 21452: 𝐼 resp. 𝐽 is a two-sided ideal of the non-unital ring 𝑅. (Contributed by AV, 21-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ 𝐼 ∈ (2Ideal‘𝑅)
Theorem	pzriprnglem9 21444	Lemma 9 for pzriprng 21452: The ring unity of the ring 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ 1 = ⟨1, 0⟩
Theorem	pzriprnglem10 21445	Lemma 10 for pzriprng 21452: The equivalence classes of 𝑅 modulo 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → [⟨𝑋, 𝑌⟩] ∼ = (ℤ × {𝑌}))
Theorem	pzriprnglem11 21446*	Lemma 11 for pzriprng 21452: The base set of the quotient of 𝑅 and 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ (Base‘𝑄) = ∪ 𝑟 ∈ ℤ {(ℤ × {𝑟})}
Theorem	pzriprnglem12 21447	Lemma 12 for pzriprng 21452: 𝑄 has a ring unity. (Contributed by AV, 23-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ (𝑋 ∈ (Base‘𝑄) → (((ℤ × {1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋))
Theorem	pzriprnglem13 21448	Lemma 13 for pzriprng 21452: 𝑄 is a unital ring. (Contributed by AV, 23-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ 𝑄 ∈ Ring
Theorem	pzriprnglem14 21449	Lemma 14 for pzriprng 21452: The ring unity of the ring 𝑄. (Contributed by AV, 23-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ (1r‘𝑄) = (ℤ × {1})
Theorem	pzriprngALT 21450	The non-unital ring (ℤring ×s ℤring) is unital because it has the two-sided ideal (ℤ × {0}), which is unital, and the quotient of the ring and the ideal is also unital (using ring2idlqusb 21265). (Contributed by AV, 23-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ℤring ×s ℤring) ∈ Ring
Theorem	pzriprng1ALT 21451	The ring unity of the ring (ℤring ×s ℤring) constructed from the ring unity of the two-sided ideal (ℤ × {0}) and the ring unity of the quotient of the ring and the ideal (using ring2idlqus1 21274). (Contributed by AV, 24-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1r‘(ℤring ×s ℤring)) = ⟨1, 1⟩
Theorem	pzriprng 21452	The non-unital ring (ℤring ×s ℤring) is unital. Direct proof in contrast to pzriprngALT 21450. (Contributed by AV, 25-Mar-2025.)
⊢ (ℤring ×s ℤring) ∈ Ring
Theorem	pzriprng1 21453	The ring unity of the ring (ℤring ×s ℤring). Direct proof in contrast to pzriprng1ALT 21451. (Contributed by AV, 25-Mar-2025.)
⊢ (1r‘(ℤring ×s ℤring)) = ⟨1, 1⟩
10.8.3  Algebraic constructions based on the complex numbers
Syntax	czrh 21454	Map the rationals into a field, or the integers into a ring.
class ℤRHom
Syntax	czlm 21455	Augment an abelian group with vector space operations to turn it into a ℤ-module.
class ℤMod
Syntax	cchr 21456	Syntax for ring characteristic.
class chr
Syntax	czn 21457	The ring of integers modulo 𝑛.
class ℤ/nℤ
Definition	df-zrh 21458	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 18998). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
Definition	df-zlm 21459	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 21460	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 21461*	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 21462	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 21463*	Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )))
Theorem	zrhmulg 21464	Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 ))
Theorem	zrhrhmb 21465	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 21466	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 21467	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 )
Theorem	zrh0 21468	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 )
Theorem	zrhpropd 21469*	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 21470	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 21471	Lemma for zlmbas 21472 and zlmplusg 21473. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx)    &   ⊢ (𝐸‘ndx) ≠ ( ·𝑠 ‘ndx)    ⇒   ⊢ (𝐸‘𝐺) = (𝐸‘𝑊)
Theorem	zlmbas 21472	Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (Base‘𝑊)
Theorem	zlmplusg 21473	Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (+g‘𝑊)
Theorem	zlmmulr 21474	Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ · = (.r‘𝑊)
Theorem	zlmsca 21475	Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊))
Theorem	zlmvsca 21476	Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ · = ( ·𝑠 ‘𝑊)
Theorem	zlmlmod 21477	The ℤ-module operation turns an arbitrary abelian group into a left module over ℤ. Also see zlmassa 21859. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ LMod)
Theorem	chrval 21478	Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑂 = (od‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐶 = (chr‘𝑅)    ⇒   ⊢ (𝑂‘ 1 ) = 𝐶
Theorem	chrcl 21479	Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝐶 = (chr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐶 ∈ ℕ0)
Theorem	chrid 21480	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 21481	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 21482	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	dvdschrmulg 21483	In a ring, any multiple of the characteristics annihilates all elements. (Contributed by Thierry Arnoux, 6-Sep-2016.)
⊢ 𝐶 = (chr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵) → (𝑁 · 𝐴) = 0 )
Theorem	fermltlchr 21484	A generalization of Fermat's little theorem in a commutative ring 𝐹 of prime characteristic. See fermltl 16711. (Contributed by Thierry Arnoux, 9-Jan-2024.)
⊢ 𝑃 = (chr‘𝐹)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐹))    &   ⊢ 𝐴 = ((ℤRHom‘𝐹)‘𝐸)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐸 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑃 ↑ 𝐴) = 𝐴)
Theorem	chrnzr 21485	Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ (chr‘𝑅) ≠ 1))
Theorem	chrrhm 21486	The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅))
Theorem	domnchr 21487	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 21488	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 21489	Making a commutative ring as a quotient of ℤ and 𝑛ℤ. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    ⇒   ⊢ (𝑁 ∈ ℤ → 𝑈 ∈ CRing)
Theorem	znval 21490	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 21491	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 21492	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 21493	Lemma for znbas 21498. (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.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (le‘ndx)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐸‘𝑈) = (𝐸‘𝑌))
Theorem	znbas2 21494	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.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (Base‘𝑈) = (Base‘𝑌))
Theorem	znadd 21495	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.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (+g‘𝑈) = (+g‘𝑌))
Theorem	znmul 21496	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.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑆 = (RSpan‘ℤring)    &   ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (.r‘𝑈) = (.r‘𝑌))
Theorem	znzrh 21497	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 21498	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 21499	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)
Theorem	znzrh2 21500*	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 → 𝐿 = (𝑥 ∈ ℤ ↦ [𝑥] ∼ ))