P. 199 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19801-19900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nn0subm 19801	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- NN0 e. (SubMnd ` ℂfld )
Theorem	rege0subm 19802	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( 0 [,) +oo ) e. (SubMnd ` ℂfld )
Theorem	absabv 19803	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 e. (AbsVal ` ℂfld )
Theorem	zsssubrg 19804	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( R e. (SubRing ` ℂfld ) -> ZZ C_ R )
Theorem	qsssubdrg 19805	The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( R e. (SubRing ` ℂfld ) /\ (ℂfld ↾s R ) e. DivRing ) -> QQ C_ R )
Theorem	cnsubrg 19806	There are no subrings of the complex numbers strictly between RR and CC. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( R e. (SubRing ` ℂfld ) /\ RR C_ R ) -> R e. { RR , CC } )
Theorem	cnmgpabl 19807	The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- M = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   =>    |- M e. Abel
Theorem	cnmgpid 19808	The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.) (Revised by AV, 26-Aug-2021.)
|- M = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   =>    |- ( 0g ` M ) = 1
Theorem	cnmsubglem 19809*	Lemma for rpmsubg 19810 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- M = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- ( x e. A -> x e. CC )   &    |- ( x e. A -> x =/= 0 )   &    |- ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )   &    |- 1 e. A   &    |- ( x e. A -> ( 1 / x ) e. A )   =>    |- A e. (SubGrp ` M )
Theorem	rpmsubg 19810	The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- M = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   =>    |- RR+ e. (SubGrp ` M )
Theorem	gzrngunitlem 19811	Lemma for gzrngunit 19812. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- Z = (ℂfld ↾s ZZ[_i] )   =>    |- ( A e. (Unit ` Z ) -> 1 <_ ( abs ` A ) )
Theorem	gzrngunit 19812	The units on ZZ [ _i ] are the gaussian integers with norm 1. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- Z = (ℂfld ↾s ZZ[_i] )   =>    |- ( A e. (Unit ` Z ) <-> ( A e. ZZ[_i] /\ ( abs ` A ) = 1 ) )
Theorem	gsumfsum 19813*	Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> (ℂfld gsumg ( k e. A |-> B ) ) = sum_ k e. A B )
Theorem	regsumfsum 19814*	Relate a group sum on (ℂfld ↾s RR ) to a finite sum on the reals. Cf. gsumfsum 19813. (Contributed by Thierry Arnoux, 7-Sep-2018.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   =>    |- ( ph -> ( (ℂfld ↾s RR ) gsumg ( k e. A |-> B ) ) = sum_ k e. A B )
Theorem	expmhm 19815*	Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- N = (ℂfld ↾s NN0 )   &    |- M = (mulGrp ` ℂfld )   =>    |- ( A e. CC -> ( x e. NN0 |-> ( A ^ x ) ) e. ( N MndHom M ) )
Theorem	nn0srg 19816	The nonnegative integers form a semiring (commutative by subcmn 18242). (Contributed by Thierry Arnoux, 1-May-2018.)
|- (ℂfld ↾s NN0 ) e. SRing
Theorem	rge0srg 19817	The nonnegative real numbers form a semiring (commutative by subcmn 18242). (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- (ℂfld ↾s ( 0 [,) +oo ) ) e. 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 Z." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (ℂfld ↾s ZZ ), the field of complex numbers restricted to the integers. In zringring 19821 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 19837), and zringbas 19824 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as definition df-zring 19819 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 19818	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 19819	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
|- ℤring = (ℂfld ↾s ZZ )
Theorem	zringcrng 19820	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. CRing
Theorem	zringring 19821	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 e. Ring
Theorem	zringabl 19822	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. Abel
Theorem	zringgrp 19823	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
|- ℤring e. Grp
Theorem	zringbas 19824	The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
|- ZZ = ( Base ` ℤring )
Theorem	zringplusg 19825	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 19826	The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A (.g ` ℤring ) B ) = ( A x. B ) )
Theorem	zringmulr 19827	The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
|- x. = ( .r ` ℤring )
Theorem	zring0 19828	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 19829	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 19830	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
|- ℤring e. NzRing
Theorem	dvdsrzring 19831	Ring divisibility in the ring of integers corresponds to ordinary divisibility in ZZ. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
|- || = ( ||r ` ℤring )
Theorem	zringlpirlem1 19832	Lemma for zringlpir 19837. A nonzero ideal of integers contains some positive integers. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
|- ( ph -> I e. (LIdeal ` ℤring ) )   &    |- ( ph -> I =/= { 0 } )   =>    |- ( ph -> ( I i^i NN ) =/= (/) )
Theorem	zringlpirlem2 19833	Lemma for zringlpir 19837. 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.)
|- ( ph -> I e. (LIdeal ` ℤring ) )   &    |- ( ph -> I =/= { 0 } )   &    |- G = inf ( ( I i^i NN ) , RR , < )   =>    |- ( ph -> G e. I )
Theorem	zringlpirlem3 19834	Lemma for zringlpir 19837. 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.)
|- ( ph -> I e. (LIdeal ` ℤring ) )   &    |- ( ph -> I =/= { 0 } )   &    |- G = inf ( ( I i^i NN ) , RR , < )   &    |- ( ph -> X e. I )   =>    |- ( ph -> G || X )
Theorem	zringinvg 19835	The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- ( A e. ZZ -> -u A = ( ( invg ` ℤring ) ` A ) )
Theorem	zringunit 19836	The units of ZZ are the integers with norm 1, i.e. 1 and -u 1. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
|- ( A e. (Unit ` ℤring ) <-> ( A e. ZZ /\ ( abs ` A ) = 1 ) )
Theorem	zringlpir 19837	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 e. LPIR
Theorem	zringndrg 19838	The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.)
|- ℤring e/ DivRing
Theorem	zringcyg 19839	The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.)
|- ℤring e. CycGrp
Theorem	zringmpg 19840	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 ZZ ) = (mulGrp ` ℤring )
Theorem	prmirredlem 19841	A positive integer is irreducible over ZZ iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
|- I = (Irred ` ℤring )   =>    |- ( A e. NN -> ( A e. I <-> A e. Prime ) )
Theorem	dfprm2 19842	The positive irreducible elements of ZZ are the prime numbers. This is an alternative way to define Prime. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
|- I = (Irred ` ℤring )   =>    |- Prime = ( NN i^i I )
Theorem	prmirred 19843	The irreducible elements of ZZ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
|- I = (Irred ` ℤring )   =>    |- ( A e. I <-> ( A e. ZZ /\ ( abs ` A ) e. Prime ) )
Theorem	expghm 19844*	Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.)
|- M = (mulGrp ` ℂfld )   &    |- U = ( M ↾s ( CC \ { 0 } ) )   =>    |- ( ( A e. CC /\ A =/= 0 ) -> ( x e. ZZ |-> ( A ^ x ) ) e. (ℤring GrpHom U ) )
Theorem	mulgghm2 19845*	The powers of a group element give a homomorphism from ZZ to a group. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- .x. = (.g ` R )   &    |- F = ( n e. ZZ |-> ( n .x. .1. ) )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Grp /\ .1. e. B ) -> F e. (ℤring GrpHom R ) )
Theorem	mulgrhm 19846*	The powers of the element 1 give a ring homomorphism from ZZ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- .x. = (.g ` R )   &    |- F = ( n e. ZZ |-> ( n .x. .1. ) )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> F e. (ℤring RingHom R ) )
Theorem	mulgrhm2 19847*	The powers of the element 1 give the unique ring homomorphism from ZZ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- .x. = (.g ` R )   &    |- F = ( n e. ZZ |-> ( n .x. .1. ) )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> (ℤring RingHom R ) = { F } )
10.11.3  Algebraic constructions based on the complex numbers
Syntax	czrh 19848	Map the rationals into a field, or the integers into a ring.
class ZRHom
Syntax	czlm 19849	Augment an abelian group with vector space operations to turn it into a ZZ-module.
class ZMod
Syntax	cchr 19850	Syntax for ring characteristic.
class chr
Syntax	czn 19851	The ring of integers modulo n.
class ℤ/nℤ
Definition	df-zrh 19852	Define the unique homomorphism from the integers into a ring. This encodes the usual notation of n = 1r + 1r + ... + 1r for integers (see also df-mulg 17541). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
Definition	df-zlm 19853	Augment an abelian group with vector space operations to turn it into a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
Definition	df-chr 19854	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 = ( g e. _V |-> ( ( od ` g ) ` ( 1r ` g ) ) )
Definition	df-zn 19855*	Define the ring of integers mod n. This is literally the quotient ring of ZZ by the ideal n ZZ, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- ℤ/nℤ = ( n e. NN0 |-> [_ℤring / z ]_ [_ ( z /.s ( z ~QG ( (RSpan ` z ) ` { n } ) ) ) / s ]_ ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) )
Theorem	zrhval 19856	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.)
|- L = ( ZRHom ` R )   =>    |- L = U. (ℤring RingHom R )
Theorem	zrhval2 19857*	Alternate value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- L = ( ZRHom ` R )   &    |- .x. = (.g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) )
Theorem	zrhmulg 19858	Value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- L = ( ZRHom ` R )   &    |- .x. = (.g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ N e. ZZ ) -> ( L ` N ) = ( N .x. .1. ) )
Theorem	zrhrhmb 19859	The ZRHom homomorphism is the unique ring homomorphism from Z. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- ( R e. Ring -> ( F e. (ℤring RingHom R ) <-> F = L ) )
Theorem	zrhrhm 19860	The ZRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- ( R e. Ring -> L e. (ℤring RingHom R ) )
Theorem	zrh1 19861	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- L = ( ZRHom ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( L ` 1 ) = .1. )
Theorem	zrh0 19862	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( L ` 0 ) = .0. )
Theorem	zrhpropd 19863*	The ZZ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( ZRHom ` K ) = ( ZRHom ` L ) )
Theorem	zlmval 19864	Augment an abelian group with vector space operations to turn it into a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
|- W = ( ZMod ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> W = ( ( G sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )
Theorem	zlmlem 19865	Lemma for zlmbas 19866 and zlmplusg 19867. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- E = Slot N   &    |- N e. NN   &    |- N < 5   =>    |- ( E ` G ) = ( E ` W )
Theorem	zlmbas 19866	Base set of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- B = ( Base ` G )   =>    |- B = ( Base ` W )
Theorem	zlmplusg 19867	Group operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- .+ = ( +g ` G )   =>    |- .+ = ( +g ` W )
Theorem	zlmmulr 19868	Ring operation of a ZZ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- .x. = ( .r ` G )   =>    |- .x. = ( .r ` W )
Theorem	zlmsca 19869	Scalar ring of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
|- W = ( ZMod ` G )   =>    |- ( G e. V -> ℤring = (Scalar ` W ) )
Theorem	zlmvsca 19870	Scalar multiplication operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- .x. = (.g ` G )   =>    |- .x. = ( .s ` W )
Theorem	zlmlmod 19871	The ZZ-module operation turns an arbitrary abelian group into a left module over ZZ. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   =>    |- ( G e. Abel <-> W e. LMod )
Theorem	zlmassa 19872	The ZZ-module operation turns a ring into an associative algebra over ZZ. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   =>    |- ( G e. Ring <-> W e. AssAlg )
Theorem	chrval 19873	Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- O = ( od ` R )   &    |- .1. = ( 1r ` R )   &    |- C = (chr ` R )   =>    |- ( O ` .1. ) = C
Theorem	chrcl 19874	Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- C = (chr ` R )   =>    |- ( R e. Ring -> C e. NN0 )
Theorem	chrid 19875	The canonical ZZ ring homomorphism applied to a ring's characteristic is zero. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- C = (chr ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( L ` C ) = .0. )
Theorem	chrdvds 19876	The ZZ ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- C = (chr ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ N e. ZZ ) -> ( C || N <-> ( L ` N ) = .0. ) )
Theorem	chrcong 19877	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.)
|- C = (chr ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( C || ( M - N ) <-> ( L ` M ) = ( L ` N ) ) )
Theorem	chrnzr 19878	Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( R e. Ring -> ( R e. NzRing <-> (chr ` R ) =/= 1 ) )
Theorem	chrrhm 19879	The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( F e. ( R RingHom S ) -> (chr ` S ) || (chr ` R ) )
Theorem	domnchr 19880	The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( R e. Domn -> ( (chr ` R ) = 0 \/ (chr ` R ) e. Prime ) )
Theorem	znlidl 19881	The set n ZZ is an ideal in ZZ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   =>    |- ( N e. ZZ -> ( S ` { N } ) e. (LIdeal ` ℤring ) )
Theorem	zncrng2 19882	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, 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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   =>    |- ( N e. ZZ -> U e. CRing )
Theorem	znval 19883	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, 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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` U ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( ( F o. <_ ) o. `' F )   =>    |- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
Theorem	znle 19884	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, 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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` U ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )
Theorem	znval2 19885	Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
Theorem	znbaslem 19886	Lemma for znbas 19892. (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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- E = Slot K   &    |- K e. NN   &    |- K < ; 1 0   =>    |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) )
Theorem	znbaslemOLD 19887	Obsolete version of znbaslem 19886 as of 28-Apr-2021. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- E = Slot K   &    |- K e. NN   &    |- K < 10   =>    |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) )
Theorem	znbas2 19888	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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) )
Theorem	znadd 19889	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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) )
Theorem	znmul 19890	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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) )
Theorem	znzrh 19891	The ZZ 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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( ZRHom ` U ) = ( ZRHom ` Y ) )
Theorem	znbas 19892	The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- Y = (ℤ/nℤ ` N )   &    |- R = (ℤring ~QG ( S ` { N } ) )   =>    |- ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) )
Theorem	zncrng 19893	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> Y e. CRing )
Theorem	znzrh2 19894*	The ZZ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- .~ = (ℤring ~QG ( S ` { N } ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) )
Theorem	znzrhval 19895	The ZZ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- .~ = (ℤring ~QG ( S ` { N } ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] .~ )
Theorem	znzrhfo 19896	The ZZ ring homomorphism is a surjection onto ZZ / n ZZ. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( N e. NN0 -> L : ZZ -onto-> B )
Theorem	zncyg 19897	The group ZZ / n ZZ is cyclic for all n (including n = 0). (Contributed by Mario Carneiro, 21-Apr-2016.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> Y e. CycGrp )
Theorem	zndvds 19898	Express equality of equivalence classes in ZZ / n ZZ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( L ` A ) = ( L ` B ) <-> N || ( A - B ) ) )
Theorem	zndvds0 19899	Special case of zndvds 19898 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   &    |- .0. = ( 0g ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) = .0. <-> N || A ) )
Theorem	znf1o 19900	The function F enumerates all equivalence classes in ℤ/nℤ for each n. When n = 0, ZZ / 0 ZZ = ZZ / { 0 } ~~ ZZ so we let W = ZZ; otherwise W = { 0 , ... , n - 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.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   =>    |- ( N e. NN0 -> F : W -1-1-onto-> B )