Home | Metamath
Proof Explorer Theorem List (p. 206 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnfldneg 20501 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋) | ||
Theorem | cnfldplusf 20502 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ + = (+𝑓‘ℂfld) | ||
Theorem | cnfldsub 20503 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ − = (-g‘ℂfld) | ||
Theorem | cndrng 20504 | The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ DivRing | ||
Theorem | cnflddiv 20505 | The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ / = (/r‘ℂfld) | ||
Theorem | cnfldinv 20506 | The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋)) | ||
Theorem | cnfldmulg 20507 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | cnfldexp 20508 | 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 20509 | The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ℂfld ∈ *-Ring | ||
Theorem | xrsmgm 20510 | The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ Mgm | ||
Theorem | xrsnsgrp 20511 | The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∉ Smgrp | ||
Theorem | xrsmgmdifsgrp 20512 | 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 20498. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp) | ||
Theorem | xrs1mnd 20513 | The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 20512. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | xrs10 20514 | The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | xrs1cmn 20515 | 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 20516 | 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 20517 | The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | ||
Theorem | xrsds 20518* | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))) | ||
Theorem | xrsdsval 20519 | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵))) | ||
Theorem | xrsdsreval 20520 | 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 20521 | Lemma for xrsdsreclb 20522. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | xrsdsreclb 20522 | 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 20523* | Lemma for nn0subm 20530 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
Theorem | cnsubglem 20524* | Lemma for resubdrg 20682 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
Theorem | cnsubrglem 20525* | Lemma for resubdrg 20682 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | cnsubdrglem 20526* | Lemma for resubdrg 20682 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing) | ||
Theorem | qsubdrg 20527 | 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 20528 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ ∈ (SubRing‘ℂfld) | ||
Theorem | gzsubrg 20529 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ[i] ∈ (SubRing‘ℂfld) | ||
Theorem | nn0subm 20530 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ ℕ0 ∈ (SubMnd‘ℂfld) | ||
Theorem | rege0subm 20531 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld) | ||
Theorem | absabv 20532 | 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 20533 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅) | ||
Theorem | qsssubdrg 20534 | 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 20535 | There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ}) | ||
Theorem | cnmgpabl 20536 | 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 20537 | 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 20538* | Lemma for rpmsubg 20539 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubGrp‘𝑀) | ||
Theorem | rpmsubg 20539 | 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 20540 | Lemma for gzrngunit 20541. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑍 = (ℂfld ↾s ℤ[i]) ⇒ ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴)) | ||
Theorem | gzrngunit 20541 | 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 20542* | 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 20543* | Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 20542. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | expmhm 20544* | 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 20545 | The nonnegative integers form a semiring (commutative by subcmn 18888). (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ SRing | ||
Theorem | rge0srg 20546 | The nonnegative real numbers form a semiring (commutative by subcmn 18888). (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 20550 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 20566), and zringbas 20553 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as definition df-zring 20548 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) 20548). | ||
Syntax | zring 20547 | Extend class notation with the (unital) ring of integers. |
class ℤring | ||
Definition | df-zring 20548 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
⊢ ℤring = (ℂfld ↾s ℤ) | ||
Theorem | zringcrng 20549 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ CRing | ||
Theorem | zringring 20550 | 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 | zringabl 20551 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ Abel | ||
Theorem | zringgrp 20552 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
⊢ ℤring ∈ Grp | ||
Theorem | zringbas 20553 | 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 20554 | 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 20555 | 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 20556 | 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 20557 | The neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ 0 = (0g‘ℤring) | ||
Theorem | zring1 20558 | The multiplicative neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ 1 = (1r‘ℤring) | ||
Theorem | zringnzr 20559 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
⊢ ℤring ∈ NzRing | ||
Theorem | dvdsrzring 20560 | 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 20561 | Lemma for zringlpir 20566. 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 20562 | Lemma for zringlpir 20566. 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 20563 | Lemma for zringlpir 20566. 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 20564 | 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 20565 | 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 20566 | 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 20567 | The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.) |
⊢ ℤring ∉ DivRing | ||
Theorem | zringcyg 20568 | The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.) |
⊢ ℤring ∈ CycGrp | ||
Theorem | zringmpg 20569 | 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 20570 | 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 20571 | 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 20572 | 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 20573* | 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 20574* | 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 20575* | 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 20576* | 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 𝑅) = {𝐹}) | ||
Syntax | czrh 20577 | Map the rationals into a field, or the integers into a ring. |
class ℤRHom | ||
Syntax | czlm 20578 | Augment an abelian group with vector space operations to turn it into a ℤ-module. |
class ℤMod | ||
Syntax | cchr 20579 | Syntax for ring characteristic. |
class chr | ||
Syntax | czn 20580 | The ring of integers modulo 𝑛. |
class ℤ/nℤ | ||
Definition | df-zrh 20581 | Define the unique homomorphism from the integers into a ring. This encodes the usual notation of 𝑛 = 1r + 1r + ... + 1r for integers (see also df-mulg 18165). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟)) | ||
Definition | df-zlm 20582 | 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 = (𝑔 ∈ V ↦ ((𝑔 sSet 〈(Scalar‘ndx), ℤring〉) sSet 〈( ·𝑠 ‘ndx), (.g‘𝑔)〉)) | ||
Definition | df-chr 20583 | 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 = (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔))) | ||
Definition | df-zn 20584* | Define the ring of integers mod 𝑛. 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ℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉)) | ||
Theorem | zrhval 20585 | 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 20586* | Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))) | ||
Theorem | zrhmulg 20587 | Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 )) | ||
Theorem | zrhrhmb 20588 | The ℤRHom homomorphism is the unique ring homomorphism from 𝑍. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐹 ∈ (ℤring RingHom 𝑅) ↔ 𝐹 = 𝐿)) | ||
Theorem | zrhrhm 20589 | The ℤRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅)) | ||
Theorem | zrh1 20590 | Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 ) | ||
Theorem | zrh0 20591 | Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 ) | ||
Theorem | zrhpropd 20592* | The ℤ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (ℤRHom‘𝐾) = (ℤRHom‘𝐿)) | ||
Theorem | zlmval 20593 | 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‘ndx), ℤring〉) sSet 〈( ·𝑠 ‘ndx), · 〉)) | ||
Theorem | zlmlem 20594 | Lemma for zlmbas 20595 and zlmplusg 20596. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 5 ⇒ ⊢ (𝐸‘𝐺) = (𝐸‘𝑊) | ||
Theorem | zlmbas 20595 | Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (Base‘𝑊) | ||
Theorem | zlmplusg 20596 | Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (+g‘𝑊) | ||
Theorem | zlmmulr 20597 | Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.r‘𝐺) ⇒ ⊢ · = (.r‘𝑊) | ||
Theorem | zlmsca 20598 | Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊)) | ||
Theorem | zlmvsca 20599 | Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = ( ·𝑠 ‘𝑊) | ||
Theorem | zlmlmod 20600 | The ℤ-module operation turns an arbitrary abelian group into a left module over ℤ. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ LMod) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |