![]() |
Metamath
Proof Explorer Theorem List (p. 254 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vmaf 25301 | Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ Λ:ℕ⟶ℝ | ||
Theorem | efvmacl 25302 | The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (exp‘(Λ‘𝐴)) ∈ ℕ) | ||
Theorem | vmage0 25303 | The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴)) | ||
Theorem | chpval 25304* | Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛)) | ||
Theorem | chpf 25305 | Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ψ:ℝ⟶ℝ | ||
Theorem | chpcl 25306 | Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ) | ||
Theorem | efchpcl 25307 | The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (exp‘(ψ‘𝐴)) ∈ ℕ) | ||
Theorem | chpge0 25308 | The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (ψ‘𝐴)) | ||
Theorem | ppival 25309 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) = (♯‘((0[,]𝐴) ∩ ℙ))) | ||
Theorem | ppival2 25310 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (π‘𝐴) = (♯‘((2...𝐴) ∩ ℙ))) | ||
Theorem | ppival2g 25311 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 2 ∈ (ℤ≥‘𝑀)) → (π‘𝐴) = (♯‘((𝑀...𝐴) ∩ ℙ))) | ||
Theorem | ppif 25312 | Domain and range of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ π:ℝ⟶ℕ0 | ||
Theorem | ppicl 25313 | Real closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) ∈ ℕ0) | ||
Theorem | muval 25314* | The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) = if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴})))) | ||
Theorem | muval1 25315 | The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑃 ∈ (ℤ≥‘2) ∧ (𝑃↑2) ∥ 𝐴) → (μ‘𝐴) = 0) | ||
Theorem | muval2 25316* | The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) → (μ‘𝐴) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}))) | ||
Theorem | isnsqf 25317* | Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) = 0 ↔ ∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴)) | ||
Theorem | issqf 25318* | Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1)) | ||
Theorem | sqfpc 25319 | The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt 𝐴) ≤ 1) | ||
Theorem | dvdssqf 25320 | A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → ((μ‘𝐴) ≠ 0 → (μ‘𝐵) ≠ 0)) | ||
Theorem | sqf11 25321* | A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ (((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) ∧ (𝐵 ∈ ℕ ∧ (μ‘𝐵) ≠ 0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) | ||
Theorem | muf 25322 | The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ μ:ℕ⟶ℤ | ||
Theorem | mucl 25323 | Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) ∈ ℤ) | ||
Theorem | sgmval 25324* | The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝑐𝐴)) | ||
Theorem | sgmval2 25325* | The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝐴)) | ||
Theorem | 0sgm 25326* | The value of the sum-of-divisors function, usually denoted σ<SUB>0</SUB>(<i>n</i>). (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝐴 ∈ ℕ → (0 σ 𝐴) = (♯‘{𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴})) | ||
Theorem | sgmf 25327 | The divisor function is a function into the complex numbers. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.) |
⊢ σ :(ℂ × ℕ)⟶ℂ | ||
Theorem | sgmcl 25328 | Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℂ) | ||
Theorem | sgmnncl 25329 | Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℕ) | ||
Theorem | mule1 25330 | The Möbius function takes on values in magnitude at most 1. (Together with mucl 25323, this implies that it takes a value in {-1, 0, 1} for every positive integer.) (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (abs‘(μ‘𝐴)) ≤ 1) | ||
Theorem | chtfl 25331 | The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘(⌊‘𝐴)) = (θ‘𝐴)) | ||
Theorem | chpfl 25332 | The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘(⌊‘𝐴)) = (ψ‘𝐴)) | ||
Theorem | ppiprm 25333 | The prime-counting function π at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = ((π‘𝐴) + 1)) | ||
Theorem | ppinprm 25334 | The prime-counting function π at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = (π‘𝐴)) | ||
Theorem | chtprm 25335 | The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = ((θ‘𝐴) + (log‘(𝐴 + 1)))) | ||
Theorem | chtnprm 25336 | The Chebyshev function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = (θ‘𝐴)) | ||
Theorem | chpp1 25337 | The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016.) |
⊢ (𝐴 ∈ ℕ0 → (ψ‘(𝐴 + 1)) = ((ψ‘𝐴) + (Λ‘(𝐴 + 1)))) | ||
Theorem | chtwordi 25338 | The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ≤ (θ‘𝐵)) | ||
Theorem | chpwordi 25339 | The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (ψ‘𝐴) ≤ (ψ‘𝐵)) | ||
Theorem | chtdif 25340* | The difference of the Chebyshev function at two points sums the logarithms of the primes in an interval. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((θ‘𝑁) − (θ‘𝑀)) = Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝)) | ||
Theorem | efchtdvds 25341 | The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∥ (exp‘(θ‘𝐵))) | ||
Theorem | ppifl 25342 | The prime-counting function π does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘(⌊‘𝐴)) = (π‘𝐴)) | ||
Theorem | ppip1le 25343 | The prime-counting function π cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘(𝐴 + 1)) ≤ ((π‘𝐴) + 1)) | ||
Theorem | ppiwordi 25344 | The prime-counting function π is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (π‘𝐴) ≤ (π‘𝐵)) | ||
Theorem | ppidif 25345 | The difference of the prime-counting function π at two points counts the number of primes in an interval. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((π‘𝑁) − (π‘𝑀)) = (♯‘(((𝑀 + 1)...𝑁) ∩ ℙ))) | ||
Theorem | ppi1 25346 | The prime-counting function π at 1. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘1) = 0 | ||
Theorem | cht1 25347 | The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘1) = 0 | ||
Theorem | vma1 25348 | The von Mangoldt function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (Λ‘1) = 0 | ||
Theorem | chp1 25349 | The second Chebyshev function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (ψ‘1) = 0 | ||
Theorem | ppi1i 25350 | Inference form of ppiprm 25333. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (π‘𝑀) = 𝐾 & ⊢ 𝑁 ∈ ℙ ⇒ ⊢ (π‘𝑁) = (𝐾 + 1) | ||
Theorem | ppi2i 25351 | Inference form of ppinprm 25334. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (π‘𝑀) = 𝐾 & ⊢ ¬ 𝑁 ∈ ℙ ⇒ ⊢ (π‘𝑁) = 𝐾 | ||
Theorem | ppi2 25352 | The prime-counting function π at 2. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘2) = 1 | ||
Theorem | ppi3 25353 | The prime-counting function π at 3. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘3) = 2 | ||
Theorem | cht2 25354 | The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘2) = (log‘2) | ||
Theorem | cht3 25355 | The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘3) = (log‘6) | ||
Theorem | ppinncl 25356 | Closure of the prime-counting function π in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (π‘𝐴) ∈ ℕ) | ||
Theorem | chtrpcl 25357 | Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ+) | ||
Theorem | ppieq0 25358 | The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((π‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | ppiltx 25359 | The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (π‘𝐴) < 𝐴) | ||
Theorem | prmorcht 25360 | 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 25361 | Lemma for mumul 25363. A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = 0) | ||
Theorem | mumullem2 25362 | Lemma for mumul 25363. The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0) | ||
Theorem | mumul 25363 | 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 25364* | 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 25365* | A "diagonal commutation" of divisor sums analogous to fsum0diag 14917. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}))) | ||
Theorem | fsumdvdsdiag 25366* | A "diagonal commutation" of divisor sums analogous to fsum0diag 14917. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐴) | ||
Theorem | fsumdvdscom 25367* | A double commutation of divisor sums based on fsumdvdsdiag 25366. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) | ||
Theorem | dvdsppwf1o 25368* | 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 25369* | 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 25370* | A sum commutation from Σ𝑛 ≤ 𝐴, Σ𝑑 ∥ 𝑛, 𝐵(𝑛, 𝑑) to Σ𝑑 ≤ 𝐴, Σ𝑚 ≤ 𝐴 / 𝑑, 𝐵(𝑛, 𝑑𝑚). (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) | ||
Theorem | fsumfldivdiaglem 25371* | Lemma for fsumfldivdiag 25372. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚)))))) | ||
Theorem | fsumfldivdiag 25372* | The right-hand side of dvdsflsumcom 25370 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 25373* | 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 25375. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0)) | ||
Theorem | musumsum 25374* | Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑚 = 1 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 1 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚} ((μ‘𝑘) · 𝐵) = 𝐶) | ||
Theorem | muinv 25375* | 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 25376* | 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 25377* | 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 25378* | The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝐴 σ (𝑃↑𝑁)) = Σ𝑘 ∈ (0...𝑁)((𝑃↑𝑐𝐴)↑𝑘)) | ||
Theorem | 0sgmppw 25379 | A prime power 𝑃↑𝐾 has 𝐾 + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0) → (0 σ (𝑃↑𝐾)) = (𝐾 + 1)) | ||
Theorem | 1sgmprm 25380 | 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 25381 | The sum of the divisors of 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1)) | ||
Theorem | sgmmul 25382 | The divisor function for fixed parameter 𝐴 is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) → (𝐴 σ (𝑀 · 𝑁)) = ((𝐴 σ 𝑀) · (𝐴 σ 𝑁))) | ||
Theorem | ppiublem1 25383 | Lemma for ppiub 25385. (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 25384 | 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 25385 | 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 25386 | The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ≤ (log‘𝐴)) | ||
Theorem | chtlepsi 25387 | The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ≤ (ψ‘𝐴)) | ||
Theorem | chprpcl 25388 | Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ+) | ||
Theorem | chpeq0 25389 | The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((ψ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chteq0 25390 | The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((θ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chtleppi 25391 | Upper bound on the θ function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (θ‘𝐴) ≤ ((π‘𝐴) · (log‘𝐴))) | ||
Theorem | chtublem 25392 | Lemma for chtub 25393. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1)))) | ||
Theorem | chtub 25393 | 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 25394* | 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 25395* | Apply fsumvma 25394 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 25396* | The logarithmic analogue of pcprod 16007. 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 25397* | 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 25398* | 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 25399* | 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 25400* | 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 / 𝑘)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |