Home | Metamath
Proof Explorer Theorem List (p. 199 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nn0subm 19801 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
SubMndℂfld | ||
Theorem | rege0subm 19802 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
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.) |
AbsValℂfld | ||
Theorem | zsssubrg 19804 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
SubRingℂfld | ||
Theorem | qsssubdrg 19805 | The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
SubRingℂfld ℂfld ↾s | ||
Theorem | cnsubrg 19806 | There are no subrings of the complex numbers strictly between and . (Contributed by Mario Carneiro, 15-Oct-2015.) |
SubRingℂfld | ||
Theorem | cnmgpabl 19807 | The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.) |
mulGrpℂfld ↾s | ||
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.) |
mulGrpℂfld ↾s | ||
Theorem | cnmsubglem 19809* | Lemma for rpmsubg 19810 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.) |
mulGrpℂfld ↾s SubGrp | ||
Theorem | rpmsubg 19810 | The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015.) |
mulGrpℂfld ↾s SubGrp | ||
Theorem | gzrngunitlem 19811 | Lemma for gzrngunit 19812. (Contributed by Mario Carneiro, 4-Dec-2014.) |
ℂfld ↾s Unit | ||
Theorem | gzrngunit 19812 | The units on are the gaussian integers with norm . (Contributed by Mario Carneiro, 4-Dec-2014.) |
ℂfld ↾s Unit | ||
Theorem | gsumfsum 19813* | Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.) |
ℂfld g | ||
Theorem | regsumfsum 19814* | Relate a group sum on ℂfld ↾s to a finite sum on the reals. Cf. gsumfsum 19813. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
ℂfld ↾s g | ||
Theorem | expmhm 19815* | Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) |
ℂfld ↾s mulGrpℂfld MndHom | ||
Theorem | nn0srg 19816 | The nonnegative integers form a semiring (commutative by subcmn 18242). (Contributed by Thierry Arnoux, 1-May-2018.) |
ℂfld ↾s SRing | ||
Theorem | rge0srg 19817 | The nonnegative real numbers form a semiring (commutative by subcmn 18242). (Contributed by Thierry Arnoux, 6-Sep-2018.) |
ℂfld ↾s SRing | ||
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 ." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by ℂfld ↾s , 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. |
ℤring | ||
Definition | df-zring 19819 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
ℤring ℂfld ↾s | ||
Theorem | zringcrng 19820 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
ℤring | ||
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 | ||
Theorem | zringabl 19822 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
ℤring | ||
Theorem | zringgrp 19823 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
ℤring | ||
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.) |
ℤ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.) |
ℤ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.) |
.gℤring | ||
Theorem | zringmulr 19827 | The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
ℤ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.) |
ℤ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.) |
ℤring | ||
Theorem | zringnzr 19830 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
ℤring NzRing | ||
Theorem | dvdsrzring 19831 | Ring divisibility in the ring of integers corresponds to ordinary divisibility in . (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.) |
LIdealℤring | ||
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.) |
LIdealℤring inf | ||
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.) |
LIdealℤring inf | ||
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.) |
ℤring | ||
Theorem | zringunit 19836 | The units of are the integers with norm , i.e. and . (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
Unitℤring | ||
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 LPIR | ||
Theorem | zringndrg 19838 | The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.) |
ℤring | ||
Theorem | zringcyg 19839 | The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.) |
ℤring 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 mulGrpℤring | ||
Theorem | prmirredlem 19841 | A positive integer is irreducible over iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
Irredℤring | ||
Theorem | dfprm2 19842 | The positive irreducible elements of are the prime numbers. This is an alternative way to define . (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
Irredℤring | ||
Theorem | prmirred 19843 | The irreducible elements of are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
Irredℤring | ||
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.) |
mulGrpℂfld ↾s ℤring | ||
Theorem | mulgghm2 19845* | The powers of a group element give a homomorphism from to a group. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
.g ℤring | ||
Theorem | mulgrhm 19846* | The powers of the element give a ring homomorphism from to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
.g ℤring RingHom | ||
Theorem | mulgrhm2 19847* | The powers of the element give the unique ring homomorphism from to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
.g ℤring RingHom | ||
Syntax | czrh 19848 | Map the rationals into a field, or the integers into a ring. |
RHom | ||
Syntax | czlm 19849 | Augment an abelian group with vector space operations to turn it into a -module. |
Mod | ||
Syntax | cchr 19850 | Syntax for ring characteristic. |
chr | ||
Syntax | czn 19851 | The ring of integers modulo . |
ℤ/nℤ | ||
Definition | df-zrh 19852 | Define the unique homomorphism from the integers into a ring. This encodes the usual notation of for integers (see also df-mulg 17541). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
RHom ℤring RingHom | ||
Definition | df-zlm 19853 | Augment an abelian group with vector space operations to turn it into a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
Mod sSet Scalar ℤring sSet .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 | ||
Definition | df-zn 19855* | Define the ring of integers . This is literally the quotient ring of by the ideal , but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
ℤ/nℤ ℤring s ~QG RSpan sSet RHom ..^ | ||
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.) |
RHom ℤring RingHom | ||
Theorem | zrhval2 19857* | Alternate value of the RHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
RHom .g | ||
Theorem | zrhmulg 19858 | Value of the RHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.) |
RHom .g | ||
Theorem | zrhrhmb 19859 | The RHom homomorphism is the unique ring homomorphism from . (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
RHom ℤring RingHom | ||
Theorem | zrhrhm 19860 | The RHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
RHom ℤring RingHom | ||
Theorem | zrh1 19861 | Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
RHom | ||
Theorem | zrh0 19862 | Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
RHom | ||
Theorem | zrhpropd 19863* | The ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.) |
RHom RHom | ||
Theorem | zlmval 19864 | Augment an abelian group with vector space operations to turn it into a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
Mod .g sSet Scalar ℤring sSet | ||
Theorem | zlmlem 19865 | Lemma for zlmbas 19866 and zlmplusg 19867. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Mod Slot | ||
Theorem | zlmbas 19866 | Base set of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Mod | ||
Theorem | zlmplusg 19867 | Group operation of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Mod | ||
Theorem | zlmmulr 19868 | Ring operation of a -module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) |
Mod | ||
Theorem | zlmsca 19869 | Scalar ring of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
Mod ℤring Scalar | ||
Theorem | zlmvsca 19870 | Scalar multiplication operation of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Mod .g | ||
Theorem | zlmlmod 19871 | The -module operation turns an arbitrary abelian group into a left module over . (Contributed by Mario Carneiro, 2-Oct-2015.) |
Mod | ||
Theorem | zlmassa 19872 | The -module operation turns a ring into an associative algebra over . (Contributed by Mario Carneiro, 2-Oct-2015.) |
Mod AssAlg | ||
Theorem | chrval 19873 | Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
chr | ||
Theorem | chrcl 19874 | Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
chr | ||
Theorem | chrid 19875 | The canonical ring homomorphism applied to a ring's characteristic is zero. (Contributed by Mario Carneiro, 23-Sep-2015.) |
chr RHom | ||
Theorem | chrdvds 19876 | The ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
chr RHom | ||
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.) |
chr RHom | ||
Theorem | chrnzr 19878 | Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
NzRing chr | ||
Theorem | chrrhm 19879 | The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
RingHom chr chr | ||
Theorem | domnchr 19880 | The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Domn chr chr | ||
Theorem | znlidl 19881 | The set is an ideal in . (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring LIdealℤring | ||
Theorem | zncrng2 19882 | The value of the ℤ/nℤ structure. It is defined as the quotient ring , with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤring s ℤring ~QG | ||
Theorem | znval 19883 | The value of the ℤ/nℤ structure. It is defined as the quotient ring , with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ RHom ..^ sSet | ||
Theorem | znle 19884 | The value of the ℤ/nℤ structure. It is defined as the quotient ring , with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ RHom ..^ | ||
Theorem | znval2 19885 | Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ sSet | ||
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.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ Slot ; | ||
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.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ Slot | ||
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.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ | ||
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.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ | ||
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.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ | ||
Theorem | znzrh 19891 | The ring homomorphism of ℤ/nℤ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤring s ℤring ~QG ℤ/nℤ RHom RHom | ||
Theorem | znbas 19892 | The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤ/nℤ ℤring ~QG | ||
Theorem | zncrng 19893 | ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ | ||
Theorem | znzrh2 19894* | The ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤring ~QG ℤ/nℤ RHom | ||
Theorem | znzrhval 19895 | The ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
RSpanℤring ℤring ~QG ℤ/nℤ RHom | ||
Theorem | znzrhfo 19896 | The ring homomorphism is a surjection onto . (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ RHom | ||
Theorem | zncyg 19897 | The group is cyclic for all (including ). (Contributed by Mario Carneiro, 21-Apr-2016.) |
ℤ/nℤ CycGrp | ||
Theorem | zndvds 19898 | Express equality of equivalence classes in in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ RHom | ||
Theorem | zndvds0 19899 | Special case of zndvds 19898 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ RHom | ||
Theorem | znf1o 19900 | The function enumerates all equivalence classes in ℤ/nℤ for each . When , so we let ; otherwise enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.) |
ℤ/nℤ RHom ..^ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |