P. 151 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	ccnfld 15001	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 15002*	The field of complex numbers. Other number fields and rings can be constructed by applying the ↾s restriction operator. The contract of this set is defined entirely by cnfldex 15004, cnfldadd 15007, cnfldmul 15009, cnfldcj 15010, cnfldtset 15011, cnfldle 15012, cnfldds 15013, and cnfldbas 15005. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.)
|- ℂfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } ) )
Theorem	cnfldstr 15003	The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- ℂfld Struct <. 1 , ; 1 3 >.
Theorem	cnfldex 15004	The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- ℂfld e. _V
Theorem	cnfldbas 15005	The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- CC = ( Base ` ℂfld )
Theorem	mpocnfldadd 15006*	The addition operation of the field of complex numbers. Version of cnfldadd 15007 using maps-to notation, which does not require ax-addf 8307. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x + y ) ) = ( +g ` ℂfld )
Theorem	cnfldadd 15007	The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
|- + = ( +g ` ℂfld )
Theorem	mpocnfldmul 15008*	The multiplication operation of the field of complex numbers. Version of cnfldmul 15009 using maps-to notation, which does not require ax-mulf 8308. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) = ( .r ` ℂfld )
Theorem	cnfldmul 15009	The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
|- x. = ( .r ` ℂfld )
Theorem	cnfldcj 15010	The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- * = ( *r ` ℂfld )
Theorem	cnfldtset 15011	The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 31-Mar-2025.)
|- ( MetOpen ` ( abs o. - ) ) = (TopSet ` ℂfld )
Theorem	cnfldle 15012	The ordering of the field of complex numbers. Note that this is not actually an ordering on CC, but we put it in the structure anyway because restricting to RR does not affect this component, so that (ℂfld ↾s RR ) is an ordered field even though ℂfld itself is not. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 15002. (Revised by GG, 31-Mar-2025.)
|- <_ = ( le ` ℂfld )
Theorem	cnfldds 15013	The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 15002. (Revised by GG, 31-Mar-2025.)
|- ( abs o. - ) = ( dist ` ℂfld )
Theorem	cncrng 15014	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
|- ℂfld e. CRing
Theorem	cnring 15015	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. Ring
Theorem	cnfld0 15016	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 0 = ( 0g ` ℂfld )
Theorem	cnfld1 15017	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 1 = ( 1r ` ℂfld )
Theorem	cnfldneg 15018	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ( X e. CC -> ( ( invg ` ℂfld ) ` X ) = -u X )
Theorem	cnfldplusf 15019	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- + = ( +f ` ℂfld )
Theorem	cnfldsub 15020	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- - = ( -g ` ℂfld )
Theorem	cnfldmulg 15021	The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ( A e. ZZ /\ B e. CC ) -> ( A (.g ` ℂfld ) B ) = ( A x. B ) )
Theorem	cnfldexp 15022	The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.)
|- ( ( A e. CC /\ B e. NN0 ) -> ( B (.g ` (mulGrp ` ℂfld ) ) A ) = ( A ^ B ) )
Theorem	cnsubmlem 15023*	Lemma for nn0subm 15028 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( x e. A -> x e. CC )   &    |- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )   &    |- 0 e. A   =>    |- A e. (SubMnd ` ℂfld )
Theorem	cnsubglem 15024*	Lemma for cnsubrglem 15025 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( x e. A -> x e. CC )   &    |- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )   &    |- ( x e. A -> -u x e. A )   &    |- B e. A   =>    |- A e. (SubGrp ` ℂfld )
Theorem	cnsubrglem 15025*	Lemma for zsubrg 15026 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( x e. A -> x e. CC )   &    |- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )   &    |- ( x e. A -> -u x e. A )   &    |- 1 e. A   &    |- ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )   =>    |- A e. (SubRing ` ℂfld )
Theorem	zsubrg 15026	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ e. (SubRing ` ℂfld )
Theorem	gzsubrg 15027	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ[_i] e. (SubRing ` ℂfld )
Theorem	nn0subm 15028	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- NN0 e. (SubMnd ` ℂfld )
Theorem	rege0subm 15029	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( 0 [,) +oo ) e. (SubMnd ` ℂfld )
Theorem	zsssubrg 15030	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	gsumfsum 15031*	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	cnfldui 15032	The invertible complex numbers are exactly those apart from zero. This is recapb 9009 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.)
|- { z e. CC | z # 0 } = (Unit ` ℂfld )
7.7.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 15036 it is shown that this restriction is a ring, and zringbas 15039 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 15034 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) 15034).
Syntax	czring 15033	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 15034	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
|- ℤring = (ℂfld ↾s ZZ )
Theorem	zringcrng 15035	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. CRing
Theorem	zringring 15036	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 15037	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. Abel
Theorem	zringgrp 15038	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
|- ℤring e. Grp
Theorem	zringbas 15039	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 15040	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 15041	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 15042	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 15043	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 15044	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 15045	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
|- ℤring e. NzRing
Theorem	dvdsrzring 15046	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	zringinvg 15047	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	zringsubgval 15048	Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.)
|- .- = ( -g ` ℤring )   =>    |- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )
Theorem	zringmpg 15049	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 ZZ ) = (mulGrp ` ℤring )
Theorem	expghmap 15050*	Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.)
|- M = (mulGrp ` ℂfld )   &    |- U = ( M ↾s { z e. CC | z # 0 } )   =>    |- ( ( A e. CC /\ A # 0 ) -> ( x e. ZZ |-> ( A ^ x ) ) e. (ℤring GrpHom U ) )
Theorem	mulgghm2 15051*	The powers of a group element give a homomorphism from ZZ 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.)
|- .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 15052*	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 15053*	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 } )
7.7.3  Algebraic constructions based on the complex numbers
Syntax	czrh 15054	Map the rationals into a field, or the integers into a ring.
class ZRHom
Syntax	czlm 15055	Augment an abelian group with vector space operations to turn it into a ZZ-module.
class ZMod
Syntax	czn 15056	The ring of integers modulo n.
class ℤ/nℤ
Definition	df-zrh 15057	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 13981). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
Definition	df-zlm 15058	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-zn 15059*	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 15060	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	zrhvalg 15061	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 )   =>    |- ( R e. V -> L = U. (ℤring RingHom R ) )
Theorem	zrhval2 15062*	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 15063	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	zrhex 15064	Set existence for ZRHom. (Contributed by Jim Kingdon, 19-May-2025.)
|- L = ( ZRHom ` R )   =>    |- ( R e. V -> L e. _V )
Theorem	zrhrhmb 15065	The ZRHom homomorphism is the unique ring homomorphism from ZZ. (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 15066	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 15067	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 15068	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 15069*	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 15070	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	zlmlemg 15071	Lemma for zlmbasg 15072 and zlmplusgg 15073. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( E ` ndx ) =/= (Scalar ` ndx )   &    |- ( E ` ndx ) =/= ( .s ` ndx )   =>    |- ( G e. V -> ( E ` G ) = ( E ` W ) )
Theorem	zlmbasg 15072	Base set of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- B = ( Base ` G )   =>    |- ( G e. V -> B = ( Base ` W ) )
Theorem	zlmplusgg 15073	Group operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. V -> .+ = ( +g ` W ) )
Theorem	zlmmulrg 15074	Ring operation of a ZZ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- .x. = ( .r ` G )   =>    |- ( G e. V -> .x. = ( .r ` W ) )
Theorem	zlmsca 15075	Scalar ring of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
|- W = ( ZMod ` G )   =>    |- ( G e. V -> ℤring = (Scalar ` W ) )
Theorem	zlmvscag 15076	Scalar multiplication operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> .x. = ( .s ` W ) )
Theorem	znlidl 15077	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 15078	Making a commutative ring as a quotient of ZZ and n ZZ. (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 15079	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, with an "artificial" ordering added. (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 15080	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, with an "artificial" ordering added. (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 15081	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	znbaslemnn 15082	Lemma for znbas 15087. (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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( E ` ndx ) =/= ( le ` ndx )   =>    |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) )
Theorem	znbas2 15083	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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) )
Theorem	znadd 15084	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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) )
Theorem	znmul 15085	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.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) )
Theorem	znzrh 15086	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 15087	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 15088	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> Y e. CRing )
Theorem	znzrh2 15089*	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 15090	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 15091	The ZZ ring homomorphism is a surjection onto ℤ/nℤ. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( N e. NN0 -> L : ZZ -onto-> B )
Theorem	zndvds 15092	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 15093	Special case of zndvds 15092 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 15094	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 )
Theorem	znle2 15095	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )
Theorem	znleval 15096	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   &    |- X = ( Base ` Y )   =>    |- ( N e. NN0 -> ( A .<_ B <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
Theorem	znleval2 15097	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   &    |- X = ( Base ` Y )   =>    |- ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( A .<_ B <-> ( `' F ` A ) <_ ( `' F ` B ) ) )
Theorem	znfi 15098	The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   =>    |- ( N e. NN -> B e. Fin )
Theorem	znhash 15099	The ℤ/nℤ structure has n elements. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   =>    |- ( N e. NN -> (♯ ` B ) = N )
Theorem	znidom 15100	The ℤ/nℤ structure is an integral domain when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. Prime -> Y e. IDomn )