Home | Metamath
Proof Explorer Theorem List (p. 259 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | perfect 25801* | The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer 𝑁 is a perfect number (that is, its divisor sum is 2𝑁) if and only if it is of the form 2↑(𝑝 − 1) · (2↑𝑝 − 1), where 2↑𝑝 − 1 is prime (a Mersenne prime). (It follows from this that 𝑝 is also prime.) This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → ((1 σ 𝑁) = (2 · 𝑁) ↔ ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))))) | ||
Syntax | cdchr 25802 | Extend class notation with the group of Dirichlet characters. |
class DChr | ||
Definition | df-dchr 25803* | The group of Dirichlet characters mod 𝑛 is the set of monoid homomorphisms from ℤ / 𝑛ℤ to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ DChr = (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))〉}) | ||
Theorem | dchrval 25804* | Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) ⇒ ⊢ (𝜑 → 𝐺 = {〈(Base‘ndx), 𝐷〉, 〈(+g‘ndx), ( ∘f · ↾ (𝐷 × 𝐷))〉}) | ||
Theorem | dchrbas 25805* | Base set of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥}) | ||
Theorem | dchrelbas 25806 | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋))) | ||
Theorem | dchrelbas2 25807* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))) | ||
Theorem | dchrelbas3 25808* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋:𝐵⟶ℂ ∧ (∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))))) | ||
Theorem | dchrelbasd 25809* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ (𝑘 = 𝑥 → 𝑋 = 𝐴) & ⊢ (𝑘 = 𝑦 → 𝑋 = 𝐶) & ⊢ (𝑘 = (𝑥(.r‘𝑍)𝑦) → 𝑋 = 𝐸) & ⊢ (𝑘 = (1r‘𝑍) → 𝑋 = 𝑌) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑋 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐸 = (𝐴 · 𝐶)) & ⊢ (𝜑 → 𝑌 = 1) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 𝑋, 0)) ∈ 𝐷) | ||
Theorem | dchrrcl 25810 | Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) | ||
Theorem | dchrmhm 25811 | A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) | ||
Theorem | dchrf 25812 | A Dirichlet character is a function. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝑋:𝐵⟶ℂ) | ||
Theorem | dchrelbas4 25813* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) ⇒ ⊢ (𝑋 ∈ 𝐷 ↔ (𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0))) | ||
Theorem | dchrzrh1 25814 | Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘1)) = 1) | ||
Theorem | dchrzrhcl 25815 | A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘𝐴)) ∈ ℂ) | ||
Theorem | dchrzrhmul 25816 | A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘(𝐴 · 𝐶))) = ((𝑋‘(𝐿‘𝐴)) · (𝑋‘(𝐿‘𝐶)))) | ||
Theorem | dchrplusg 25817 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → · = ( ∘f · ↾ (𝐷 × 𝐷))) | ||
Theorem | dchrmul 25818 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘f · 𝑌)) | ||
Theorem | dchrmulcl 25819 | Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷) | ||
Theorem | dchrn0 25820 | A Dirichlet character is nonzero on the units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋‘𝐴) ≠ 0 ↔ 𝐴 ∈ 𝑈)) | ||
Theorem | dchr1cl 25821* | Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 ∈ 𝐷) | ||
Theorem | dchrmulid2 25822* | Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0)) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → ( 1 · 𝑋) = 𝑋) | ||
Theorem | dchrinvcl 25823* | Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0)) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ 𝐾 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0)) ⇒ ⊢ (𝜑 → (𝐾 ∈ 𝐷 ∧ (𝐾 · 𝑋) = 1 )) | ||
Theorem | dchrabl 25824 | The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) | ||
Theorem | dchrfi 25825 | The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) | ||
Theorem | dchrghm 25826 | A Dirichlet character restricted to the unit group of ℤ/nℤ is a group homomorphism into the multiplicative group of nonzero complex numbers. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈) & ⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 GrpHom 𝑀)) | ||
Theorem | dchr1 25827 | Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ( 1 ‘𝐴) = 1) | ||
Theorem | dchreq 25828* | A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 = 𝑌 ↔ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = (𝑌‘𝑘))) | ||
Theorem | dchrresb 25829 | A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑋 ↾ 𝑈) = (𝑌 ↾ 𝑈) ↔ 𝑋 = 𝑌)) | ||
Theorem | dchrabs 25830 | A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) = 1) | ||
Theorem | dchrinv 25831 | The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of 𝑋 are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) = (∗ ∘ 𝑋)) | ||
Theorem | dchrabs2 25832 | A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ≤ 1) | ||
Theorem | dchr1re 25833 | The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 :𝐵⟶ℝ) | ||
Theorem | dchrptlem1 25834* | Lemma for dchrpt 25837. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 1 = (1r‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ≠ 1 ) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈) & ⊢ · = (.g‘𝐻) & ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑈) & ⊢ (𝜑 → 𝐻dom DProd 𝑆) & ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) & ⊢ 𝑃 = (𝐻dProj𝑆) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) & ⊢ (𝜑 → 𝐼 ∈ dom 𝑊) & ⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 ) & ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) ⇒ ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (𝑇↑𝑀)) | ||
Theorem | dchrptlem2 25835* | Lemma for dchrpt 25837. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 1 = (1r‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ≠ 1 ) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈) & ⊢ · = (.g‘𝐻) & ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑈) & ⊢ (𝜑 → 𝐻dom DProd 𝑆) & ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) & ⊢ 𝑃 = (𝐻dProj𝑆) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼)))) & ⊢ (𝜑 → 𝐼 ∈ dom 𝑊) & ⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 ) & ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) | ||
Theorem | dchrptlem3 25836* | Lemma for dchrpt 25837. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 1 = (1r‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ≠ 1 ) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈) & ⊢ · = (.g‘𝐻) & ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑈) & ⊢ (𝜑 → 𝐻dom DProd 𝑆) & ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) | ||
Theorem | dchrpt 25837* | For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 1 = (1r‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) | ||
Theorem | dchrsum2 25838* | An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character 𝑋 is 0 if 𝑋 is non-principal and ϕ(𝑛) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ 𝑈 = (Unit‘𝑍) ⇒ ⊢ (𝜑 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0)) | ||
Theorem | dchrsum 25839* | An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character 𝑋 is 0 if 𝑋 is non-principal and ϕ(𝑛) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ 𝐵 = (Base‘𝑍) ⇒ ⊢ (𝜑 → Σ𝑎 ∈ 𝐵 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0)) | ||
Theorem | sumdchr2 25840* | Lemma for sumdchr 25842. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (1r‘𝑍) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)) | ||
Theorem | dchrhash 25841 | There are exactly ϕ(𝑁) Dirichlet characters modulo 𝑁. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝐷) = (ϕ‘𝑁)) | ||
Theorem | sumdchr 25842* | An orthogonality relation for Dirichlet characters: the sum of 𝑥(𝐴) for fixed 𝐴 and all 𝑥 is 0 if 𝐴 = 1 and ϕ(𝑛) otherwise. Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (1r‘𝑍) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (ϕ‘𝑁), 0)) | ||
Theorem | dchr2sum 25843* | An orthogonality relation for Dirichlet characters: the sum of 𝑋(𝑎) · ∗𝑌(𝑎) over all 𝑎 is nonzero only when 𝑋 = 𝑌. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → Σ𝑎 ∈ 𝐵 ((𝑋‘𝑎) · (∗‘(𝑌‘𝑎))) = if(𝑋 = 𝑌, (ϕ‘𝑁), 0)) | ||
Theorem | sum2dchr 25844* | An orthogonality relation for Dirichlet characters: the sum of 𝑥(𝐴) for fixed 𝐴 and all 𝑥 is 0 if 𝐴 = 1 and ϕ(𝑛) otherwise. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 ((𝑥‘𝐴) · (∗‘(𝑥‘𝐶))) = if(𝐴 = 𝐶, (ϕ‘𝑁), 0)) | ||
Theorem | bcctr 25845 | Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁)))) | ||
Theorem | pcbcctr 25846* | Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))))) | ||
Theorem | bcmono 25847 | The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵)) | ||
Theorem | bcmax 25848 | The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁)) | ||
Theorem | bcp1ctr 25849 | Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((2 · (𝑁 + 1))C(𝑁 + 1)) = (((2 · 𝑁)C𝑁) · (2 · (((2 · 𝑁) + 1) / (𝑁 + 1))))) | ||
Theorem | bclbnd 25850 | A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) | ||
Theorem | efexple 25851 | Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴))))) | ||
Theorem | bpos1lem 25852* | Lemma for bpos1 25853. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑) & ⊢ (𝑁 ∈ (ℤ≥‘𝑃) → 𝜑) & ⊢ 𝑃 ∈ ℙ & ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 · 2) = 𝐵 & ⊢ 𝐴 < 𝑃 & ⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝐴) → 𝜑) | ||
Theorem | bpos1 25853* | Bertrand's postulate, checked numerically for 𝑁 ≤ 64, using the prime sequence 2, 3, 5, 7, 13, 23, 43, 83. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≤ ;64) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) | ||
Theorem | bposlem1 25854 | An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) | ||
Theorem | bposlem2 25855 | There are no odd primes in the range (2𝑁 / 3, 𝑁] dividing the 𝑁-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 2 < 𝑃) & ⊢ (𝜑 → ((2 · 𝑁) / 3) < 𝑃) & ⊢ (𝜑 → 𝑃 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = 0) | ||
Theorem | bposlem3 25856* | Lemma for bpos 25863. Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 25855 and prmfac1 16057, respectively, and it does not have any in the range (𝑁, 2𝑁] by hypothesis, the product of the primes up through 2𝑁 / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5)) & ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) & ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3)) ⇒ ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁)) | ||
Theorem | bposlem4 25857* | Lemma for bpos 25863. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5)) & ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) & ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3)) & ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁))) ⇒ ⊢ (𝜑 → 𝑀 ∈ (3...𝐾)) | ||
Theorem | bposlem5 25858* | Lemma for bpos 25863. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5)) & ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) & ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3)) & ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁))) ⇒ ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2))) | ||
Theorem | bposlem6 25859* | Lemma for bpos 25863. By using the various bounds at our disposal, arrive at an inequality that is false for 𝑁 large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5)) & ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) & ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3)) & ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁))) ⇒ ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5)))) | ||
Theorem | bposlem7 25860* | Lemma for bpos 25863. The function 𝐹 is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛))))) & ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥)) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → (e↑2) ≤ 𝐴) & ⊢ (𝜑 → (e↑2) ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 → (𝐹‘𝐵) < (𝐹‘𝐴))) | ||
Theorem | bposlem8 25861 | Lemma for bpos 25863. Evaluate 𝐹(64) and show it is less than log2. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛))))) & ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥)) ⇒ ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)) | ||
Theorem | bposlem9 25862* | Lemma for bpos 25863. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛))))) & ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ;64 < 𝑁) & ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bpos 25863* | Bertrand's postulate: there is a prime between 𝑁 and 2𝑁 for every positive integer 𝑁. This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) | ||
If the congruence ((𝑥↑2) mod 𝑝) = (𝑛 mod 𝑝) has a solution we say that 𝑛 is a quadratic residue mod 𝑝. If the congruence has no solution we say that 𝑛 is a quadratic nonresidue mod 𝑝, see definition in [ApostolNT] p. 178. The Legendre symbol (𝑛 /L 𝑝) is defined in a way that its value is 1 if 𝑛 is a quadratic residue mod 𝑝 and -1 if 𝑛 is a quadratic nonresidue mod 𝑝 (and 0 if 𝑝 divides 𝑛), see lgsqr 25921. Originally, the Legendre symbol (𝑁 /L 𝑃) was defined for odd primes 𝑃 only (and arbitrary integers 𝑁) by Adrien-Marie Legendre in 1798, see definition in [ApostolNT] p. 179. It was generalized to be defined for any positive odd integer by Carl Gustav Jacob Jacobi in 1837 (therefore called "Jacobi symbol" since then), see definition in [ApostolNT] p. 188. Finally, it was generalized to be defined for any integer by Leopold Kronecker in 1885 (therefore called "Kronecker symbol" since then). The definition df-lgs 25865 for the "Legendre symbol" /L is actually the definition of the "Kronecker symbol". Since only one definition (and one class symbol) are provided in set.mm, the names "Legendre symbol", "Jacobi symbol" and "Kronecker symbol" are used synonymously for /L, but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol". | ||
Syntax | clgs 25864 | Extend class notation with the Legendre symbol function. |
class /L | ||
Definition | df-lgs 25865* | Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in [ApostolNT] p. 179 resp. definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ /L = (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛))))) | ||
Theorem | zabsle1 25866 | {-1, 0, 1} is the set of all integers with absolute value at most 1. (Contributed by AV, 13-Jul-2021.) |
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ {-1, 0, 1} ↔ (abs‘𝑍) ≤ 1)) | ||
Theorem | lgslem1 25867 | When 𝑎 is coprime to the prime 𝑝, 𝑎↑((𝑝 − 1) / 2) is equivalent mod 𝑝 to 1 or -1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2}) | ||
Theorem | lgslem2 25868 | The set 𝑍 of all integers with absolute value at most 1 contains {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ (-1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍) | ||
Theorem | lgslem3 25869* | The set 𝑍 of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ ((𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑍) → (𝐴 · 𝐵) ∈ 𝑍) | ||
Theorem | lgslem4 25870* | Lemma for lgsfcl2 25873. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.) |
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) | ||
Theorem | lgsval 25871* | Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))) | ||
Theorem | lgsfval 25872* | Value of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1)) | ||
Theorem | lgsfcl2 25873* | The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 25866). (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) & ⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶𝑍) | ||
Theorem | lgscllem 25874* | The Legendre symbol is an element of 𝑍. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) & ⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍) | ||
Theorem | lgsfcl 25875* | Closure of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ) | ||
Theorem | lgsfle1 25876* | The function 𝐹 has magnitude less or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑀 ∈ ℕ) → (abs‘(𝐹‘𝑀)) ≤ 1) | ||
Theorem | lgsval2lem 25877* | Lemma for lgsval2 25883. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ) → (𝐴 /L 𝑁) = if(𝑁 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑁 − 1) / 2)) + 1) mod 𝑁) − 1))) | ||
Theorem | lgsval4lem 25878* | Lemma for lgsval4 25887. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))) | ||
Theorem | lgscl2 25879* | The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍) | ||
Theorem | lgs0 25880 | The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0)) | ||
Theorem | lgscl 25881 | The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ) | ||
Theorem | lgsle1 25882 | The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 25881 this implies that it takes values in {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴 /L 𝑁)) ≤ 1) | ||
Theorem | lgsval2 25883 | The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime 2). (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝐴 /L 𝑃) = if(𝑃 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))) | ||
Theorem | lgs2 25884 | The Legendre symbol at 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (𝐴 ∈ ℤ → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1))) | ||
Theorem | lgsval3 25885 | The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝐴 /L 𝑃) = ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) | ||
Theorem | lgsvalmod 25886 | The Legendre symbol is equivalent to 𝑎↑((𝑝 − 1) / 2), mod 𝑝. This theorem is also called "Euler's criterion", see theorem 9.2 in [ApostolNT] p. 180, or a representation of Euler's criterion using the Legendre symbol, see also lgsqr 25921. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) | ||
Theorem | lgsval4 25887* | Restate lgsval 25871 for nonzero 𝑁, where the function 𝐹 has been abbreviated into a self-referential expression taking the value of /L on the primes as given. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) | ||
Theorem | lgsfcl3 25888* | Closure of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ) | ||
Theorem | lgsval4a 25889* | Same as lgsval4 25887 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁)) | ||
Theorem | lgscl1 25890 | The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ {-1, 0, 1}) | ||
Theorem | lgsneg 25891 | The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L -𝑁) = (if(𝐴 < 0, -1, 1) · (𝐴 /L 𝑁))) | ||
Theorem | lgsneg1 25892 | The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → (𝐴 /L -𝑁) = (𝐴 /L 𝑁)) | ||
Theorem | lgsmod 25893 | The Legendre (Jacobi) symbol is preserved under reduction mod 𝑛 when 𝑛 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁)) | ||
Theorem | lgsdilem 25894 | Lemma for lgsdi 25904 and lgsdir 25902: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1))) | ||
Theorem | lgsdir2lem1 25895 | Lemma for lgsdir2 25900. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((1 mod 8) = 1 ∧ (-1 mod 8) = 7) ∧ ((3 mod 8) = 3 ∧ (-3 mod 8) = 5)) | ||
Theorem | lgsdir2lem2 25896 | Lemma for lgsdir2 25900. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (𝐾 ∈ ℤ ∧ 2 ∥ (𝐾 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...𝐾) → (𝐴 mod 8) ∈ 𝑆))) & ⊢ 𝑀 = (𝐾 + 1) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ 𝑁 ∈ 𝑆 ⇒ ⊢ (𝑁 ∈ ℤ ∧ 2 ∥ (𝑁 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...𝑁) → (𝐴 mod 8) ∈ 𝑆))) | ||
Theorem | lgsdir2lem3 25897 | Lemma for lgsdir2 25900. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5})) | ||
Theorem | lgsdir2lem4 25898 | Lemma for lgsdir2 25900. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7})) | ||
Theorem | lgsdir2lem5 25899 | Lemma for lgsdir2 25900. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7}) | ||
Theorem | lgsdir2 25900 | The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |