P. 219 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21801-21900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zringinvg 21801	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 21802	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 21803	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 21804	The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.)
⊢ ℤring ∉ DivRing
Theorem	zringcyg 21805	The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.)
⊢ ℤring ∈ CycGrp
Theorem	zringsubgval 21806	Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmpg 21807	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 21808	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 21809	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 21810	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 21811*	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 21812*	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 21813*	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 21814*	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 21815	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 21816	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 20852: " 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 21833), but provide the prerequisites for ring2idlqusb 21636 to show that 𝑅 is a unital ring, and for ring2idlqus1 21645 to show that ⟨1, 1⟩ is its ring unity.
Theorem	pzriprnglem1 21817	Lemma 1 for pzriprng 21833: 𝑅 is a non-unital (actually a unital!) ring. (Contributed by AV, 17-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	pzriprnglem2 21818	Lemma 2 for pzriprng 21833: The base set of 𝑅 is the cartesian product of the integers. (Contributed by AV, 17-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    ⇒   ⊢ (Base‘𝑅) = (ℤ × ℤ)
Theorem	pzriprnglem3 21819*	Lemma 3 for pzriprng 21833: An element of 𝐼 is an ordered pair. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑥 ∈ ℤ 𝑋 = ⟨𝑥, 0⟩)
Theorem	pzriprnglem4 21820	Lemma 4 for pzriprng 21833: 𝐼 is a subgroup of 𝑅. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ 𝐼 ∈ (SubGrp‘𝑅)
Theorem	pzriprnglem5 21821	Lemma 5 for pzriprng 21833: 𝐼 is a subring of the non-unital ring 𝑅. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ 𝐼 ∈ (SubRng‘𝑅)
Theorem	pzriprnglem6 21822	Lemma 6 for pzriprng 21833: 𝐽 has a ring unity. (Contributed by AV, 19-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ (𝑋 ∈ 𝐼 → ((⟨1, 0⟩(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)⟨1, 0⟩) = 𝑋))
Theorem	pzriprnglem7 21823	Lemma 7 for pzriprng 21833: 𝐽 is a unital ring. (Contributed by AV, 19-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ 𝐽 ∈ Ring
Theorem	pzriprnglem8 21824	Lemma 8 for pzriprng 21833: 𝐼 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 21825	Lemma 9 for pzriprng 21833: The ring unity of the ring 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ 1 = ⟨1, 0⟩
Theorem	pzriprnglem10 21826	Lemma 10 for pzriprng 21833: The equivalence classes of 𝑅 modulo 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → [⟨𝑋, 𝑌⟩] ∼ = (ℤ × {𝑌}))
Theorem	pzriprnglem11 21827*	Lemma 11 for pzriprng 21833: 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 21828	Lemma 12 for pzriprng 21833: 𝑄 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 21829	Lemma 13 for pzriprng 21833: 𝑄 is a unital ring. (Contributed by AV, 23-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ 𝑄 ∈ Ring
Theorem	pzriprnglem14 21830	Lemma 14 for pzriprng 21833: 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 21831	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 21636). (Contributed by AV, 23-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ℤring ×s ℤring) ∈ Ring
Theorem	pzriprng1ALT 21832	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 21645). (Contributed by AV, 24-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1r‘(ℤring ×s ℤring)) = ⟨1, 1⟩
Theorem	pzriprng 21833	The non-unital ring (ℤring ×s ℤring) is unital. Direct proof in contrast to pzriprngALT 21831. (Contributed by AV, 25-Mar-2025.)
⊢ (ℤring ×s ℤring) ∈ Ring
Theorem	pzriprng1 21834	The ring unity of the ring (ℤring ×s ℤring). Direct proof in contrast to pzriprng1ALT 21832. (Contributed by AV, 25-Mar-2025.)
⊢ (1r‘(ℤring ×s ℤring)) = ⟨1, 1⟩
10.8.3  Algebraic constructions based on the complex numbers
Syntax	czrh 21835	Map the rationals into a field, or the integers into a ring.
class ℤRHom
Syntax	czlm 21836	Augment an abelian group with vector space operations to turn it into a ℤ-module.
class ℤMod
Syntax	cchr 21837	Syntax for ring characteristic.
class chr
Syntax	czn 21838	The ring of integers modulo 𝑛.
class ℤ/nℤ
Definition	df-zrh 21839	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 19307). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
Definition	df-zlm 21840	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 21841	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 21842*	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 21843	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 21844*	Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )))
Theorem	zrhmulg 21845	Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 ))
Theorem	zrhrhmb 21846	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 21847	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 21848	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 )
Theorem	zrh0 21849	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 )
Theorem	zrhpropd 21850*	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 21851	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 21852	Lemma for zlmbas 21853 and zlmplusg 21854. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx)    &   ⊢ (𝐸‘ndx) ≠ ( ·𝑠 ‘ndx)    ⇒   ⊢ (𝐸‘𝐺) = (𝐸‘𝑊)
Theorem	zlmbas 21853	Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (Base‘𝑊)
Theorem	zlmplusg 21854	Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (+g‘𝑊)
Theorem	zlmmulr 21855	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 21856	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 21857	Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ · = ( ·𝑠 ‘𝑊)
Theorem	zlmlmod 21858	The ℤ-module operation turns an arbitrary abelian group into a left module over ℤ. Also see zlmassa 22241. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ LMod)
Theorem	chrval 21859	Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑂 = (od‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐶 = (chr‘𝑅)    ⇒   ⊢ (𝑂‘ 1 ) = 𝐶
Theorem	chrcl 21860	Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝐶 = (chr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐶 ∈ ℕ0)
Theorem	chrid 21861	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 21862	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 21863	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 21864	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 21865	A generalization of Fermat's little theorem in a commutative ring 𝐹 of prime characteristic. See fermltl 16990. (Contributed by Thierry Arnoux, 9-Jan-2024.)
⊢ 𝑃 = (chr‘𝐹)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐹))    &   ⊢ 𝐴 = ((ℤRHom‘𝐹)‘𝐸)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐸 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑃 ↑ 𝐴) = 𝐴)
Theorem	chrnzr 21866	Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ (chr‘𝑅) ≠ 1))
Theorem	chrrhm 21867	The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅))
Theorem	domnchr 21868	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 21869	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 21870	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 21871	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 21872	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 21873	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 21874	Lemma for znbas 21879. (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 21875	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 21876	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 21877	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 21878	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 21879	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 21880	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)
Theorem	znzrh2 21881*	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 21882	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 21883	The ℤ ring homomorphism is a surjection onto ℤ/nℤ. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ⟶onto𝐵)
Theorem	zncyg 21884	The group ℤ / 𝑛ℤ is cyclic for all 𝑛 (including 𝑛 = 0). (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CycGrp)
Theorem	zndvds 21885	Express equality of equivalence classes in ℤ / 𝑛ℤ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ 𝑁 ∥ (𝐴 − 𝐵)))
Theorem	zndvds0 21886	Special case of zndvds 21885 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴))
Theorem	znf1o 21887	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-1onto𝐵)
Theorem	zzngim 21888	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 21889	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 21890	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 21891	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 21892	Lemma for zntos 21893. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset)
Theorem	zntos 21893	The ℤ/nℤ structure is a totally ordered set. (The order is not respected by the operations, except in the case 𝑁 = 0 when it coincides with the ordering on ℤ.) (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset)
Theorem	znhash 21894	The ℤ/nℤ structure has 𝑛 elements. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝐵) = 𝑁)
Theorem	znfi 21895	The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
Theorem	znfld 21896	The ℤ/nℤ structure is a finite field when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field)
Theorem	znidomb 21897	The ℤ/nℤ structure is a domain (and hence a field) precisely when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ))
Theorem	znchr 21898	Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (chr‘𝑌) = 𝑁)
Theorem	znunit 21899	The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1))
Theorem	znunithash 21900	The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝑈) = (ϕ‘𝑁))