P. 143 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14201-14300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rng2idlsubgnsg 14201	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> I e. (NrmSGrp ` R ) )
Theorem	rng2idlsubg0 14202	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> ( 0g ` R ) e. I )
Theorem	2idlcpblrng 14203	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.)
|- X = ( Base ` R )   &    |- E = ( R ~QG S )   &    |- I = (2Ideal ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ S e. I /\ S e. (SubGrp ` R ) ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
Theorem	2idlcpbl 14204	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)
|- X = ( Base ` R )   &    |- E = ( R ~QG S )   &    |- I = (2Ideal ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
Theorem	qus2idrng 14205	The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 14207 analog). (Contributed by AV, 23-Feb-2025.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   =>    |- ( ( R e. Rng /\ S e. I /\ S e. (SubGrp ` R ) ) -> U e. Rng )
Theorem	qus1 14206	The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> ( U e. Ring /\ [ .1. ] ( R ~QG S ) = ( 1r ` U ) ) )
Theorem	qusring 14207	If S is a two-sided ideal in R, then U = R / S is a ring, called the quotient ring of R by S. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> U e. Ring )
Theorem	qusrhm 14208*	If S is a two-sided ideal in R, then the "natural map" from elements to their cosets is a ring homomorphism from R to R / S. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   &    |- X = ( Base ` R )   &    |- F = ( x e. X |-> [ x ] ( R ~QG S ) )   =>    |- ( ( R e. Ring /\ S e. I ) -> F e. ( R RingHom U ) )
Theorem	qusmul2 14209	Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.)
|- Q = ( R /.s ( R ~QG I ) )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` Q )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )
Theorem	crngridl 14210	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   =>    |- ( R e. CRing -> I = (LIdeal ` O ) )
Theorem	crng2idl 14211	In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   =>    |- ( R e. CRing -> I = (2Ideal ` R ) )
Theorem	qusmulrng 14212	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14213. Similar to qusmul2 14209. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.)
|- .~ = ( R ~QG S )   &    |- H = ( R /.s .~ )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` H )   =>    |- ( ( ( R e. Rng /\ S e. (2Ideal ` R ) /\ S e. (SubGrp ` R ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	quscrng 14213	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (LIdeal ` R )   =>    |- ( ( R e. CRing /\ S e. I ) -> U e. CRing )
7.6.4  Principal ideal rings. Divisibility in the integers
Theorem	rspsn 14214*	Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` R )   &    |- K = (RSpan ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { x | G .|| x } )
7.7  The complex numbers as an algebraic extensible structure
7.7.1  Definition and basic properties
Syntax	cpsmet 14215	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 14216	Extend class notation with the class of all extended metric spaces.
class *Met
Syntax	cmet 14217	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 14218	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 14219	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 14220	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 14221	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 14222	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 14223*	Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- PsMet = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-xmet 14224*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 14225, but we also allow the metric to take on the value +oo. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-met 14225*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. (Contributed by NM, 25-Aug-2006.)
|- Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )
Definition	df-bl 14226*	Define the metric space ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
Definition	df-mopn 14227	Define a function whose value is the family of open sets of a metric space. (Contributed by NM, 1-Sep-2006.)
|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
Definition	df-fbas 14228*	Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- fBas = ( w e. _V |-> { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) } )
Definition	df-fg 14229*	Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
Definition	df-metu 14230*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
Theorem	blfn 14231	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ball Fn _V
Theorem	mopnset 14232	Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ( D e. V -> ( MetOpen ` D ) e. _V )
Theorem	cndsex 14233	The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( abs o. - ) e. _V
Theorem	cntopex 14234	The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)
|- ( MetOpen ` ( abs o. - ) ) e. _V
Theorem	metuex 14235	Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( A e. V -> (metUnif ` A ) e. _V )
Syntax	ccnfld 14236	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 14237*	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 14239, cnfldadd 14242, cnfldmul 14244, cnfldcj 14245, cnfldtset 14246, cnfldle 14247, cnfldds 14248, and cnfldbas 14240. 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 14238	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 14239	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 14240	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 14241*	The addition operation of the field of complex numbers. Version of cnfldadd 14242 using maps-to notation, which does not require ax-addf 8029. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x + y ) ) = ( +g ` ℂfld )
Theorem	cnfldadd 14242	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 14243*	The multiplication operation of the field of complex numbers. Version of cnfldmul 14244 using maps-to notation, which does not require ax-mulf 8030. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) = ( .r ` ℂfld )
Theorem	cnfldmul 14244	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 14245	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 14246	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 14247	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 14237. (Revised by GG, 31-Mar-2025.)
|- <_ = ( le ` ℂfld )
Theorem	cnfldds 14248	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 14237. (Revised by GG, 31-Mar-2025.)
|- ( abs o. - ) = ( dist ` ℂfld )
Theorem	cncrng 14249	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
|- ℂfld e. CRing
Theorem	cnring 14250	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. Ring
Theorem	cnfld0 14251	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 0 = ( 0g ` ℂfld )
Theorem	cnfld1 14252	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 1 = ( 1r ` ℂfld )
Theorem	cnfldneg 14253	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 14254	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- + = ( +f ` ℂfld )
Theorem	cnfldsub 14255	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- - = ( -g ` ℂfld )
Theorem	cnfldmulg 14256	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 14257	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 14258*	Lemma for nn0subm 14263 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 14259*	Lemma for cnsubrglem 14260 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 14260*	Lemma for zsubrg 14261 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 14261	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ e. (SubRing ` ℂfld )
Theorem	gzsubrg 14262	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ[_i] e. (SubRing ` ℂfld )
Theorem	nn0subm 14263	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- NN0 e. (SubMnd ` ℂfld )
Theorem	rege0subm 14264	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( 0 [,) +oo ) e. (SubMnd ` ℂfld )
Theorem	zsssubrg 14265	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	gsumfzfsumlem0 14266*	Lemma for gsumfzfsum 14268. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> N < M )   =>    |- ( ph -> (ℂfld gsumg ( k e. ( M ... N ) |-> B ) ) = sum_ k e. ( M ... N ) B )
Theorem	gsumfzfsumlemm 14267*	Lemma for gsumfzfsum 14268. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> B e. CC )   =>    |- ( ph -> (ℂfld gsumg ( k e. ( M ... N ) |-> B ) ) = sum_ k e. ( M ... N ) B )
Theorem	gsumfzfsum 14268*	Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> B e. CC )   =>    |- ( ph -> (ℂfld gsumg ( k e. ( M ... N ) |-> B ) ) = sum_ k e. ( M ... N ) B )
Theorem	cnfldui 14269	The invertible complex numbers are exactly those apart from zero. This is recapb 8726 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 14273 it is shown that this restriction is a ring, and zringbas 14276 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 14271 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) 14271).
Syntax	czring 14270	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 14271	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
|- ℤring = (ℂfld ↾s ZZ )
Theorem	zringcrng 14272	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. CRing
Theorem	zringring 14273	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 14274	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. Abel
Theorem	zringgrp 14275	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
|- ℤring e. Grp
Theorem	zringbas 14276	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 14277	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 14278	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 14279	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 14280	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 14281	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 14282	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
|- ℤring e. NzRing
Theorem	dvdsrzring 14283	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 14284	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 14285	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 14286	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 14287*	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 14288*	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 14289*	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 14290*	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 14291	Map the rationals into a field, or the integers into a ring.
class ZRHom
Syntax	czlm 14292	Augment an abelian group with vector space operations to turn it into a ZZ-module.
class ZMod
Syntax	czn 14293	The ring of integers modulo n.
class ℤ/nℤ
Definition	df-zrh 14294	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 13374). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
Definition	df-zlm 14295	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 14296*	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 14297	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 14298	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 14299*	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 14300	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. ) )