P. 258 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25701-25800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vmage0 25701	The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴))
Theorem	chpval 25702*	Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛))
Theorem	chpf 25703	Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ ψ:ℝ⟶ℝ
Theorem	chpcl 25704	Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ)
Theorem	efchpcl 25705	The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (exp‘(ψ‘𝐴)) ∈ ℕ)
Theorem	chpge0 25706	The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (ψ‘𝐴))
Theorem	ppival 25707	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘𝐴) = (♯‘((0[,]𝐴) ∩ ℙ)))
Theorem	ppival2 25708	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℤ → (π‘𝐴) = (♯‘((2...𝐴) ∩ ℙ)))
Theorem	ppival2g 25709	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 2 ∈ (ℤ≥‘𝑀)) → (π‘𝐴) = (♯‘((𝑀...𝐴) ∩ ℙ)))
Theorem	ppif 25710	Domain and range of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ π:ℝ⟶ℕ0
Theorem	ppicl 25711	Real closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘𝐴) ∈ ℕ0)
Theorem	muval 25712*	The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) = if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}))))
Theorem	muval1 25713	The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑃 ∈ (ℤ≥‘2) ∧ (𝑃↑2) ∥ 𝐴) → (μ‘𝐴) = 0)
Theorem	muval2 25714*	The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) → (μ‘𝐴) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴})))
Theorem	isnsqf 25715*	Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) = 0 ↔ ∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴))
Theorem	issqf 25716*	Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1))
Theorem	sqfpc 25717	The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015.)
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt 𝐴) ≤ 1)
Theorem	dvdssqf 25718	A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → ((μ‘𝐴) ≠ 0 → (μ‘𝐵) ≠ 0))
Theorem	sqf11 25719*	A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015.)
⊢ (((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) ∧ (𝐵 ∈ ℕ ∧ (μ‘𝐵) ≠ 0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵)))
Theorem	muf 25720	The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ μ:ℕ⟶ℤ
Theorem	mucl 25721	Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) ∈ ℤ)
Theorem	sgmval 25722*	The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝑐𝐴))
Theorem	sgmval2 25723*	The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝐴))
Theorem	0sgm 25724*	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 25725	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 25726	Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℂ)
Theorem	sgmnncl 25727	Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℕ)
Theorem	mule1 25728	The Möbius function takes on values in magnitude at most 1. (Together with mucl 25721, 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 25729	The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (θ‘(⌊‘𝐴)) = (θ‘𝐴))
Theorem	chpfl 25730	The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘(⌊‘𝐴)) = (ψ‘𝐴))
Theorem	ppiprm 25731	The prime-counting function π at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = ((π‘𝐴) + 1))
Theorem	ppinprm 25732	The prime-counting function π at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = (π‘𝐴))
Theorem	chtprm 25733	The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = ((θ‘𝐴) + (log‘(𝐴 + 1))))
Theorem	chtnprm 25734	The Chebyshev function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = (θ‘𝐴))
Theorem	chpp1 25735	The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016.)
⊢ (𝐴 ∈ ℕ0 → (ψ‘(𝐴 + 1)) = ((ψ‘𝐴) + (Λ‘(𝐴 + 1))))
Theorem	chtwordi 25736	The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ≤ (θ‘𝐵))
Theorem	chpwordi 25737	The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (ψ‘𝐴) ≤ (ψ‘𝐵))
Theorem	chtdif 25738*	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 25739	The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∥ (exp‘(θ‘𝐵)))
Theorem	ppifl 25740	The prime-counting function π does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘(⌊‘𝐴)) = (π‘𝐴))
Theorem	ppip1le 25741	The prime-counting function π cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘(𝐴 + 1)) ≤ ((π‘𝐴) + 1))
Theorem	ppiwordi 25742	The prime-counting function π is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (π‘𝐴) ≤ (π‘𝐵))
Theorem	ppidif 25743	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 25744	The prime-counting function π at 1. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (π‘1) = 0
Theorem	cht1 25745	The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (θ‘1) = 0
Theorem	vma1 25746	The von Mangoldt function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (Λ‘1) = 0
Theorem	chp1 25747	The second Chebyshev function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (ψ‘1) = 0
Theorem	ppi1i 25748	Inference form of ppiprm 25731. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ (π‘𝑀) = 𝐾    &   ⊢ 𝑁 ∈ ℙ    ⇒   ⊢ (π‘𝑁) = (𝐾 + 1)
Theorem	ppi2i 25749	Inference form of ppinprm 25732. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ (π‘𝑀) = 𝐾    &   ⊢ ¬ 𝑁 ∈ ℙ    ⇒   ⊢ (π‘𝑁) = 𝐾
Theorem	ppi2 25750	The prime-counting function π at 2. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (π‘2) = 1
Theorem	ppi3 25751	The prime-counting function π at 3. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (π‘3) = 2
Theorem	cht2 25752	The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (θ‘2) = (log‘2)
Theorem	cht3 25753	The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (θ‘3) = (log‘6)
Theorem	ppinncl 25754	Closure of the prime-counting function π in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (π‘𝐴) ∈ ℕ)
Theorem	chtrpcl 25755	Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ+)
Theorem	ppieq0 25756	The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ → ((π‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	ppiltx 25757	The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (π‘𝐴) < 𝐴)
Theorem	prmorcht 25758	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 25759	Lemma for mumul 25761. A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = 0)
Theorem	mumullem2 25760	Lemma for mumul 25761. The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0)
Theorem	mumul 25761	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 25762*	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 25763*	A "diagonal commutation" of divisor sums analogous to fsum0diag 15135. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})))
Theorem	fsumdvdsdiag 25764*	A "diagonal commutation" of divisor sums analogous to fsum0diag 15135. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐴)
Theorem	fsumdvdscom 25765*	A double commutation of divisor sums based on fsumdvdsdiag 25764. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
Theorem	dvdsppwf1o 25766*	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 25767*	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 25768*	A sum commutation from Σ𝑛 ≤ 𝐴, Σ𝑑 ∥ 𝑛, 𝐵(𝑛, 𝑑) to Σ𝑑 ≤ 𝐴, Σ𝑚 ≤ 𝐴 / 𝑑, 𝐵(𝑛, 𝑑𝑚). (Contributed by Mario Carneiro, 4-May-2016.)
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶)
Theorem	fsumfldivdiaglem 25769*	Lemma for fsumfldivdiag 25770. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚))))))
Theorem	fsumfldivdiag 25770*	The right-hand side of dvdsflsumcom 25768 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 25771*	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 25773. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0))
Theorem	musumsum 25772*	Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ (𝑚 = 1 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 1 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚} ((μ‘𝑘) · 𝐵) = 𝐶)
Theorem	muinv 25773*	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 25774*	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 25775*	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 25776*	The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝐴 σ (𝑃↑𝑁)) = Σ𝑘 ∈ (0...𝑁)((𝑃↑𝑐𝐴)↑𝑘))
Theorem	0sgmppw 25777	A prime power 𝑃↑𝐾 has 𝐾 + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0) → (0 σ (𝑃↑𝐾)) = (𝐾 + 1))
Theorem	1sgmprm 25778	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 25779	The sum of the divisors of 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 17-May-2016.)
⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1))
Theorem	sgmmul 25780	The divisor function for fixed parameter 𝐴 is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) → (𝐴 σ (𝑀 · 𝑁)) = ((𝐴 σ 𝑀) · (𝐴 σ 𝑁)))
Theorem	ppiublem1 25781	Lemma for ppiub 25783. (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 25782	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 25783	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 25784	The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ≤ (log‘𝐴))
Theorem	chtlepsi 25785	The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ≤ (ψ‘𝐴))
Theorem	chprpcl 25786	Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ+)
Theorem	chpeq0 25787	The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → ((ψ‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	chteq0 25788	The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → ((θ‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	chtleppi 25789	Upper bound on the θ function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (θ‘𝐴) ≤ ((π‘𝐴) · (log‘𝐴)))
Theorem	chtublem 25790	Lemma for chtub 25791. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))
Theorem	chtub 25791	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 25792*	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 25793*	Apply fsumvma 25792 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 25794*	The logarithmic analogue of pcprod 16234. 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 25795*	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 25796*	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 25797*	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 25798*	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 25799	An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴))))
Theorem	logfacubnd 25800	A simple upper bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) ≤ (𝐴 · (log‘𝐴)))