Home | Metamath
Proof Explorer Theorem List (p. 248 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | chtrpcl 24701 | Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ+) | ||
Theorem | ppieq0 24702 | The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((π‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | ppiltx 24703 | The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (π‘𝐴) < 𝐴) | ||
Theorem | prmorcht 24704 | Relate the primorial (product of the first 𝑛 primes) to the Chebyshev function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) ⇒ ⊢ (𝐴 ∈ ℕ → (exp‘(θ‘𝐴)) = (seq1( · , 𝐹)‘𝐴)) | ||
Theorem | mumullem1 24705 | Lemma for mumul 24707. A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = 0) | ||
Theorem | mumullem2 24706 | Lemma for mumul 24707. The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0) | ||
Theorem | mumul 24707 | The Möbius function is a multiplicative function. This is one of the primary interests of the Möbius function as an arithmetic function. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → (μ‘(𝐴 · 𝐵)) = ((μ‘𝐴) · (μ‘𝐵))) | ||
Theorem | sqff1o 24708* | There is a bijection from the squarefree divisors of a number 𝑁 to the powerset of the prime divisors of 𝑁. Among other things, this implies that a number has 2↑𝑘 squarefree divisors where 𝑘 is the number of prime divisors, and a squarefree number has 2↑𝑘 divisors (because all divisors of a squarefree number are squarefree). The inverse function to 𝐹 takes the product of all the primes in some subset of prime divisors of 𝑁. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ 𝑆 = {𝑥 ∈ ℕ ∣ ((μ‘𝑥) ≠ 0 ∧ 𝑥 ∥ 𝑁)} & ⊢ 𝐹 = (𝑛 ∈ 𝑆 ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝑆–1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | ||
Theorem | fsumdvdsdiaglem 24709* | A "diagonal commutation" of divisor sums analogous to fsum0diag 14351. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}))) | ||
Theorem | fsumdvdsdiag 24710* | A "diagonal commutation" of divisor sums analogous to fsum0diag 14351. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐴) | ||
Theorem | fsumdvdscom 24711* | A double commutation of divisor sums based on fsumdvdsdiag 24710. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) | ||
Theorem | dvdsppwf1o 24712* | A bijection from the divisors of a prime power to the integers less than the prime count. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝐹 = (𝑛 ∈ (0...𝐴) ↦ (𝑃↑𝑛)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → 𝐹:(0...𝐴)–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) | ||
Theorem | dvdsflf1o 24713* | A bijection from the numbers less than 𝑁 / 𝐴 to the multiples of 𝐴 less than 𝑁. Useful for some sum manipulations. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐹 = (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ↦ (𝑁 · 𝑛)) ⇒ ⊢ (𝜑 → 𝐹:(1...(⌊‘(𝐴 / 𝑁)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) | ||
Theorem | dvdsflsumcom 24714* | A sum commutation from Σ𝑛 ≤ 𝐴, Σ𝑑 ∥ 𝑛, 𝐵(𝑛, 𝑑) to Σ𝑑 ≤ 𝐴, Σ𝑚 ≤ 𝐴 / 𝑑, 𝐵(𝑛, 𝑑𝑚). (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) | ||
Theorem | fsumfldivdiaglem 24715* | Lemma for fsumfldivdiag 24716. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚)))))) | ||
Theorem | fsumfldivdiag 24716* | The right-hand side of dvdsflsumcom 24714 is commutative in the variables, because it can be written as the manifestly symmetric sum over those 〈𝑚, 𝑛〉 such that 𝑚 · 𝑛 ≤ 𝐴. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))𝐵 = Σ𝑚 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚)))𝐵) | ||
Theorem | musum 24717* | The sum of the Möbius function over the divisors of 𝑁 gives one if 𝑁 = 1, but otherwise always sums to zero. Theorem 2.1 in [ApostolNT] p. 25. This makes the Möbius function useful for inverting divisor sums; see also muinv 24719. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0)) | ||
Theorem | musumsum 24718* | Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑚 = 1 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 1 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚} ((μ‘𝑘) · 𝐵) = 𝐶) | ||
Theorem | muinv 24719* | The Möbius inversion formula. If 𝐺(𝑛) = Σ𝑘 ∥ 𝑛𝐹(𝑘) for every 𝑛 ∈ ℕ, then 𝐹(𝑛) = Σ𝑘 ∥ 𝑛 μ(𝑘)𝐺(𝑛 / 𝑘) = Σ𝑘 ∥ 𝑛μ(𝑛 / 𝑘)𝐺(𝑘), i.e. the Möbius function is the Dirichlet convolution inverse of the constant function 1. Theorem 2.9 in [ApostolNT] p. 32. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) & ⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐹 = (𝑚 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗))))) | ||
Theorem | dvdsmulf1o 24720* | If 𝑀 and 𝑁 are two coprime integers, multiplication forms a bijection from the set of pairs 〈𝑗, 𝑘〉 where 𝑗 ∥ 𝑀 and 𝑘 ∥ 𝑁, to the set of divisors of 𝑀 · 𝑁. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀} & ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} & ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)} ⇒ ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍) | ||
Theorem | fsumdvdsmul 24721* | Product of two divisor sums. (This is also the main part of the proof that "Σ𝑘 ∥ 𝑁𝐹(𝑘) is a multiplicative function if 𝐹 is".) (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀} & ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} & ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)} & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌)) → (𝐴 · 𝐵) = 𝐷) & ⊢ (𝑖 = (𝑗 · 𝑘) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Σ𝑗 ∈ 𝑋 𝐴 · Σ𝑘 ∈ 𝑌 𝐵) = Σ𝑖 ∈ 𝑍 𝐶) | ||
Theorem | sgmppw 24722* | The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝐴 σ (𝑃↑𝑁)) = Σ𝑘 ∈ (0...𝑁)((𝑃↑𝑐𝐴)↑𝑘)) | ||
Theorem | 0sgmppw 24723 | A prime power 𝑃↑𝐾 has 𝐾 + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0) → (0 σ (𝑃↑𝐾)) = (𝐾 + 1)) | ||
Theorem | 1sgmprm 24724 | 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 24725 | The sum of the divisors of 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1)) | ||
Theorem | sgmmul 24726 | The divisor function for fixed parameter 𝐴 is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) → (𝐴 σ (𝑀 · 𝑁)) = ((𝐴 σ 𝑀) · (𝐴 σ 𝑁))) | ||
Theorem | ppiublem1 24727 | Lemma for ppiub 24729. (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 24728 | 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 24729 | 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 24730 | The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ≤ (log‘𝐴)) | ||
Theorem | chtlepsi 24731 | The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ≤ (ψ‘𝐴)) | ||
Theorem | chprpcl 24732 | Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ+) | ||
Theorem | chpeq0 24733 | The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((ψ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chteq0 24734 | The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((θ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chtleppi 24735 | Upper bound on the θ function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (θ‘𝐴) ≤ ((π‘𝐴) · (log‘𝐴))) | ||
Theorem | chtublem 24736 | Lemma for chtub 24737. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1)))) | ||
Theorem | chtub 24737 | 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 24738* | 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 24739* | Apply fsumvma 24738 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 24740* | The logarithmic analogue of pcprod 15437. 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 24741* | 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 24742* | 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 24743* | 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 24744* | 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 24745 | An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴)))) | ||
Theorem | logfacubnd 24746 | A simple upper bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) ≤ (𝐴 · (log‘𝐴))) | ||
Theorem | logfaclbnd 24747 | A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 · ((log‘𝐴) − 2)) ≤ (log‘(!‘(⌊‘𝐴)))) | ||
Theorem | logfacbnd3 24748 | Show the stronger statement log(𝑥!) = 𝑥log𝑥 − 𝑥 + 𝑂(log𝑥) alluded to in logfacrlim 24749. (Contributed by Mario Carneiro, 20-May-2016.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)) | ||
Theorem | logfacrlim 24749 | Combine the estimates logfacubnd 24746 and logfaclbnd 24747, 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 24750* | 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 24751* | Write out logfacrlim 24749 as a sum of logs. (Contributed by Mario Carneiro, 18-May-2016.) (Revised by Mario Carneiro, 22-May-2016.) |
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 | ||
Theorem | mersenne 24752 | 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 24753 | 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 24754 | Lemma for perfect 24756. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝐵) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)) | ||
Theorem | perfectlem2 24755 | Lemma for perfect 24756. (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 24756* | 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 24757 | Extend class notation with the group of Dirichlet characters. |
class DChr | ||
Definition | df-dchr 24758* | 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), ( ∘𝑓 · ↾ (𝑏 × 𝑏))〉}) | ||
Theorem | dchrval 24759* | 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), ( ∘𝑓 · ↾ (𝐷 × 𝐷))〉}) | ||
Theorem | dchrbas 24760* | 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 24761 | 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 24762* | 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 24763* | 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 24764* | 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 24765 | Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) | ||
Theorem | dchrmhm 24766 | A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) | ||
Theorem | dchrf 24767 | A Dirichlet character is a function. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝑋:𝐵⟶ℂ) | ||
Theorem | dchrelbas4 24768* | 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 24769 | Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘1)) = 1) | ||
Theorem | dchrzrhcl 24770 | A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘𝐴)) ∈ ℂ) | ||
Theorem | dchrzrhmul 24771 | A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑋‘(𝐿‘(𝐴 · 𝐶))) = ((𝑋‘(𝐿‘𝐴)) · (𝑋‘(𝐿‘𝐶)))) | ||
Theorem | dchrplusg 24772 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → · = ( ∘𝑓 · ↾ (𝐷 × 𝐷))) | ||
Theorem | dchrmul 24773 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘𝑓 · 𝑌)) | ||
Theorem | dchrmulcl 24774 | Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ · = (+g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷) | ||
Theorem | dchrn0 24775 | 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 24776* | 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 24777* | 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 24778* | 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 24779 | The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) | ||
Theorem | dchrfi 24780 | The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) | ||
Theorem | dchrghm 24781 | 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 24782 | Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ( 1 ‘𝐴) = 1) | ||
Theorem | dchreq 24783* | 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 24784 | 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 24785 | A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) = 1) | ||
Theorem | dchrinv 24786 | 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 24787 | A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ≤ 1) | ||
Theorem | dchr1re 24788 | The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 :𝐵⟶ℝ) | ||
Theorem | dchrptlem1 24789* | Lemma for dchrpt 24792. (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 24790* | Lemma for dchrpt 24792. (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 24791* | Lemma for dchrpt 24792. (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 24792* | 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 24793* | 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 24794* | 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 24795* | Lemma for sumdchr 24797. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 1 = (1r‘𝑍) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (#‘𝐷), 0)) | ||
Theorem | dchrhash 24796 | 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 24797* | 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 24798* | 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 24799* | 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 24800 | Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |