P. 271 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27001-27100   *Has distinct variable group(s)

Type	Label	Description
Statement
14.4.4  Number-theoretical functions
Syntax	ccht 27001	Extend class notation with the first Chebyshev function.
class θ
Syntax	cvma 27002	Extend class notation with the von Mangoldt function.
class Λ
Syntax	cchp 27003	Extend class notation with the second Chebyshev function.
class ψ
Syntax	cppi 27004	Extend class notation with the prime-counting function pi.
class π
Syntax	cmu 27005	Extend class notation with the Möbius function.
class μ
Syntax	csgm 27006	Extend class notation with the divisor function.
class σ
Definition	df-cht 27007*	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 27009. See https://en.wikipedia.org/wiki/Chebyshev_function 27009 for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝))
Definition	df-vma 27008*	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 27009*	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 27010	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 27011*	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 27012*	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 27013*	Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (exp‘𝐵) ∈ ℕ)    ⇒   ⊢ (𝜑 → (exp‘Σ𝑘 ∈ 𝐴 𝐵) ∈ ℕ)
Theorem	ppisval 27014	The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ))
Theorem	ppisval2 27015	The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈ (ℤ≥‘𝑀)) → ((0[,]𝐴) ∩ ℙ) = ((𝑀...(⌊‘𝐴)) ∩ ℙ))
Theorem	ppifi 27016	The set of primes less than 𝐴 is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
Theorem	prmdvdsfi 27017*	The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin)
Theorem	chtf 27018	Domain and codoamin of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ θ:ℝ⟶ℝ
Theorem	chtcl 27019	Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ)
Theorem	chtval 27020*	Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
Theorem	efchtcl 27021	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 27022	The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (θ‘𝐴))
Theorem	vmaval 27023*	Value of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ 𝑆 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}    ⇒   ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) = if((♯‘𝑆) = 1, (log‘∪ 𝑆), 0))
Theorem	isppw 27024*	Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝐴))
Theorem	isppw2 27025*	Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)))
Theorem	vmappw 27026	Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (Λ‘(𝑃↑𝐾)) = (log‘𝑃))
Theorem	vmaprm 27027	Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝑃 ∈ ℙ → (Λ‘𝑃) = (log‘𝑃))
Theorem	vmacl 27028	Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ)
Theorem	vmaf 27029	Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ Λ:ℕ⟶ℝ
Theorem	efvmacl 27030	The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → (exp‘(Λ‘𝐴)) ∈ ℕ)
Theorem	vmage0 27031	The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴))
Theorem	chpval 27032*	Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛))
Theorem	chpf 27033	Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ ψ:ℝ⟶ℝ
Theorem	chpcl 27034	Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ)
Theorem	efchpcl 27035	The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (exp‘(ψ‘𝐴)) ∈ ℕ)
Theorem	chpge0 27036	The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (ψ‘𝐴))
Theorem	ppival 27037	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘𝐴) = (♯‘((0[,]𝐴) ∩ ℙ)))
Theorem	ppival2 27038	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℤ → (π‘𝐴) = (♯‘((2...𝐴) ∩ ℙ)))
Theorem	ppival2g 27039	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 2 ∈ (ℤ≥‘𝑀)) → (π‘𝐴) = (♯‘((𝑀...𝐴) ∩ ℙ)))
Theorem	ppif 27040	Domain and codomain of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ π:ℝ⟶ℕ0
Theorem	ppicl 27041	Real closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘𝐴) ∈ ℕ0)
Theorem	muval 27042*	The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) = if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}))))
Theorem	muval1 27043	The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑃 ∈ (ℤ≥‘2) ∧ (𝑃↑2) ∥ 𝐴) → (μ‘𝐴) = 0)
Theorem	muval2 27044*	The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) → (μ‘𝐴) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴})))
Theorem	isnsqf 27045*	Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) = 0 ↔ ∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴))
Theorem	issqf 27046*	Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1))
Theorem	sqfpc 27047	The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015.)
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt 𝐴) ≤ 1)
Theorem	dvdssqf 27048	A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → ((μ‘𝐴) ≠ 0 → (μ‘𝐵) ≠ 0))
Theorem	sqf11 27049*	A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015.)
⊢ (((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) ∧ (𝐵 ∈ ℕ ∧ (μ‘𝐵) ≠ 0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵)))
Theorem	muf 27050	The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ μ:ℕ⟶ℤ
Theorem	mucl 27051	Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) ∈ ℤ)
Theorem	sgmval 27052*	The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝑐𝐴))
Theorem	sgmval2 27053*	The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝐴))
Theorem	0sgm 27054*	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 27055	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 27056	Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℂ)
Theorem	sgmnncl 27057	Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) ∈ ℕ)
Theorem	mule1 27058	The Möbius function takes on values in magnitude at most 1. (Together with mucl 27051, 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 27059	The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (θ‘(⌊‘𝐴)) = (θ‘𝐴))
Theorem	chpfl 27060	The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘(⌊‘𝐴)) = (ψ‘𝐴))
Theorem	ppiprm 27061	The prime-counting function π at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = ((π‘𝐴) + 1))
Theorem	ppinprm 27062	The prime-counting function π at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (π‘(𝐴 + 1)) = (π‘𝐴))
Theorem	chtprm 27063	The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = ((θ‘𝐴) + (log‘(𝐴 + 1))))
Theorem	chtnprm 27064	The Chebyshev function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ ¬ (𝐴 + 1) ∈ ℙ) → (θ‘(𝐴 + 1)) = (θ‘𝐴))
Theorem	chpp1 27065	The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016.)
⊢ (𝐴 ∈ ℕ0 → (ψ‘(𝐴 + 1)) = ((ψ‘𝐴) + (Λ‘(𝐴 + 1))))
Theorem	chtwordi 27066	The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ≤ (θ‘𝐵))
Theorem	chpwordi 27067	The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (ψ‘𝐴) ≤ (ψ‘𝐵))
Theorem	chtdif 27068*	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 27069	The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∥ (exp‘(θ‘𝐵)))
Theorem	ppifl 27070	The prime-counting function π does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘(⌊‘𝐴)) = (π‘𝐴))
Theorem	ppip1le 27071	The prime-counting function π cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘(𝐴 + 1)) ≤ ((π‘𝐴) + 1))
Theorem	ppiwordi 27072	The prime-counting function π is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (π‘𝐴) ≤ (π‘𝐵))
Theorem	ppidif 27073	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 27074	The prime-counting function π at 1. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (π‘1) = 0
Theorem	cht1 27075	The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (θ‘1) = 0
Theorem	vma1 27076	The von Mangoldt function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (Λ‘1) = 0
Theorem	chp1 27077	The second Chebyshev function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (ψ‘1) = 0
Theorem	ppi1i 27078	Inference form of ppiprm 27061. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ (π‘𝑀) = 𝐾    &   ⊢ 𝑁 ∈ ℙ    ⇒   ⊢ (π‘𝑁) = (𝐾 + 1)
Theorem	ppi2i 27079	Inference form of ppinprm 27062. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ (π‘𝑀) = 𝐾    &   ⊢ ¬ 𝑁 ∈ ℙ    ⇒   ⊢ (π‘𝑁) = 𝐾
Theorem	ppi2 27080	The prime-counting function π at 2. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (π‘2) = 1
Theorem	ppi3 27081	The prime-counting function π at 3. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ (π‘3) = 2
Theorem	cht2 27082	The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (θ‘2) = (log‘2)
Theorem	cht3 27083	The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (θ‘3) = (log‘6)
Theorem	ppinncl 27084	Closure of the prime-counting function π in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (π‘𝐴) ∈ ℕ)
Theorem	chtrpcl 27085	Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ+)
Theorem	ppieq0 27086	The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ → ((π‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	ppiltx 27087	The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (π‘𝐴) < 𝐴)
Theorem	prmorcht 27088	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 27089	Lemma for mumul 27091. A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = 0)
Theorem	mumullem2 27090	Lemma for mumul 27091. The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0)
Theorem	mumul 27091	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 27092*	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 27093*	A "diagonal commutation" of divisor sums analogous to fsum0diag 15743. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})))
Theorem	fsumdvdsdiag 27094*	A "diagonal commutation" of divisor sums analogous to fsum0diag 15743. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐴)
Theorem	fsumdvdscom 27095*	A double commutation of divisor sums based on fsumdvdsdiag 27094. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
Theorem	dvdsppwf1o 27096*	A bijection between the divisors of a prime power and the integers less than or equal to the exponent. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝐹 = (𝑛 ∈ (0...𝐴) ↦ (𝑃↑𝑛))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → 𝐹:(0...𝐴)–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)})
Theorem	dvdsflf1o 27097*	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 27098*	A sum commutation from Σ𝑛 ≤ 𝐴, Σ𝑑 ∥ 𝑛, 𝐵(𝑛, 𝑑) to Σ𝑑 ≤ 𝐴, Σ𝑚 ≤ 𝐴 / 𝑑, 𝐵(𝑛, 𝑑𝑚). (Contributed by Mario Carneiro, 4-May-2016.)
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶)
Theorem	fsumfldivdiaglem 27099*	Lemma for fsumfldivdiag 27100. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚))))))
Theorem	fsumfldivdiag 27100*	The right-hand side of dvdsflsumcom 27098 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...(⌊‘(𝐴 / 𝑚)))𝐵)