P. 275 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27401-27500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	1sgm2ppw 27401	The sum of the divisors of 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 17-May-2016.)
⊢ (𝑁 ∈ ℕ → (1 σ (2↑(𝑁 − 1))) = ((2↑𝑁) − 1))
Theorem	sgmmul 27402	The divisor function for fixed parameter 𝐴 is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) → (𝐴 σ (𝑀 · 𝑁)) = ((𝐴 σ 𝑀) · (𝐴 σ 𝑁)))
Theorem	ppiublem1 27403	Lemma for ppiub 27405. (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 27404	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 27405	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 27406	The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ≤ (log‘𝐴))
Theorem	chtlepsi 27407	The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ≤ (ψ‘𝐴))
Theorem	chprpcl 27408	Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ+)
Theorem	chpeq0 27409	The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → ((ψ‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	chteq0 27410	The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝐴 ∈ ℝ → ((θ‘𝐴) = 0 ↔ 𝐴 < 2))
Theorem	chtleppi 27411	Upper bound on the θ function. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (θ‘𝐴) ≤ ((π‘𝐴) · (log‘𝐴)))
Theorem	chtublem 27412	Lemma for chtub 27413. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))
Theorem	chtub 27413	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 27414*	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 27415*	Apply fsumvma 27414 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 27416*	The logarithmic analogue of pcprod 16980. 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 27417*	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 27418*	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 27419*	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 27420*	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 27421	An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴))))
Theorem	logfacubnd 27422	A simple upper bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) ≤ (𝐴 · (log‘𝐴)))
Theorem	logfaclbnd 27423	A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 · ((log‘𝐴) − 2)) ≤ (log‘(!‘(⌊‘𝐴))))
Theorem	logfacbnd3 27424	Show the stronger statement log(𝑥!) = 𝑥log𝑥 − 𝑥 + 𝑂(log𝑥) alluded to in logfacrlim 27425. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))
Theorem	logfacrlim 27425	Combine the estimates logfacubnd 27422 and logfaclbnd 27423, 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 27426*	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 27427*	Write out logfacrlim 27425 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 27428	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 27429	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 27430	Lemma for perfect 27432. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)    &   ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))    ⇒   ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
Theorem	perfectlem2 27431	Lemma for perfect 27432. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by Wolf Lammen, 17-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)    &   ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
Theorem	perfect 27432*	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 27428. 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 27433	Extend class notation with the group of Dirichlet characters.
class DChr
Definition	df-dchr 27434*	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 27435*	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 27436*	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 27437	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 27438*	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 27439*	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 27440*	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 27441	Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ)
Theorem	dchrmhm 27442	A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld))
Theorem	dchrf 27443	A Dirichlet character is a function. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝑋:𝐵⟶ℂ)
Theorem	dchrelbas4 27444*	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 27445	Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘1)) = 1)
Theorem	dchrzrhcl 27446	A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘𝐴)) ∈ ℂ)
Theorem	dchrzrhmul 27447	A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘(𝐴 · 𝐶))) = ((𝑋‘(𝐿‘𝐴)) · (𝑋‘(𝐿‘𝐶))))
Theorem	dchrplusg 27448	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → · = ( ∘f · ↾ (𝐷 × 𝐷)))
Theorem	dchrmul 27449	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘f · 𝑌))
Theorem	dchrmulcl 27450	Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷)
Theorem	dchrn0 27451	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 27452*	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 27453*	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 27454*	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 27455	The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
Theorem	dchrfi 27456	The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
Theorem	dchrghm 27457	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 27458	Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ( 1 ‘𝐴) = 1)
Theorem	dchreq 27459*	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 27460	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 27461	A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) = 1)
Theorem	dchrinv 27462	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 27463	A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ≤ 1)
Theorem	dchr1re 27464	The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 :𝐵⟶ℝ)
Theorem	dchrptlem1 27465*	Lemma for dchrpt 27468. (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 27466*	Lemma for dchrpt 27468. (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 27467*	Lemma for dchrpt 27468. (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 27468*	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 27469*	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 27470*	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 27471*	Lemma for sumdchr 27473. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))
Theorem	dchrhash 27472	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 27473*	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 27474*	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 27475*	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 27476	Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))
Theorem	pcbcctr 27477*	Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
Theorem	bcmono 27478	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 27479	The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁))
Theorem	bcp1ctr 27480	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 27481	A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Theorem	efexple 27482	Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴)))))
Theorem	bpos1lem 27483*	Lemma for bpos1 27484. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑)    &   ⊢ (𝑁 ∈ (ℤ≥‘𝑃) → 𝜑)    &   ⊢ 𝑃 ∈ ℙ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 · 2) = 𝐵    &   ⊢ 𝐴 < 𝑃    &   ⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝐴) → 𝜑)
Theorem	bpos1 27484*	Bertrand's postulate, checked numerically for 𝑁 ≤ 64, using the prime sequence 2, 3, 5, 7, 13, 23, 43, 83. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≤ ;64) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
Theorem	bposlem1 27485	An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
Theorem	bposlem2 27486	There are no odd primes in the range (2𝑁 / 3, 𝑁] dividing the 𝑁-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 2 < 𝑃)    &   ⊢ (𝜑 → ((2 · 𝑁) / 3) < 𝑃)    &   ⊢ (𝜑 → 𝑃 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = 0)
Theorem	bposlem3 27487*	Lemma for bpos 27494. Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 27486 and prmfac1 16804, respectively, and it does not have any in the range (𝑁, 2𝑁] by hypothesis, the product of the primes up through 2𝑁 / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
Theorem	bposlem4 27488*	Lemma for bpos 27494. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (3...𝐾))
Theorem	bposlem5 27489*	Lemma for bpos 27494. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
Theorem	bposlem6 27490*	Lemma for bpos 27494. By using the various bounds at our disposal, arrive at an inequality that is false for 𝑁 large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
Theorem	bposlem7 27491*	Lemma for bpos 27494. The function 𝐹 is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → (e↑2) ≤ 𝐴)    &   ⊢ (𝜑 → (e↑2) ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 → (𝐹‘𝐵) < (𝐹‘𝐴)))
Theorem	bposlem8 27492	Lemma for bpos 27494. Evaluate 𝐹(64) and show it is less than log2. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    ⇒   ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
Theorem	bposlem9 27493*	Lemma for bpos 27494. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ;64 < 𝑁)    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bpos 27494*	Bertrand's postulate: there is a prime between 𝑁 and 2𝑁 for every positive integer 𝑁. This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
14.4.8  Quadratic residues and the Legendre symbol If the congruence ((𝑥↑2) mod 𝑝) = (𝑛 mod 𝑝) has a solution we say that 𝑛 is a quadratic residue mod 𝑝. If the congruence has no solution we say that 𝑛 is a quadratic nonresidue mod 𝑝, see definition in [ApostolNT] p. 178. The Legendre symbol (𝑛 /L 𝑝) is defined in a way that its value is 1 if 𝑛 is a quadratic residue mod 𝑝 and -1 if 𝑛 is a quadratic nonresidue mod 𝑝 (and 0 if 𝑝 divides 𝑛), see lgsqr 27552. Originally, the Legendre symbol (𝑁 /L 𝑃) was defined for odd primes 𝑃 only (and arbitrary integers 𝑁) by Adrien-Marie Legendre in 1798, see definition in [ApostolNT] p. 179. It was generalized to be defined for any positive odd integer by Carl Gustav Jacob Jacobi in 1837 (therefore called "Jacobi symbol" since then), see definition in [ApostolNT] p. 188. Finally, it was generalized to be defined for any integer by Leopold Kronecker in 1885 (therefore called "Kronecker symbol" since then). The definition df-lgs 27496 for the "Legendre symbol" /L is actually the definition of the "Kronecker symbol". Since only one definition (and one class symbol) are provided in set.mm, the names "Legendre symbol", "Jacobi symbol" and "Kronecker symbol" are used synonymously for /L, but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol".
Syntax	clgs 27495	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 27496*	Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in [ApostolNT] p. 179 resp. definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ /L = (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)))))
Theorem	zabsle1 27497	{-1, 0, 1} is the set of all integers with absolute value at most 1. (Contributed by AV, 13-Jul-2021.)
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ {-1, 0, 1} ↔ (abs‘𝑍) ≤ 1))
Theorem	lgslem1 27498	When 𝑎 is coprime to the prime 𝑝, 𝑎↑((𝑝 − 1) / 2) is equivalent mod 𝑝 to 1 or -1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2})
Theorem	lgslem2 27499	The set 𝑍 of all integers with absolute value at most 1 contains {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ (-1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍)
Theorem	lgslem3 27500*	The set 𝑍 of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑍) → (𝐴 · 𝐵) ∈ 𝑍)