| Metamath
Proof Explorer Theorem List (p. 215 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cncrng 21401 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) Avoid ax-mulf 11235. (Revised by GG, 31-Mar-2025.) |
| ⊢ ℂfld ∈ CRing | ||
| Theorem | cncrngOLD 21402 | Obsolete version of cncrng 21401 as of 30-Apr-2025. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ℂfld ∈ CRing | ||
| Theorem | cnring 21403 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ ℂfld ∈ Ring | ||
| Theorem | xrsmcmn 21404 | The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 21421.) (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd | ||
| Theorem | cnfld0 21405 | Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ 0 = (0g‘ℂfld) | ||
| Theorem | cnfld1 21406 | One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11235. (Revised by GG, 31-Mar-2025.) |
| ⊢ 1 = (1r‘ℂfld) | ||
| Theorem | cnfld1OLD 21407 | Obsolete version of cnfld1 21406 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 21408 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋) | ||
| Theorem | cnfldplusf 21409 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ + = (+𝑓‘ℂfld) | ||
| Theorem | cnfldsub 21410 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ − = (-g‘ℂfld) | ||
| Theorem | cndrng 21411 | The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) Avoid ax-mulf 11235. (Revised by GG, 30-Apr-2025.) |
| ⊢ ℂfld ∈ DivRing | ||
| Theorem | cndrngOLD 21412 | Obsolete version of cndrng 21411 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 21413 | 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 11235. (Revised by GG, 30-Apr-2025.) |
| ⊢ / = (/r‘ℂfld) | ||
| Theorem | cnflddivOLD 21414 | Obsolete version of cnflddiv 21413 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 21415 | The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋)) | ||
| Theorem | cnfldmulg 21416 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) | ||
| Theorem | cnfldexp 21417 | 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 21418 | The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ ℂfld ∈ *-Ring | ||
| Theorem | xrsmgm 21419 | The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.) |
| ⊢ ℝ*𝑠 ∈ Mgm | ||
| Theorem | xrsnsgrp 21420 | The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.) |
| ⊢ ℝ*𝑠 ∉ Smgrp | ||
| Theorem | xrsmgmdifsgrp 21421 | 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 21404. (Contributed by AV, 30-Jan-2020.) |
| ⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp) | ||
| Theorem | xrs1mnd 21422 | The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 21421. (Contributed by Mario Carneiro, 27-Nov-2014.) |
| ⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ Mnd | ||
| Theorem | xrs10 21423 | The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 0 = (0g‘𝑅) | ||
| Theorem | xrs1cmn 21424 | 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 21425 | 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 21426 | The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | ||
| Theorem | xrsds 21427* | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))) | ||
| Theorem | xrsdsval 21428 | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵))) | ||
| Theorem | xrsdsreval 21429 | 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 21430 | Lemma for xrsdsreclb 21431. (Contributed by Mario Carneiro, 3-Sep-2015.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
| Theorem | xrsdsreclb 21431 | 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 21432* | Lemma for nn0subm 21440 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
| Theorem | cnsubglem 21433* | Lemma for resubdrg 21626 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
| Theorem | cnsubrglem 21434* | Lemma for resubdrg 21626 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) Avoid ax-mulf 11235. (Revised by GG, 30-Apr-2025.) |
| ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
| Theorem | cnsubrglemOLD 21435* | Obsolete version of cnsubrglem 21434 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 21436* | Lemma for resubdrg 21626 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing) | ||
| Theorem | qsubdrg 21437 | 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 21438 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ ℤ ∈ (SubRing‘ℂfld) | ||
| Theorem | gzsubrg 21439 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ ℤ[i] ∈ (SubRing‘ℂfld) | ||
| Theorem | nn0subm 21440 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ ℕ0 ∈ (SubMnd‘ℂfld) | ||
| Theorem | rege0subm 21441 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld) | ||
| Theorem | absabv 21442 | 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 21443 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
| ⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅) | ||
| Theorem | qsssubdrg 21444 | 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 21445 | There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
| ⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ}) | ||
| Theorem | cnmgpabl 21446 | 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 21447 | 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 21448* | Lemma for rpmsubg 21449 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.) |
| ⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubGrp‘𝑀) | ||
| Theorem | rpmsubg 21449 | 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 21450 | Lemma for gzrngunit 21451. (Contributed by Mario Carneiro, 4-Dec-2014.) |
| ⊢ 𝑍 = (ℂfld ↾s ℤ[i]) ⇒ ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴)) | ||
| Theorem | gzrngunit 21451 | 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 21452* | 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 21453* | Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 21452. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
| Theorem | expmhm 21454* | 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 21455 | The nonnegative integers form a semiring (commutative by subcmn 19855). (Contributed by Thierry Arnoux, 1-May-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ SRing | ||
| Theorem | rge0srg 21456 | The nonnegative real numbers form a semiring (commutative by subcmn 19855). (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 21460 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 21478), and zringbas 21464 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 21458 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) 21458). | ||
| Syntax | czring 21457 | Extend class notation with the (unital) ring of integers. |
| class ℤring | ||
| Definition | df-zring 21458 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
| ⊢ ℤring = (ℂfld ↾s ℤ) | ||
| Theorem | zringcrng 21459 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
| ⊢ ℤring ∈ CRing | ||
| Theorem | zringring 21460 | 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 21461 | The ring of integers is a non-unital ring. (Contributed by AV, 17-Mar-2025.) |
| ⊢ ℤring ∈ Rng | ||
| Theorem | zringabl 21462 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
| ⊢ ℤring ∈ Abel | ||
| Theorem | zringgrp 21463 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
| ⊢ ℤring ∈ Grp | ||
| Theorem | zringbas 21464 | 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 21465 | 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 21466 | The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025.) |
| ⊢ − = (-g‘ℤring) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
| Theorem | zringmulg 21467 | 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 21468 | 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 21469 | 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 21470 | 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 21471 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
| ⊢ ℤring ∈ NzRing | ||
| Theorem | dvdsrzring 21472 | 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 21473 | Lemma for zringlpir 21478. 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 21474 | Lemma for zringlpir 21478. 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 21475 | Lemma for zringlpir 21478. 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 21476 | 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 21477 | 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 21478 | 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 21479 | The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.) |
| ⊢ ℤring ∉ DivRing | ||
| Theorem | zringcyg 21480 | The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.) |
| ⊢ ℤring ∈ CycGrp | ||
| Theorem | zringsubgval 21481 | Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.) |
| ⊢ − = (-g‘ℤring) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
| Theorem | zringmpg 21482 | 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 21483 | 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 21484 | 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 21485 | 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 21486* | 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 21487* | The powers of a group element give a homomorphism from ℤ 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.) |
| ⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅)) | ||
| Theorem | mulgrhm 21488* | 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 21489* | 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 21490 | 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 21491 | 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 20570: " 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 21508), but provide the prerequisites for ring2idlqusb 21320 to show that 𝑅 is a unital ring, and for ring2idlqus1 21329 to show that 〈1, 1〉 is its ring unity. | ||
| Theorem | pzriprnglem1 21492 | Lemma 1 for pzriprng 21508: 𝑅 is a non-unital (actually a unital!) ring. (Contributed by AV, 17-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) ⇒ ⊢ 𝑅 ∈ Rng | ||
| Theorem | pzriprnglem2 21493 | Lemma 2 for pzriprng 21508: The base set of 𝑅 is the cartesian product of the integers. (Contributed by AV, 17-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) ⇒ ⊢ (Base‘𝑅) = (ℤ × ℤ) | ||
| Theorem | pzriprnglem3 21494* | Lemma 3 for pzriprng 21508: An element of 𝐼 is an ordered pair. (Contributed by AV, 18-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑥 ∈ ℤ 𝑋 = 〈𝑥, 0〉) | ||
| Theorem | pzriprnglem4 21495 | Lemma 4 for pzriprng 21508: 𝐼 is a subgroup of 𝑅. (Contributed by AV, 18-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ 𝐼 ∈ (SubGrp‘𝑅) | ||
| Theorem | pzriprnglem5 21496 | Lemma 5 for pzriprng 21508: 𝐼 is a subring of the non-unital ring 𝑅. (Contributed by AV, 18-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ 𝐼 ∈ (SubRng‘𝑅) | ||
| Theorem | pzriprnglem6 21497 | Lemma 6 for pzriprng 21508: 𝐽 has a ring unity. (Contributed by AV, 19-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ (𝑋 ∈ 𝐼 → ((〈1, 0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋)) | ||
| Theorem | pzriprnglem7 21498 | Lemma 7 for pzriprng 21508: 𝐽 is a unital ring. (Contributed by AV, 19-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ 𝐽 ∈ Ring | ||
| Theorem | pzriprnglem8 21499 | Lemma 8 for pzriprng 21508: 𝐼 resp. 𝐽 is a two-sided ideal of the non-unital ring 𝑅. (Contributed by AV, 21-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ 𝐼 ∈ (2Ideal‘𝑅) | ||
| Theorem | pzriprnglem9 21500 | Lemma 9 for pzriprng 21508: The ring unity of the ring 𝐽. (Contributed by AV, 22-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) ⇒ ⊢ 1 = 〈1, 0〉 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |