Home | Metamath
Proof Explorer Theorem List (p. 258 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 | sgmppw 25701* | The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝐴 σ (𝑃↑𝑁)) = Σ𝑘 ∈ (0...𝑁)((𝑃↑𝑐𝐴)↑𝑘)) | ||
Theorem | 0sgmppw 25702 | A prime power 𝑃↑𝐾 has 𝐾 + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0) → (0 σ (𝑃↑𝐾)) = (𝐾 + 1)) | ||
Theorem | 1sgmprm 25703 | The sum of divisors for a prime is 𝑃 + 1 because the only divisors are 1 and 𝑃. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ (𝑃 ∈ ℙ → (1 σ 𝑃) = (𝑃 + 1)) | ||
Theorem | 1sgm2ppw 25704 | The sum of the divisors of 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1)) | ||
Theorem | sgmmul 25705 | The divisor function for fixed parameter 𝐴 is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) → (𝐴 σ (𝑀 · 𝑁)) = ((𝐴 σ 𝑀) · (𝐴 σ 𝑁))) | ||
Theorem | ppiublem1 25706 | Lemma for ppiub 25708. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ (𝑁 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (𝑁...5) → (𝑃 mod 6) ∈ {1, 5}))) & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (2 ∥ 𝑀 ∨ 3 ∥ 𝑀 ∨ 𝑀 ∈ {1, 5}) ⇒ ⊢ (𝑀 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (𝑀...5) → (𝑃 mod 6) ∈ {1, 5}))) | ||
Theorem | ppiublem2 25707 | A prime greater than 3 does not divide 2 or 3, so its residue mod 6 is 1 or 5. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → (𝑃 mod 6) ∈ {1, 5}) | ||
Theorem | ppiub 25708 | An upper bound on the prime-counting function π, which counts the number of primes less than 𝑁. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2)) | ||
Theorem | vmalelog 25709 | The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ≤ (log‘𝐴)) | ||
Theorem | chtlepsi 25710 | The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ≤ (ψ‘𝐴)) | ||
Theorem | chprpcl 25711 | Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ+) | ||
Theorem | chpeq0 25712 | The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((ψ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chteq0 25713 | The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((θ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chtleppi 25714 | Upper bound on the θ function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (θ‘𝐴) ≤ ((π‘𝐴) · (log‘𝐴))) | ||
Theorem | chtublem 25715 | Lemma for chtub 25716. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1)))) | ||
Theorem | chtub 25716 | An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014.) (Revised 22-Sep-2014.) |
⊢ ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3))) | ||
Theorem | fsumvma 25717* | Rewrite a sum over the von Mangoldt function as a sum over prime powers. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝑥 = (𝑝↑𝑘) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑃 ∈ Fin) & ⊢ (𝜑 → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ 𝐴))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (Λ‘𝑥) = 0)) → 𝐵 = 0) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑝 ∈ 𝑃 Σ𝑘 ∈ 𝐾 𝐶) | ||
Theorem | fsumvma2 25718* | Apply fsumvma 25717 for the common case of all numbers less than a real number 𝐴. (Contributed by Mario Carneiro, 30-Apr-2016.) |
⊢ (𝑥 = (𝑝↑𝑘) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑥) = 0)) → 𝐵 = 0) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ (1...(⌊‘𝐴))𝐵 = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))𝐶) | ||
Theorem | pclogsum 25719* | The logarithmic analogue of pcprod 16221. The sum of the logarithms of the primes dividing 𝐴 multiplied by their powers yields the logarithm of 𝐴. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝)) = (log‘𝐴)) | ||
Theorem | vmasum 25720* | The sum of the von Mangoldt function over the divisors of 𝑛. Equation 9.2.4 of [Shapiro], p. 328 and theorem 2.10 in [ApostolNT] p. 32. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} (Λ‘𝑛) = (log‘𝐴)) | ||
Theorem | logfac2 25721* | Another expression for the logarithm of a factorial, in terms of the von Mangoldt function. Equation 9.2.7 of [Shapiro], p. 329. (Contributed by Mario Carneiro, 15-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) | ||
Theorem | chpval2 25722* | Express the second Chebyshev function directly as a sum over the primes less than 𝐴 (instead of indirectly through the von Mangoldt function). (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) | ||
Theorem | chpchtsum 25723* | The second Chebyshev function is the sum of the theta function at arguments quickly approaching zero. (This is usually stated as an infinite sum, but after a certain point, the terms are all zero, and it is easier for us to use an explicit finite sum.) (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑘 ∈ (1...(⌊‘𝐴))(θ‘(𝐴↑𝑐(1 / 𝑘)))) | ||
Theorem | chpub 25724 | An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴)))) | ||
Theorem | logfacubnd 25725 | A simple upper bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) ≤ (𝐴 · (log‘𝐴))) | ||
Theorem | logfaclbnd 25726 | A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 · ((log‘𝐴) − 2)) ≤ (log‘(!‘(⌊‘𝐴)))) | ||
Theorem | logfacbnd3 25727 | Show the stronger statement log(𝑥!) = 𝑥log𝑥 − 𝑥 + 𝑂(log𝑥) alluded to in logfacrlim 25728. (Contributed by Mario Carneiro, 20-May-2016.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)) | ||
Theorem | logfacrlim 25728 | Combine the estimates logfacubnd 25725 and logfaclbnd 25726, to get log(𝑥!) = 𝑥log𝑥 + 𝑂(𝑥). Equation 9.2.9 of [Shapiro], p. 329. This is a weak form of the even stronger statement, log(𝑥!) = 𝑥log𝑥 − 𝑥 + 𝑂(log𝑥). (Contributed by Mario Carneiro, 16-Apr-2016.) (Revised by Mario Carneiro, 21-May-2016.) |
⊢ (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝𝑟 1 | ||
Theorem | logexprlim 25729* | The sum Σ𝑛 ≤ 𝑥, log↑𝑁(𝑥 / 𝑛) has the asymptotic expansion (𝑁!)𝑥 + 𝑜(𝑥). (More precisely, the omitted term has order 𝑂(log↑𝑁(𝑥) / 𝑥).) (Contributed by Mario Carneiro, 22-May-2016.) |
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁)) | ||
Theorem | logfacrlim2 25730* | Write out logfacrlim 25728 as a sum of logs. (Contributed by Mario Carneiro, 18-May-2016.) (Revised by Mario Carneiro, 22-May-2016.) |
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 | ||
Theorem | mersenne 25731 | A Mersenne prime is a prime number of the form 2↑𝑃 − 1. This theorem shows that the 𝑃 in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 𝑃 ∈ ℙ) | ||
Theorem | perfect1 25732 | Euclid's contribution to the Euclid-Euler theorem. A number of the form 2↑(𝑝 − 1) · (2↑𝑝 − 1) is a perfect number. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → (1 σ ((2↑(𝑃 − 1)) · ((2↑𝑃) − 1))) = ((2↑𝑃) · ((2↑𝑃) − 1))) | ||
Theorem | perfectlem1 25733 | Lemma for perfect 25735. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝐵) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)) | ||
Theorem | perfectlem2 25734 | Lemma for perfect 25735. (Contributed by Mario Carneiro, 17-May-2016.) Replace OLD theorem. (Revised by Wolf Lammen, 17-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝐵) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1))) | ||
Theorem | perfect 25735* | 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 25736 | Extend class notation with the group of Dirichlet characters. |
class DChr | ||
Definition | df-dchr 25737* | 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 25738* | 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 25739* | 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 25740 | 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 25741* | 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 25742* | 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 25743* | 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 25744 | Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) | ||
Theorem | dchrmhm 25745 | A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) | ||
Theorem | dchrf 25746 | A Dirichlet character is a function. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝑋:𝐵⟶ℂ) | ||
Theorem | dchrelbas4 25747* | 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 25748 | Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘1)) = 1) | ||
Theorem | dchrzrhcl 25749 | A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘𝐴)) ∈ ℂ) | ||
Theorem | dchrzrhmul 25750 | A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘(𝐴 · 𝐶))) = ((𝑋‘(𝐿‘𝐴)) · (𝑋‘(𝐿‘𝐶)))) | ||
Theorem | dchrplusg 25751 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → · = ( ∘f · ↾ (𝐷 × 𝐷))) | ||
Theorem | dchrmul 25752 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘f · 𝑌)) | ||
Theorem | dchrmulcl 25753 | Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷) | ||
Theorem | dchrn0 25754 | 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 25755* | 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 25756* | 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 25757* | 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 25758 | The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) | ||
Theorem | dchrfi 25759 | The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) | ||
Theorem | dchrghm 25760 | 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 25761 | Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ( 1 ‘𝐴) = 1) | ||
Theorem | dchreq 25762* | 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 25763 | 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 25764 | A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) = 1) | ||
Theorem | dchrinv 25765 | 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 25766 | A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ≤ 1) | ||
Theorem | dchr1re 25767 | The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 :𝐵⟶ℝ) | ||
Theorem | dchrptlem1 25768* | Lemma for dchrpt 25771. (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 25769* | Lemma for dchrpt 25771. (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 25770* | Lemma for dchrpt 25771. (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 25771* | 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 25772* | 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 25773* | 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 25774* | Lemma for sumdchr 25776. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (1r‘𝑍) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)) | ||
Theorem | dchrhash 25775 | 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 25776* | 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 25777* | 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 25778* | 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 25779 | Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁)))) | ||
Theorem | pcbcctr 25780* | Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))))) | ||
Theorem | bcmono 25781 | 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 25782 | The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁)) | ||
Theorem | bcp1ctr 25783 | 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 25784 | A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) | ||
Theorem | efexple 25785 | Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴))))) | ||
Theorem | bpos1lem 25786* | Lemma for bpos1 25787. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑) & ⊢ (𝑁 ∈ (ℤ≥‘𝑃) → 𝜑) & ⊢ 𝑃 ∈ ℙ & ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 · 2) = 𝐵 & ⊢ 𝐴 < 𝑃 & ⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝐴) → 𝜑) | ||
Theorem | bpos1 25787* | 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 25788 | 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 25789 | 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 25790* | Lemma for bpos 25797. Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 25789 and prmfac1 16053, 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 25791* | Lemma for bpos 25797. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5)) & ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) & ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3)) & ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁))) ⇒ ⊢ (𝜑 → 𝑀 ∈ (3...𝐾)) | ||
Theorem | bposlem5 25792* | Lemma for bpos 25797. 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 25793* | Lemma for bpos 25797. 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 25794* | Lemma for bpos 25797. 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 25795 | Lemma for bpos 25797. 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 25796* | Lemma for bpos 25797. 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 25797* | 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 25855. 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 25799 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 25798 | Extend class notation with the Legendre symbol function. |
class /L | ||
Definition | df-lgs 25799* | 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 25800 | {-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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |