![]() |
Metamath
Proof Explorer Theorem List (p. 214 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrstset 21301 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠) | ||
Theorem | xrsle 21302 | The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ≤ = (le‘ℝ*𝑠) | ||
Theorem | cncrng 21303 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) Avoid ax-mulf 11210. (Revised by GG, 31-Mar-2025.) |
⊢ ℂfld ∈ CRing | ||
Theorem | cncrngOLD 21304 | Obsolete version of cncrng 21303 as of 30-Apr-2025. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℂfld ∈ CRing | ||
Theorem | cnring 21305 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ Ring | ||
Theorem | xrsmcmn 21306 | The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 21323.) (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd | ||
Theorem | cnfld0 21307 | Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 0 = (0g‘ℂfld) | ||
Theorem | cnfld1 21308 | One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11210. (Revised by GG, 31-Mar-2025.) |
⊢ 1 = (1r‘ℂfld) | ||
Theorem | cnfld1OLD 21309 | Obsolete version of cnfld1 21308 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 1 = (1r‘ℂfld) | ||
Theorem | cnfldneg 21310 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋) | ||
Theorem | cnfldplusf 21311 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ + = (+𝑓‘ℂfld) | ||
Theorem | cnfldsub 21312 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ − = (-g‘ℂfld) | ||
Theorem | cndrng 21313 | The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11210. (Revised by GG, 30-Apr-2025.) |
⊢ ℂfld ∈ DivRing | ||
Theorem | cndrngOLD 21314 | Obsolete version of cndrng 21313 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℂfld ∈ DivRing | ||
Theorem | cnflddiv 21315 | The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) Avoid ax-mulf 11210. (Revised by GG, 30-Apr-2025.) |
⊢ / = (/r‘ℂfld) | ||
Theorem | cnflddivOLD 21316 | Obsolete version of cnflddiv 21315 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ / = (/r‘ℂfld) | ||
Theorem | cnfldinv 21317 | The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋)) | ||
Theorem | cnfldmulg 21318 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | cnfldexp 21319 | The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐵(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑𝐵)) | ||
Theorem | cnsrng 21320 | The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ℂfld ∈ *-Ring | ||
Theorem | xrsmgm 21321 | The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ Mgm | ||
Theorem | xrsnsgrp 21322 | The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∉ Smgrp | ||
Theorem | xrsmgmdifsgrp 21323 | The "additive group" of the extended reals is a magma but not a semigroup, and therefore also not a monoid nor a group, in contrast to the "multiplicative group", see xrsmcmn 21306. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp) | ||
Theorem | xrs1mnd 21324 | The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 21323. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | xrs10 21325 | The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | xrs1cmn 21326 | The extended real numbers restricted to ℝ* ∖ {-∞} form a commutative monoid. They are not a group because 1 + +∞ = 2 + +∞ even though 1 ≠ 2. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ CMnd | ||
Theorem | xrge0subm 21327 | The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ (0[,]+∞) ∈ (SubMnd‘𝑅) | ||
Theorem | xrge0cmn 21328 | The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | ||
Theorem | xrsds 21329* | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))) | ||
Theorem | xrsdsval 21330 | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵))) | ||
Theorem | xrsdsreval 21331 | The metric of the extended real number structure coincides with the real number metric on the reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
Theorem | xrsdsreclblem 21332 | Lemma for xrsdsreclb 21333. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | xrsdsreclb 21333 | The metric of the extended real number structure is only real when both arguments are real. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) → ((𝐴𝐷𝐵) ∈ ℝ ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | cnsubmlem 21334* | Lemma for nn0subm 21342 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
Theorem | cnsubglem 21335* | Lemma for resubdrg 21527 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
Theorem | cnsubrglem 21336* | Lemma for resubdrg 21527 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) Avoid ax-mulf 11210. (Revised by GG, 30-Apr-2025.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | cnsubrglemOLD 21337* | Obsolete version of cnsubrglem 21336 as of 30-Apr-2025. (Contributed by Mario Carneiro, 4-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | cnsubdrglem 21338* | Lemma for resubdrg 21527 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing) | ||
Theorem | qsubdrg 21339 | The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing) | ||
Theorem | zsubrg 21340 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ ∈ (SubRing‘ℂfld) | ||
Theorem | gzsubrg 21341 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ[i] ∈ (SubRing‘ℂfld) | ||
Theorem | nn0subm 21342 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ ℕ0 ∈ (SubMnd‘ℂfld) | ||
Theorem | rege0subm 21343 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld) | ||
Theorem | absabv 21344 | The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ abs ∈ (AbsVal‘ℂfld) | ||
Theorem | zsssubrg 21345 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅) | ||
Theorem | qsssubdrg 21346 | The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝑅) ∈ DivRing) → ℚ ⊆ 𝑅) | ||
Theorem | cnsubrg 21347 | There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ}) | ||
Theorem | cnmgpabl 21348 | The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ⇒ ⊢ 𝑀 ∈ Abel | ||
Theorem | cnmgpid 21349 | 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 (ℂ ∖ {0})) ⇒ ⊢ (0g‘𝑀) = 1 | ||
Theorem | cnmsubglem 21350* | Lemma for rpmsubg 21351 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubGrp‘𝑀) | ||
Theorem | rpmsubg 21351 | The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ⇒ ⊢ ℝ+ ∈ (SubGrp‘𝑀) | ||
Theorem | gzrngunitlem 21352 | Lemma for gzrngunit 21353. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑍 = (ℂfld ↾s ℤ[i]) ⇒ ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴)) | ||
Theorem | gzrngunit 21353 | The units on ℤ[i] are the gaussian integers with norm 1. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑍 = (ℂfld ↾s ℤ[i]) ⇒ ⊢ (𝐴 ∈ (Unit‘𝑍) ↔ (𝐴 ∈ ℤ[i] ∧ (abs‘𝐴) = 1)) | ||
Theorem | gsumfsum 21354* | Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | regsumfsum 21355* | Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 21354. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | expmhm 21356* | Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑁 = (ℂfld ↾s ℕ0) & ⊢ 𝑀 = (mulGrp‘ℂfld) ⇒ ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀)) | ||
Theorem | nn0srg 21357 | The nonnegative integers form a semiring (commutative by subcmn 19783). (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ SRing | ||
Theorem | rge0srg 21358 | The nonnegative real numbers form a semiring (commutative by subcmn 19783). (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ (ℂfld ↾s (0[,)+∞)) ∈ 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 21362 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 21380), and zringbas 21366 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 21360 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) 21360). | ||
Syntax | czring 21359 | Extend class notation with the (unital) ring of integers. |
class ℤring | ||
Definition | df-zring 21360 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
⊢ ℤring = (ℂfld ↾s ℤ) | ||
Theorem | zringcrng 21361 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ CRing | ||
Theorem | zringring 21362 | 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 ∈ Ring | ||
Theorem | zringrng 21363 | The ring of integers is a non-unital ring. (Contributed by AV, 17-Mar-2025.) |
⊢ ℤring ∈ Rng | ||
Theorem | zringabl 21364 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ Abel | ||
Theorem | zringgrp 21365 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
⊢ ℤring ∈ Grp | ||
Theorem | zringbas 21366 | The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ ℤ = (Base‘ℤring) | ||
Theorem | zringplusg 21367 | The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ + = (+g‘ℤring) | ||
Theorem | zringsub 21368 | The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025.) |
⊢ − = (-g‘ℤring) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
Theorem | zringmulg 21369 | 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 21370 | The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ · = (.r‘ℤring) | ||
Theorem | zring0 21371 | 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 21372 | 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 21373 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
⊢ ℤring ∈ NzRing | ||
Theorem | dvdsrzring 21374 | 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 21375 | Lemma for zringlpir 21380. 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)) & ⊢ (𝜑 → 𝐼 ≠ {0}) ⇒ ⊢ (𝜑 → (𝐼 ∩ ℕ) ≠ ∅) | ||
Theorem | zringlpirlem2 21376 | Lemma for zringlpir 21380. 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)) & ⊢ (𝜑 → 𝐼 ≠ {0}) & ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐼) | ||
Theorem | zringlpirlem3 21377 | Lemma for zringlpir 21380. 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)) & ⊢ (𝜑 → 𝐼 ≠ {0}) & ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < ) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝐺 ∥ 𝑋) | ||
Theorem | zringinvg 21378 | The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ (𝐴 ∈ ℤ → -𝐴 = ((invg‘ℤring)‘𝐴)) | ||
Theorem | zringunit 21379 | The units of ℤ are the integers with norm 1, i.e. 1 and -1. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
⊢ (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1)) | ||
Theorem | zringlpir 21380 | 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 21381 | The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.) |
⊢ ℤring ∉ DivRing | ||
Theorem | zringcyg 21382 | The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.) |
⊢ ℤring ∈ CycGrp | ||
Theorem | zringsubgval 21383 | Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.) |
⊢ − = (-g‘ℤring) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
Theorem | zringmpg 21384 | 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 ℤ) = (mulGrp‘ℤring) | ||
Theorem | prmirredlem 21385 | 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 21386 | 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 21387 | 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) ⇒ ⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈ ℙ)) | ||
Theorem | expghm 21388* | 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 (ℂ ∖ {0})) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈)) | ||
Theorem | mulgghm2 21389* | 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‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅)) | ||
Theorem | mulgrhm 21390* | The powers of the element 1 give a ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐹 ∈ (ℤring RingHom 𝑅)) | ||
Theorem | mulgrhm2 21391* | The powers of the element 1 give the unique ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (ℤring RingHom 𝑅) = {𝐹}) | ||
Theorem | irinitoringc 21392 | The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ℤring ∈ 𝑈) & ⊢ 𝐶 = (RingCat‘𝑈) ⇒ ⊢ (𝜑 → ℤring ∈ (InitO‘𝐶)) | ||
Theorem | nzerooringczr 21393 | There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RingCat‘𝑈) & ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → ℤring ∈ 𝑈) ⇒ ⊢ (𝜑 → (ZeroO‘𝐶) = ∅) | ||
In this subsubsection, an example is given for a condition for a non-unital ring to be unital. This example is already mentioned in the comment for df-subrg 20497: " The subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity ⟨1, 0⟩ which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring." The theorems in this subsubsection do not assume that 𝑅 = (ℤring ×s ℤring) is a ring (which can be proven directly very easily, see pzriprng 21410), but provide the prerequisites for ring2idlqusb 21189 to show that 𝑅 is a unital ring, and for ring2idlqus1 21198 to show that ⟨1, 1⟩ is its ring unity. | ||
Theorem | pzriprnglem1 21394 | Lemma 1 for pzriprng 21410: 𝑅 is a non-unital (actually a unital!) ring. (Contributed by AV, 17-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | pzriprnglem2 21395 | Lemma 2 for pzriprng 21410: The base set of 𝑅 is the cartesian product of the integers. (Contributed by AV, 17-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) ⇒ ⊢ (Base‘𝑅) = (ℤ × ℤ) | ||
Theorem | pzriprnglem3 21396* | Lemma 3 for pzriprng 21410: An element of 𝐼 is an ordered pair. (Contributed by AV, 18-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑥 ∈ ℤ 𝑋 = ⟨𝑥, 0⟩) | ||
Theorem | pzriprnglem4 21397 | Lemma 4 for pzriprng 21410: 𝐼 is a subgroup of 𝑅. (Contributed by AV, 18-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ 𝐼 ∈ (SubGrp‘𝑅) | ||
Theorem | pzriprnglem5 21398 | Lemma 5 for pzriprng 21410: 𝐼 is a subring of the non-unital ring 𝑅. (Contributed by AV, 18-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ 𝐼 ∈ (SubRng‘𝑅) | ||
Theorem | pzriprnglem6 21399 | Lemma 6 for pzriprng 21410: 𝐽 has a ring unity. (Contributed by AV, 19-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ (𝑋 ∈ 𝐼 → ((⟨1, 0⟩(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)⟨1, 0⟩) = 𝑋)) | ||
Theorem | pzriprnglem7 21400 | Lemma 7 for pzriprng 21410: 𝐽 is a unital ring. (Contributed by AV, 19-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ 𝐽 ∈ Ring |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |