Home | Metamath
Proof Explorer Theorem List (p. 257 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 | ||
Syntax | csgm 25601 | Extend class notation with the divisor function. |
class σ | ||
Definition | df-cht 25602* | Define the first Chebyshev function, which adds up the logarithms of all primes less than 𝑥, see definition in [ApostolNT] p. 75. The symbol used to represent this function is sometimes the variant greek letter theta shown here and sometimes the greek letter psi, ψ; however, this notation can also refer to the second Chebyshev function, which adds up the logarithms of prime powers instead, see df-chp 25604. See https://en.wikipedia.org/wiki/Chebyshev_function 25604 for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝)) | ||
Definition | df-vma 25603* | Define the von Mangoldt function, which gives the logarithm of the prime at a prime power, and is zero elsewhere, see definition in [ApostolNT] p. 32. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ Λ = (𝑥 ∈ ℕ ↦ ⦋{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥} / 𝑠⦌if((♯‘𝑠) = 1, (log‘∪ 𝑠), 0)) | ||
Definition | df-chp 25604* | Define the second Chebyshev function, which adds up the logarithms of the primes corresponding to the prime powers less than 𝑥, see definition in [ApostolNT] p. 75. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)) | ||
Definition | df-ppi 25605 | Define the prime π function, which counts the number of primes less than or equal to 𝑥, see definition in [ApostolNT] p. 8. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ π = (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ))) | ||
Definition | df-mu 25606* | Define the Möbius function, which is zero for non-squarefree numbers and is -1 or 1 for squarefree numbers according as to the number of prime divisors of the number is even or odd, see definition in [ApostolNT] p. 24. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ μ = (𝑥 ∈ ℕ ↦ if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥})))) | ||
Definition | df-sgm 25607* | Define the sum of positive divisors function (𝑥 σ 𝑛), which is the sum of the xth powers of the positive integer divisors of n, see definition in [ApostolNT] p. 38. For 𝑥 = 0, (𝑥 σ 𝑛) counts the number of divisors of 𝑛, i.e. (0 σ 𝑛) is the divisor function, see remark in [ApostolNT] p. 38. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ σ = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛} (𝑘↑𝑐𝑥)) | ||
Theorem | efnnfsumcl 25608* | Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (exp‘𝐵) ∈ ℕ) ⇒ ⊢ (𝜑 → (exp‘Σ𝑘 ∈ 𝐴 𝐵) ∈ ℕ) | ||
Theorem | ppisval 25609 | The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ)) | ||
Theorem | ppisval2 25610 | The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈ (ℤ≥‘𝑀)) → ((0[,]𝐴) ∩ ℙ) = ((𝑀...(⌊‘𝐴)) ∩ ℙ)) | ||
Theorem | ppifi 25611 | The set of primes less than 𝐴 is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin) | ||
Theorem | prmdvdsfi 25612* | The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin) | ||
Theorem | chtf 25613 | Domain and range of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ θ:ℝ⟶ℝ | ||
Theorem | chtcl 25614 | Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ) | ||
Theorem | chtval 25615* | Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) | ||
Theorem | efchtcl 25616 | The Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (exp‘(θ‘𝐴)) ∈ ℕ) | ||
Theorem | chtge0 25617 | The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (θ‘𝐴)) | ||
Theorem | vmaval 25618* | Value of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ 𝑆 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ⇒ ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) = if((♯‘𝑆) = 1, (log‘∪ 𝑆), 0)) | ||
Theorem | isppw 25619* | Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝐴)) | ||
Theorem | isppw2 25620* | Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | ||
Theorem | vmappw 25621 | Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (Λ‘(𝑃↑𝐾)) = (log‘𝑃)) | ||
Theorem | vmaprm 25622 | Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝑃 ∈ ℙ → (Λ‘𝑃) = (log‘𝑃)) | ||
Theorem | vmacl 25623 | Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ) | ||
Theorem | vmaf 25624 | Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ Λ:ℕ⟶ℝ | ||
Theorem | efvmacl 25625 | The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (exp‘(Λ‘𝐴)) ∈ ℕ) | ||
Theorem | vmage0 25626 | The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴)) | ||
Theorem | chpval 25627* | Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛)) | ||
Theorem | chpf 25628 | Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ψ:ℝ⟶ℝ | ||
Theorem | chpcl 25629 | Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ) | ||
Theorem | efchpcl 25630 | The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (exp‘(ψ‘𝐴)) ∈ ℕ) | ||
Theorem | chpge0 25631 | The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (ψ‘𝐴)) | ||
Theorem | ppival 25632 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) = (♯‘((0[,]𝐴) ∩ ℙ))) | ||
Theorem | ppival2 25633 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (π‘𝐴) = (♯‘((2...𝐴) ∩ ℙ))) | ||
Theorem | ppival2g 25634 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 2 ∈ (ℤ≥‘𝑀)) → (π‘𝐴) = (♯‘((𝑀...𝐴) ∩ ℙ))) | ||
Theorem | ppif 25635 | Domain and range of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ π:ℝ⟶ℕ0 | ||
Theorem | ppicl 25636 | Real closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) ∈ ℕ0) | ||
Theorem | muval 25637* | The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) = if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴})))) | ||
Theorem | muval1 25638 | The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑃 ∈ (ℤ≥‘2) ∧ (𝑃↑2) ∥ 𝐴) → (μ‘𝐴) = 0) | ||
Theorem | muval2 25639* | The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) → (μ‘𝐴) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}))) | ||
Theorem | isnsqf 25640* | Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) = 0 ↔ ∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴)) | ||
Theorem | issqf 25641* | Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1)) | ||
Theorem | sqfpc 25642 | The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt 𝐴) ≤ 1) | ||
Theorem | dvdssqf 25643 | A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → ((μ‘𝐴) ≠ 0 → (μ‘𝐵) ≠ 0)) | ||
Theorem | sqf11 25644* | A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ (((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) ∧ (𝐵 ∈ ℕ ∧ (μ‘𝐵) ≠ 0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) | ||
Theorem | muf 25645 | The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ μ:ℕ⟶ℤ | ||
Theorem | mucl 25646 | Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) ∈ ℤ) | ||
Theorem | sgmval 25647* | The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝑐𝐴)) | ||
Theorem | sgmval2 25648* | The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝐴)) | ||
Theorem | 0sgm 25649* | 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 25650 | 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 25651 | Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℂ) | ||
Theorem | sgmnncl 25652 | Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℕ) | ||
Theorem | mule1 25653 | The Möbius function takes on values in magnitude at most 1. (Together with mucl 25646, 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 25654 | The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘(⌊‘𝐴)) = (θ‘𝐴)) | ||
Theorem | chpfl 25655 | The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘(⌊‘𝐴)) = (ψ‘𝐴)) | ||
Theorem | ppiprm 25656 | The prime-counting function π at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = ((π‘𝐴) + 1)) | ||
Theorem | ppinprm 25657 | The prime-counting function π at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = (π‘𝐴)) | ||
Theorem | chtprm 25658 | The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = ((θ‘𝐴) + (log‘(𝐴 + 1)))) | ||
Theorem | chtnprm 25659 | The Chebyshev function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = (θ‘𝐴)) | ||
Theorem | chpp1 25660 | The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016.) |
⊢ (𝐴 ∈ ℕ0 → (ψ‘(𝐴 + 1)) = ((ψ‘𝐴) + (Λ‘(𝐴 + 1)))) | ||
Theorem | chtwordi 25661 | The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ≤ (θ‘𝐵)) | ||
Theorem | chpwordi 25662 | The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (ψ‘𝐴) ≤ (ψ‘𝐵)) | ||
Theorem | chtdif 25663* | 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 25664 | The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∥ (exp‘(θ‘𝐵))) | ||
Theorem | ppifl 25665 | The prime-counting function π does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘(⌊‘𝐴)) = (π‘𝐴)) | ||
Theorem | ppip1le 25666 | The prime-counting function π cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘(𝐴 + 1)) ≤ ((π‘𝐴) + 1)) | ||
Theorem | ppiwordi 25667 | The prime-counting function π is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (π‘𝐴) ≤ (π‘𝐵)) | ||
Theorem | ppidif 25668 | 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 25669 | The prime-counting function π at 1. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘1) = 0 | ||
Theorem | cht1 25670 | The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘1) = 0 | ||
Theorem | vma1 25671 | The von Mangoldt function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (Λ‘1) = 0 | ||
Theorem | chp1 25672 | The second Chebyshev function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (ψ‘1) = 0 | ||
Theorem | ppi1i 25673 | Inference form of ppiprm 25656. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (π‘𝑀) = 𝐾 & ⊢ 𝑁 ∈ ℙ ⇒ ⊢ (π‘𝑁) = (𝐾 + 1) | ||
Theorem | ppi2i 25674 | Inference form of ppinprm 25657. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (π‘𝑀) = 𝐾 & ⊢ ¬ 𝑁 ∈ ℙ ⇒ ⊢ (π‘𝑁) = 𝐾 | ||
Theorem | ppi2 25675 | The prime-counting function π at 2. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘2) = 1 | ||
Theorem | ppi3 25676 | The prime-counting function π at 3. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ (π‘3) = 2 | ||
Theorem | cht2 25677 | The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘2) = (log‘2) | ||
Theorem | cht3 25678 | The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (θ‘3) = (log‘6) | ||
Theorem | ppinncl 25679 | Closure of the prime-counting function π in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (π‘𝐴) ∈ ℕ) | ||
Theorem | chtrpcl 25680 | Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ+) | ||
Theorem | ppieq0 25681 | The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((π‘𝐴) = 0 ↔ 𝐴 < 2)) | ||
Theorem | ppiltx 25682 | The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (π‘𝐴) < 𝐴) | ||
Theorem | prmorcht 25683 | 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 25684 | Lemma for mumul 25686. A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = 0) | ||
Theorem | mumullem2 25685 | Lemma for mumul 25686. The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0) | ||
Theorem | mumul 25686 | 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 25687* | 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 25688* | A "diagonal commutation" of divisor sums analogous to fsum0diag 15122. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}))) | ||
Theorem | fsumdvdsdiag 25689* | A "diagonal commutation" of divisor sums analogous to fsum0diag 15122. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐴) | ||
Theorem | fsumdvdscom 25690* | A double commutation of divisor sums based on fsumdvdsdiag 25689. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) | ||
Theorem | dvdsppwf1o 25691* | 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 25692* | 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 25693* | A sum commutation from Σ𝑛 ≤ 𝐴, Σ𝑑 ∥ 𝑛, 𝐵(𝑛, 𝑑) to Σ𝑑 ≤ 𝐴, Σ𝑚 ≤ 𝐴 / 𝑑, 𝐵(𝑛, 𝑑𝑚). (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) | ||
Theorem | fsumfldivdiaglem 25694* | Lemma for fsumfldivdiag 25695. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚)))))) | ||
Theorem | fsumfldivdiag 25695* | The right-hand side of dvdsflsumcom 25693 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 25696* | 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 25698. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0)) | ||
Theorem | musumsum 25697* | Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ (𝑚 = 1 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 1 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚} ((μ‘𝑘) · 𝐵) = 𝐶) | ||
Theorem | muinv 25698* | 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 25699* | 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 25700* | 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) & ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀} & ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} & ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)} & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌)) → (𝐴 · 𝐵) = 𝐷) & ⊢ (𝑖 = (𝑗 · 𝑘) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Σ𝑗 ∈ 𝑋 𝐴 · Σ𝑘 ∈ 𝑌 𝐵) = Σ𝑖 ∈ 𝑍 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |