P. 272 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27101-27200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fsumdvdsdiag 27101*	A "diagonal commutation" of divisor sums analogous to fsum0diag 15750. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐴)
Theorem	fsumdvdscom 27102*	A double commutation of divisor sums based on fsumdvdsdiag 27101. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
Theorem	dvdsppwf1o 27103*	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 27104*	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 27105*	A sum commutation from Σ𝑛 ≤ 𝐴, Σ𝑑 ∥ 𝑛, 𝐵(𝑛, 𝑑) to Σ𝑑 ≤ 𝐴, Σ𝑚 ≤ 𝐴 / 𝑑, 𝐵(𝑛, 𝑑𝑚). (Contributed by Mario Carneiro, 4-May-2016.)
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶)
Theorem	fsumfldivdiaglem 27106*	Lemma for fsumfldivdiag 27107. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚))))))
Theorem	fsumfldivdiag 27107*	The right-hand side of dvdsflsumcom 27105 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 27108*	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 27110. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0))
Theorem	musumsum 27109*	Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ (𝑚 = 1 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 1 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚} ((μ‘𝑘) · 𝐵) = 𝐶)
Theorem	muinv 27110*	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	mpodvdsmulf1o 27111*	If 𝑀 and 𝑁 are two coprime integers, multiplication forms a bijection from the set of pairs ⟨𝑗, 𝑘⟩ where 𝑗 ∥ 𝑀 and 𝑘 ∥ 𝑁, to the set of divisors of 𝑀 · 𝑁. Version of dvdsmulf1o 27113 using maps-to notation, which does not require ax-mulf 11155. (Contributed by GG, 18-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}    &   ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}    &   ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}    ⇒   ⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)
Theorem	fsumdvdsmul 27112*	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.) Avoid ax-mulf 11155. (Revised by GG, 18-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}    &   ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}    &   ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌)) → (𝐴 · 𝐵) = 𝐷)    &   ⊢ (𝑖 = (𝑗 · 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Σ𝑗 ∈ 𝑋 𝐴 · Σ𝑘 ∈ 𝑌 𝐵) = Σ𝑖 ∈ 𝑍 𝐶)
Theorem	dvdsmulf1o 27113*	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	fsumdvdsmulOLD 27114*	Obsolete version of fsumdvdsmul 27112 as of 18-Apr-2025. (Contributed by Mario Carneiro, 2-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}    &   ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}    &   ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌)) → (𝐴 · 𝐵) = 𝐷)    &   ⊢ (𝑖 = (𝑗 · 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Σ𝑗 ∈ 𝑋 𝐴 · Σ𝑘 ∈ 𝑌 𝐵) = Σ𝑖 ∈ 𝑍 𝐶)
Theorem	sgmppw 27115*	The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝐴 σ (𝑃↑𝑁)) = Σ𝑘 ∈ (0...𝑁)((𝑃↑𝑐𝐴)↑𝑘))
Theorem	0sgmppw 27116	A prime power 𝑃↑𝐾 has 𝐾 + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0) → (0 σ (𝑃↑𝐾)) = (𝐾 + 1))
Theorem	1sgmprm 27117	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 27118	The sum of the divisors of 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 17-May-2016.)
⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1))
Theorem	sgmmul 27119	The divisor function for fixed parameter 𝐴 is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) → (𝐴 σ (𝑀 · 𝑁)) = ((𝐴 σ 𝑀) · (𝐴 σ 𝑁)))
Theorem	ppiublem1 27120	Lemma for ppiub 27122. (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 27121	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 27122	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 27123	The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ≤ (log‘𝐴))
Theorem	chtlepsi 27124	The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ≤ (ψ‘𝐴))
Theorem	chprpcl 27125	Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ+)
Theorem	chpeq0 27126	The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → ((ψ‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	chteq0 27127	The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → ((θ‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	chtleppi 27128	Upper bound on the θ function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (θ‘𝐴) ≤ ((π‘𝐴) · (log‘𝐴)))
Theorem	chtublem 27129	Lemma for chtub 27130. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))
Theorem	chtub 27130	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 27131*	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 27132*	Apply fsumvma 27131 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 27133*	The logarithmic analogue of pcprod 16873. 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 27134*	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 27135*	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 27136*	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 27137*	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 27138	An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴))))
Theorem	logfacubnd 27139	A simple upper bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) ≤ (𝐴 · (log‘𝐴)))
Theorem	logfaclbnd 27140	A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 · ((log‘𝐴) − 2)) ≤ (log‘(!‘(⌊‘𝐴))))
Theorem	logfacbnd3 27141	Show the stronger statement log(𝑥!) = 𝑥log𝑥 − 𝑥 + 𝑂(log𝑥) alluded to in logfacrlim 27142. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))
Theorem	logfacrlim 27142	Combine the estimates logfacubnd 27139 and logfaclbnd 27140, to get log(𝑥!) = 𝑥log𝑥 + 𝑂(𝑥). Equation 9.2.9 of [Shapiro], p. 329. This is a weak form of the even stronger statement, log(𝑥!) = 𝑥log𝑥 − 𝑥 + 𝑂(log𝑥). (Contributed by Mario Carneiro, 16-Apr-2016.) (Revised by Mario Carneiro, 21-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝𝑟 1
Theorem	logexprlim 27143*	The sum Σ𝑛 ≤ 𝑥, log↑𝑁(𝑥 / 𝑛) has the asymptotic expansion (𝑁!)𝑥 + 𝑜(𝑥). (More precisely, the omitted term has order 𝑂(log↑𝑁(𝑥) / 𝑥).) (Contributed by Mario Carneiro, 22-May-2016.)
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁))
Theorem	logfacrlim2 27144*	Write out logfacrlim 27142 as a sum of logs. (Contributed by Mario Carneiro, 18-May-2016.) (Revised by Mario Carneiro, 22-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1
14.4.5  Perfect Number Theorem
Theorem	mersenne 27145	A Mersenne prime is a prime number of the form 2↑𝑃 − 1. This theorem shows that the 𝑃 in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 𝑃 ∈ ℙ)
Theorem	perfect1 27146	Euclid's contribution to the Euclid-Euler theorem. A number of the form 2↑(𝑝 − 1) · (2↑𝑝 − 1) is a perfect number. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → (1 σ ((2↑(𝑃 − 1)) · ((2↑𝑃) − 1))) = ((2↑𝑃) · ((2↑𝑃) − 1)))
Theorem	perfectlem1 27147	Lemma for perfect 27149. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)    &   ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))    ⇒   ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
Theorem	perfectlem2 27148	Lemma for perfect 27149. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by Wolf Lammen, 17-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)    &   ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
Theorem	perfect 27149*	The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer 𝑁 is a perfect number (that is, its divisor sum is 2𝑁) if and only if it is of the form 2↑(𝑝 − 1) · (2↑𝑝 − 1), where 2↑𝑝 − 1 is prime (a Mersenne prime), and therefore 𝑝 is also prime, see mersenne 27145. This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → ((1 σ 𝑁) = (2 · 𝑁) ↔ ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)))))
14.4.6  Characters of Z/nZ
Syntax	cdchr 27150	Extend class notation with the group of Dirichlet characters.
class DChr
Definition	df-dchr 27151*	The group of Dirichlet characters mod 𝑛 is the set of monoid homomorphisms from ℤ / 𝑛ℤ to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ DChr = (𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑛) / 𝑧⦌⦋{𝑥 ∈ ((mulGrp‘𝑧) MndHom (mulGrp‘ℂfld)) ∣ (((Base‘𝑧) ∖ (Unit‘𝑧)) × {0}) ⊆ 𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝑏 × 𝑏))⟩})
Theorem	dchrval 27152*	Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥})    ⇒   ⊢ (𝜑 → 𝐺 = {⟨(Base‘ndx), 𝐷⟩, ⟨(+g‘ndx), ( ∘f · ↾ (𝐷 × 𝐷))⟩})
Theorem	dchrbas 27153*	Base set of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∣ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑥})
Theorem	dchrelbas 27154	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ((𝐵 ∖ 𝑈) × {0}) ⊆ 𝑋)))
Theorem	dchrelbas2 27155*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))))
Theorem	dchrelbas3 27156*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋:𝐵⟶ℂ ∧ (∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))))
Theorem	dchrelbasd 27157*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ (𝑘 = 𝑥 → 𝑋 = 𝐴)    &   ⊢ (𝑘 = 𝑦 → 𝑋 = 𝐶)    &   ⊢ (𝑘 = (𝑥(.r‘𝑍)𝑦) → 𝑋 = 𝐸)    &   ⊢ (𝑘 = (1r‘𝑍) → 𝑋 = 𝑌)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐸 = (𝐴 · 𝐶))    &   ⊢ (𝜑 → 𝑌 = 1)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 𝑋, 0)) ∈ 𝐷)
Theorem	dchrrcl 27158	Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ)
Theorem	dchrmhm 27159	A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld))
Theorem	dchrf 27160	A Dirichlet character is a function. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝑋:𝐵⟶ℂ)
Theorem	dchrelbas4 27161*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of ℂ, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    ⇒   ⊢ (𝑋 ∈ 𝐷 ↔ (𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0)))
Theorem	dchrzrh1 27162	Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘1)) = 1)
Theorem	dchrzrhcl 27163	A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘𝐴)) ∈ ℂ)
Theorem	dchrzrhmul 27164	A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘(𝐴 · 𝐶))) = ((𝑋‘(𝐿‘𝐴)) · (𝑋‘(𝐿‘𝐶))))
Theorem	dchrplusg 27165	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → · = ( ∘f · ↾ (𝐷 × 𝐷)))
Theorem	dchrmul 27166	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘f · 𝑌))
Theorem	dchrmulcl 27167	Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷)
Theorem	dchrn0 27168	A Dirichlet character is nonzero on the units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋‘𝐴) ≠ 0 ↔ 𝐴 ∈ 𝑈))
Theorem	dchr1cl 27169*	Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ∈ 𝐷)
Theorem	dchrmullid 27170*	Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ( 1 · 𝑋) = 𝑋)
Theorem	dchrinvcl 27171*	Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝐾 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0))    ⇒   ⊢ (𝜑 → (𝐾 ∈ 𝐷 ∧ (𝐾 · 𝑋) = 1 ))
Theorem	dchrabl 27172	The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
Theorem	dchrfi 27173	The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
Theorem	dchrghm 27174	A Dirichlet character restricted to the unit group of ℤ/nℤ is a group homomorphism into the multiplicative group of nonzero complex numbers. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 GrpHom 𝑀))
Theorem	dchr1 27175	Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ( 1 ‘𝐴) = 1)
Theorem	dchreq 27176*	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 = 𝑌 ↔ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = (𝑌‘𝑘)))
Theorem	dchrresb 27177	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑋 ↾ 𝑈) = (𝑌 ↾ 𝑈) ↔ 𝑋 = 𝑌))
Theorem	dchrabs 27178	A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) = 1)
Theorem	dchrinv 27179	The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of 𝑋 are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = (∗ ∘ 𝑋))
Theorem	dchrabs2 27180	A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ≤ 1)
Theorem	dchr1re 27181	The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 :𝐵⟶ℝ)
Theorem	dchrptlem1 27182*	Lemma for dchrpt 27185. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ · = (.g‘𝐻)    &   ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)    &   ⊢ (𝜑 → 𝐻dom DProd 𝑆)    &   ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)    &   ⊢ 𝑃 = (𝐻dProj𝑆)    &   ⊢ 𝑂 = (od‘𝐻)    &   ⊢ 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))    &   ⊢ (𝜑 → 𝐼 ∈ dom 𝑊)    &   ⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 )    &   ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))    ⇒   ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (𝑇↑𝑀))
Theorem	dchrptlem2 27183*	Lemma for dchrpt 27185. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ · = (.g‘𝐻)    &   ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)    &   ⊢ (𝜑 → 𝐻dom DProd 𝑆)    &   ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)    &   ⊢ 𝑃 = (𝐻dProj𝑆)    &   ⊢ 𝑂 = (od‘𝐻)    &   ⊢ 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))    &   ⊢ (𝜑 → 𝐼 ∈ dom 𝑊)    &   ⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 )    &   ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
Theorem	dchrptlem3 27184*	Lemma for dchrpt 27185. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ · = (.g‘𝐻)    &   ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)    &   ⊢ (𝜑 → 𝐻dom DProd 𝑆)    &   ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
Theorem	dchrpt 27185*	For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
Theorem	dchrsum2 27186*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character 𝑋 is 0 if 𝑋 is non-principal and ϕ(𝑛) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝑈 = (Unit‘𝑍)    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0))
Theorem	dchrsum 27187*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character 𝑋 is 0 if 𝑋 is non-principal and ϕ(𝑛) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝐵 = (Base‘𝑍)    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ 𝐵 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0))
Theorem	sumdchr2 27188*	Lemma for sumdchr 27190. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))
Theorem	dchrhash 27189	There are exactly ϕ(𝑁) Dirichlet characters modulo 𝑁. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝐷) = (ϕ‘𝑁))
Theorem	sumdchr 27190*	An orthogonality relation for Dirichlet characters: the sum of 𝑥(𝐴) for fixed 𝐴 and all 𝑥 is 0 if 𝐴 = 1 and ϕ(𝑛) otherwise. Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (ϕ‘𝑁), 0))
Theorem	dchr2sum 27191*	An orthogonality relation for Dirichlet characters: the sum of 𝑋(𝑎) · ∗𝑌(𝑎) over all 𝑎 is nonzero only when 𝑋 = 𝑌. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ 𝐵 ((𝑋‘𝑎) · (∗‘(𝑌‘𝑎))) = if(𝑋 = 𝑌, (ϕ‘𝑁), 0))
Theorem	sum2dchr 27192*	An orthogonality relation for Dirichlet characters: the sum of 𝑥(𝐴) for fixed 𝐴 and all 𝑥 is 0 if 𝐴 = 1 and ϕ(𝑛) otherwise. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 ((𝑥‘𝐴) · (∗‘(𝑥‘𝐶))) = if(𝐴 = 𝐶, (ϕ‘𝑁), 0))
14.4.7  Bertrand's postulate
Theorem	bcctr 27193	Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))
Theorem	pcbcctr 27194*	Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
Theorem	bcmono 27195	The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
Theorem	bcmax 27196	The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁))
Theorem	bcp1ctr 27197	Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)
⊢ (𝑁 ∈ ℕ0 → ((2 · (𝑁 + 1))C(𝑁 + 1)) = (((2 · 𝑁)C𝑁) · (2 · (((2 · 𝑁) + 1) / (𝑁 + 1)))))
Theorem	bclbnd 27198	A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Theorem	efexple 27199	Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴)))))
Theorem	bpos1lem 27200*	Lemma for bpos1 27201. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑)    &   ⊢ (𝑁 ∈ (ℤ≥‘𝑃) → 𝜑)    &   ⊢ 𝑃 ∈ ℙ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 · 2) = 𝐵    &   ⊢ 𝐴 < 𝑃    &   ⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝐴) → 𝜑)