![]() |
Metamath
Proof Explorer Theorem List (p. 267 of 478) | < 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-30149) |
![]() (30150-31672) |
![]() (31673-47754) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vmaprm 26601 | Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝑃 ∈ ℙ → (Λ‘𝑃) = (log‘𝑃)) | ||
Theorem | vmacl 26602 | Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ) | ||
Theorem | vmaf 26603 | Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ Λ:ℕ⟶ℝ | ||
Theorem | efvmacl 26604 | The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (exp‘(Λ‘𝐴)) ∈ ℕ) | ||
Theorem | vmage0 26605 | The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴)) | ||
Theorem | chpval 26606* | Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛)) | ||
Theorem | chpf 26607 | Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ψ:ℝ⟶ℝ | ||
Theorem | chpcl 26608 | Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ) | ||
Theorem | efchpcl 26609 | The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (exp‘(ψ‘𝐴)) ∈ ℕ) | ||
Theorem | chpge0 26610 | The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (ψ‘𝐴)) | ||
Theorem | ppival 26611 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) = (♯‘((0[,]𝐴) ∩ ℙ))) | ||
Theorem | ppival2 26612 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (π‘𝐴) = (♯‘((2...𝐴) ∩ ℙ))) | ||
Theorem | ppival2g 26613 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 2 ∈ (ℤ≥‘𝑀)) → (π‘𝐴) = (♯‘((𝑀...𝐴) ∩ ℙ))) | ||
Theorem | ppif 26614 | Domain and codomain of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ π:ℝ⟶ℕ0 | ||
Theorem | ppicl 26615 | Real closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) ∈ ℕ0) | ||
Theorem | muval 26616* | The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) = if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴})))) | ||
Theorem | muval1 26617 | The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑃 ∈ (ℤ≥‘2) ∧ (𝑃↑2) ∥ 𝐴) → (μ‘𝐴) = 0) | ||
Theorem | muval2 26618* | The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) → (μ‘𝐴) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}))) | ||
Theorem | isnsqf 26619* | Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) = 0 ↔ ∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴)) | ||
Theorem | issqf 26620* | Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1)) | ||
Theorem | sqfpc 26621 | The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt 𝐴) ≤ 1) | ||
Theorem | dvdssqf 26622 | A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → ((μ‘𝐴) ≠ 0 → (μ‘𝐵) ≠ 0)) | ||
Theorem | sqf11 26623* | A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ (((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) ∧ (𝐵 ∈ ℕ ∧ (μ‘𝐵) ≠ 0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) | ||
Theorem | muf 26624 | The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ μ:ℕ⟶ℤ | ||
Theorem | mucl 26625 | Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) ∈ ℤ) | ||
Theorem | sgmval 26626* | The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝑐𝐴)) | ||
Theorem | sgmval2 26627* | The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝐴)) | ||
Theorem | 0sgm 26628* | 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 26629 | 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 26630 | Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℂ) | ||
Theorem | sgmnncl 26631 | Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℕ) | ||
Theorem | mule1 26632 | The Möbius function takes on values in magnitude at most 1. (Together with mucl 26625, 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 26633 | The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘(⌊‘𝐴)) = (θ‘𝐴)) | ||
Theorem | chpfl 26634 | The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘(⌊‘𝐴)) = (ψ‘𝐴)) | ||
Theorem | ppiprm 26635 | The prime-counting function π at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = ((π‘𝐴) + 1)) | ||
Theorem | ppinprm 26636 | The prime-counting function π at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = (π‘𝐴)) | ||
Theorem | chtprm 26637 | The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = ((θ‘𝐴) + (log‘(𝐴 + 1)))) | ||
Theorem | chtnprm 26638 | The Chebyshev function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = (θ‘𝐴)) | ||
Theorem | chpp1 26639 | The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016.) |
⊢ (𝐴 ∈ ℕ0 → (ψ‘(𝐴 + 1)) = ((ψ‘𝐴) + (Λ‘(𝐴 + 1)))) | ||
Theorem | chtwordi 26640 | The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ≤ (θ‘𝐵)) | ||
Theorem | chpwordi 26641 | The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (ψ‘𝐴) ≤ (ψ‘𝐵)) | ||
Theorem | chtdif 26642* | 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 26643 | The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∥ (exp‘(θ‘𝐵))) | ||
Theorem | ppifl 26644 | The prime-counting function π does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘(⌊‘𝐴)) = (π‘𝐴)) | ||
Theorem | ppip1le 26645 | The prime-counting function π cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘(𝐴 + 1)) ≤ ((π‘𝐴) + 1)) | ||
Theorem | ppiwordi 26646 | The prime-counting function π is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (π‘𝐴) ≤ (π‘𝐵)) | ||
Theorem | ppidif 26647 | 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 26648 | The prime-counting function π at 1. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘1) = 0 | ||
Theorem | cht1 26649 | The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘1) = 0 | ||
Theorem | vma1 26650 | The von Mangoldt function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (Λ‘1) = 0 | ||
Theorem | chp1 26651 | The second Chebyshev function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (ψ‘1) = 0 | ||
Theorem | ppi1i 26652 | Inference form of ppiprm 26635. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (π‘𝑀) = 𝐾 & ⊢ 𝑁 ∈ ℙ ⇒ ⊢ (π‘𝑁) = (𝐾 + 1) | ||
Theorem | ppi2i 26653 | Inference form of ppinprm 26636. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (π‘𝑀) = 𝐾 & ⊢ ¬ 𝑁 ∈ ℙ ⇒ ⊢ (π‘𝑁) = 𝐾 | ||
Theorem | ppi2 26654 | The prime-counting function π at 2. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘2) = 1 | ||
Theorem | ppi3 26655 | The prime-counting function π at 3. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘3) = 2 | ||
Theorem | cht2 26656 | The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘2) = (log‘2) | ||
Theorem | cht3 26657 | The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘3) = (log‘6) | ||
Theorem | ppinncl 26658 | Closure of the prime-counting function π in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (π‘𝐴) ∈ ℕ) | ||
Theorem | chtrpcl 26659 | Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ+) | ||
Theorem | ppieq0 26660 | The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((π‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | ppiltx 26661 | The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (π‘𝐴) < 𝐴) | ||
Theorem | prmorcht 26662 | 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 26663 | Lemma for mumul 26665. A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = 0) | ||
Theorem | mumullem2 26664 | Lemma for mumul 26665. The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0) | ||
Theorem | mumul 26665 | 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 26666* | 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 26667* | A "diagonal commutation" of divisor sums analogous to fsum0diag 15719. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}))) | ||
Theorem | fsumdvdsdiag 26668* | A "diagonal commutation" of divisor sums analogous to fsum0diag 15719. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐴) | ||
Theorem | fsumdvdscom 26669* | A double commutation of divisor sums based on fsumdvdsdiag 26668. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) | ||
Theorem | dvdsppwf1o 26670* | 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 26671* | 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 26672* | A sum commutation from Σ𝑛 ≤ 𝐴, Σ𝑑 ∥ 𝑛, 𝐵(𝑛, 𝑑) to Σ𝑑 ≤ 𝐴, Σ𝑚 ≤ 𝐴 / 𝑑, 𝐵(𝑛, 𝑑𝑚). (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) | ||
Theorem | fsumfldivdiaglem 26673* | Lemma for fsumfldivdiag 26674. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚)))))) | ||
Theorem | fsumfldivdiag 26674* | The right-hand side of dvdsflsumcom 26672 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 26675* | 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 26677. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0)) | ||
Theorem | musumsum 26676* | Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑚 = 1 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 1 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚} ((μ‘𝑘) · 𝐵) = 𝐶) | ||
Theorem | muinv 26677* | 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 26678* | 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 26679* | 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 26680* | The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝐴 σ (𝑃↑𝑁)) = Σ𝑘 ∈ (0...𝑁)((𝑃↑𝑐𝐴)↑𝑘)) | ||
Theorem | 0sgmppw 26681 | A prime power 𝑃↑𝐾 has 𝐾 + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0) → (0 σ (𝑃↑𝐾)) = (𝐾 + 1)) | ||
Theorem | 1sgmprm 26682 | 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 26683 | The sum of the divisors of 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1)) | ||
Theorem | sgmmul 26684 | The divisor function for fixed parameter 𝐴 is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) → (𝐴 σ (𝑀 · 𝑁)) = ((𝐴 σ 𝑀) · (𝐴 σ 𝑁))) | ||
Theorem | ppiublem1 26685 | Lemma for ppiub 26687. (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 26686 | 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 26687 | 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 26688 | The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ≤ (log‘𝐴)) | ||
Theorem | chtlepsi 26689 | The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ≤ (ψ‘𝐴)) | ||
Theorem | chprpcl 26690 | Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ+) | ||
Theorem | chpeq0 26691 | The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((ψ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chteq0 26692 | The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → ((θ‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | chtleppi 26693 | Upper bound on the θ function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (θ‘𝐴) ≤ ((π‘𝐴) · (log‘𝐴))) | ||
Theorem | chtublem 26694 | Lemma for chtub 26695. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1)))) | ||
Theorem | chtub 26695 | 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 26696* | 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 26697* | Apply fsumvma 26696 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 26698* | The logarithmic analogue of pcprod 16824. 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 26699* | 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 26700* | 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...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |