P. 147 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rng2idlsubg0 14601	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 14602	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 14603	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 14604	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 14606 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 14605	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 14606	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 14607*	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 14608	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 14609	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 14610	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 14611	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14612. Similar to qusmul2 14608. (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 14612	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 14613*	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 14614	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 14615	Extend class notation with the class of all extended metric spaces.
class *Met
Syntax	cmet 14616	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 14617	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 14618	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 14619	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 14620	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 14621	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 14622*	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 14623*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 14624, 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 14624*	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 14625*	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 14626	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 14627*	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 14628*	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 14629*	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 14630	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ball Fn _V
Theorem	mopnset 14631	Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ( D e. V -> ( MetOpen ` D ) e. _V )
Theorem	cndsex 14632	The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( abs o. - ) e. _V
Theorem	cntopex 14633	The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)
|- ( MetOpen ` ( abs o. - ) ) e. _V
Theorem	metuex 14634	Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( A e. V -> (metUnif ` A ) e. _V )
Syntax	ccnfld 14635	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 14636*	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 14638, cnfldadd 14641, cnfldmul 14643, cnfldcj 14644, cnfldtset 14645, cnfldle 14646, cnfldds 14647, and cnfldbas 14639. 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 14637	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 14638	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 14639	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 14640*	The addition operation of the field of complex numbers. Version of cnfldadd 14641 using maps-to notation, which does not require ax-addf 8197. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x + y ) ) = ( +g ` ℂfld )
Theorem	cnfldadd 14641	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 14642*	The multiplication operation of the field of complex numbers. Version of cnfldmul 14643 using maps-to notation, which does not require ax-mulf 8198. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) = ( .r ` ℂfld )
Theorem	cnfldmul 14643	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 14644	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 14645	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 14646	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 14636. (Revised by GG, 31-Mar-2025.)
|- <_ = ( le ` ℂfld )
Theorem	cnfldds 14647	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 14636. (Revised by GG, 31-Mar-2025.)
|- ( abs o. - ) = ( dist ` ℂfld )
Theorem	cncrng 14648	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
|- ℂfld e. CRing
Theorem	cnring 14649	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. Ring
Theorem	cnfld0 14650	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 0 = ( 0g ` ℂfld )
Theorem	cnfld1 14651	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 1 = ( 1r ` ℂfld )
Theorem	cnfldneg 14652	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 14653	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- + = ( +f ` ℂfld )
Theorem	cnfldsub 14654	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- - = ( -g ` ℂfld )
Theorem	cnfldmulg 14655	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 14656	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 14657*	Lemma for nn0subm 14662 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 14658*	Lemma for cnsubrglem 14659 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 14659*	Lemma for zsubrg 14660 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 14660	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ e. (SubRing ` ℂfld )
Theorem	gzsubrg 14661	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ[_i] e. (SubRing ` ℂfld )
Theorem	nn0subm 14662	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- NN0 e. (SubMnd ` ℂfld )
Theorem	rege0subm 14663	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( 0 [,) +oo ) e. (SubMnd ` ℂfld )
Theorem	zsssubrg 14664	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 14665*	Lemma for gsumfzfsum 14667. 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 14666*	Lemma for gsumfzfsum 14667. 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 14667*	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 14668	The invertible complex numbers are exactly those apart from zero. This is recapb 8893 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 14672 it is shown that this restriction is a ring, and zringbas 14675 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 14670 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) 14670).
Syntax	czring 14669	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 14670	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
|- ℤring = (ℂfld ↾s ZZ )
Theorem	zringcrng 14671	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. CRing
Theorem	zringring 14672	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 14673	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. Abel
Theorem	zringgrp 14674	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
|- ℤring e. Grp
Theorem	zringbas 14675	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 14676	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 14677	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 14678	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 14679	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 14680	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 14681	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
|- ℤring e. NzRing
Theorem	dvdsrzring 14682	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 14683	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 14684	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 14685	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 14686*	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 14687*	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 14688*	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 14689*	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 14690	Map the rationals into a field, or the integers into a ring.
class ZRHom
Syntax	czlm 14691	Augment an abelian group with vector space operations to turn it into a ZZ-module.
class ZMod
Syntax	czn 14692	The ring of integers modulo n.
class ℤ/nℤ
Definition	df-zrh 14693	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 13770). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
Definition	df-zlm 14694	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 14695*	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 14696	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 14697	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 14698*	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 14699	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 14700	Set existence for ZRHom. (Contributed by Jim Kingdon, 19-May-2025.)
|- L = ( ZRHom ` R )   =>    |- ( R e. V -> L e. _V )