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
Theorem	lgamgulmlem3 27001*	Lemma for lgamgulm 27005. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁)    ⇒   ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))))
Theorem	lgamgulmlem4 27002*	Lemma for lgamgulm 27005. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    &   ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))    ⇒   ⊢ (𝜑 → seq1( + , 𝑇) ∈ dom ⇝ )
Theorem	lgamgulmlem5 27003*	Lemma for lgamgulm 27005. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    &   ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))    ⇒   ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) ≤ (𝑇‘𝑛))
Theorem	lgamgulmlem6 27004*	The series 𝐺 is uniformly convergent on the compact region 𝑈, which describes a circle of radius 𝑅 with holes of size 1 / 𝑅 around the poles of the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    &   ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))    ⇒   ⊢ (𝜑 → (seq1( ∘f + , 𝐺) ∈ dom (⇝𝑢‘𝑈) ∧ (seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ 𝑂) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘𝑂) ≤ 𝑟)))
Theorem	lgamgulm 27005*	The series 𝐺 is uniformly convergent on the compact region 𝑈, which describes a circle of radius 𝑅 with holes of size 1 / 𝑅 around the poles of the gamma function. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    ⇒   ⊢ (𝜑 → seq1( ∘f + , 𝐺) ∈ dom (⇝𝑢‘𝑈))
Theorem	lgamgulm2 27006*	Rewrite the limit of the sequence 𝐺 in terms of the log-Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    ⇒   ⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))))
Theorem	lgambdd 27007*	The log-Gamma function is bounded on the region 𝑈. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟)
Theorem	lgamucov 27008*	The 𝑈 regions used in the proof of lgamgulm 27005 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))
Theorem	lgamucov2 27009*	The 𝑈 regions used in the proof of lgamgulm 27005 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈)
Theorem	lgamcvglem 27010*	Lemma for lgamf 27012 and lgamcvg 27024. (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    ⇒   ⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))))
Theorem	lgamcl 27011	The log-Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘𝐴) ∈ ℂ)
Theorem	lgamf 27012	The log-Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ log Γ:(ℂ ∖ (ℤ ∖ ℕ))⟶ℂ
Theorem	gamf 27013	The Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ Γ:(ℂ ∖ (ℤ ∖ ℕ))⟶ℂ
Theorem	gamcl 27014	The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℂ)
Theorem	eflgam 27015	The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴))
Theorem	gamne0 27016	The Gamma function is never zero. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ≠ 0)
Theorem	igamval 27017	Value of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) = if(𝐴 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝐴))))
Theorem	igamz 27018	Value of the inverse Gamma function on nonpositive integers. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℤ ∖ ℕ) → (1/Γ‘𝐴) = 0)
Theorem	igamgam 27019	Value of the inverse Gamma function in terms of the Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (1 / (Γ‘𝐴)))
Theorem	igamlgam 27020	Value of the inverse Gamma function in terms of the log-Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (exp‘-(log Γ‘𝐴)))
Theorem	igamf 27021	Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ 1/Γ:ℂ⟶ℂ
Theorem	igamcl 27022	Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) ∈ ℂ)
Theorem	gamigam 27023	The Gamma function is the inverse of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) = (1 / (1/Γ‘𝐴)))
Theorem	lgamcvg 27024*	The series 𝐺 converges to log Γ(𝐴) + log(𝐴). (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴)))
Theorem	lgamcvg2 27025*	The series 𝐺 converges to log Γ(𝐴 + 1). (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))
Theorem	gamcvg 27026*	The pointwise exponential of the series 𝐺 converges to Γ(𝐴) · 𝐴. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴))
Theorem	lgamp1 27027	The functional equation of the (log) Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) = ((log Γ‘𝐴) + (log‘𝐴)))
Theorem	gamp1 27028	The functional equation of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘(𝐴 + 1)) = ((Γ‘𝐴) · 𝐴))
Theorem	gamcvg2lem 27029*	Lemma for gamcvg2 27030. (Contributed by Mario Carneiro, 10-Jul-2017.)
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1)))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    ⇒   ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) = seq1( · , 𝐹))
Theorem	gamcvg2 27030*	An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1)))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → seq1( · , 𝐹) ⇝ ((Γ‘𝐴) · 𝐴))
Theorem	regamcl 27031	The Gamma function is real for real input. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℝ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℝ)
Theorem	relgamcl 27032	The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → (log Γ‘𝐴) ∈ ℝ)
Theorem	rpgamcl 27033	The log-Gamma function is positive real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → (Γ‘𝐴) ∈ ℝ+)
Theorem	lgam1 27034	The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (log Γ‘1) = 0
Theorem	gam1 27035	The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (Γ‘1) = 1
Theorem	facgam 27036	The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) = (Γ‘(𝑁 + 1)))
Theorem	gamfac 27037	The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝑁 ∈ ℕ → (Γ‘𝑁) = (!‘(𝑁 − 1)))
14.4  Basic number theory
14.4.1  Wilson's theorem
Theorem	wilthlem1 27038	The only elements that are equal to their own inverses in the multiplicative group of nonzero elements in ℤ / 𝑃ℤ are 1 and -1≡𝑃 − 1. (Note that from prmdiveq 16717, (𝑁↑(𝑃 − 2)) mod 𝑃 is the modular inverse of 𝑁 in ℤ / 𝑃ℤ. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1))))
Theorem	wilthlem2 27039*	Lemma for wilth 27041: induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from 1 to 𝑃 − 1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except 1 and 𝑃 − 1, and so each pair multiplies to 1, and 1 and 𝑃 − 1≡-1 multiply to -1, so the full product is equal to -1. Here we make this precise by doing the product pair by pair. The induction hypothesis says that every subset 𝑆 of 1...(𝑃 − 1) that is closed under inverse (i.e. all pairs are matched up) and contains 𝑃 − 1 multiplies to -1 mod 𝑃. Given such a set, we take out one element 𝑧 ≠ 𝑃 − 1. If there are no such elements, then 𝑆 = {𝑃 − 1} which forms the base case. Otherwise, 𝑆 ∖ {𝑧, 𝑧↑-1} is also closed under inverse and contains 𝑃 − 1, so the induction hypothesis says that this equals -1; and the remaining two elements are either equal to each other, in which case wilthlem1 27038 gives that 𝑧 = 1 or 𝑃 − 1, and we've already excluded the second case, so the product gives 1; or 𝑧 ≠ 𝑧↑-1 and their product is 1. In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ 𝑇 = (mulGrp‘ℂfld)    &   ⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))    ⇒   ⊢ (𝜑 → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
Theorem	wilthlem3 27040*	Lemma for wilth 27041. Here we round out the argument of wilthlem2 27039 with the final step of the induction. The induction argument shows that every subset of 1...(𝑃 − 1) that is closed under inverse and contains 𝑃 − 1 multiplies to -1 mod 𝑃, and clearly 1...(𝑃 − 1) itself is such a set. Thus, the product of all the elements is -1, and all that is left is to translate the group sum notation (which we used for its unordered summing capabilities) into an ordered sequence to match the definition of the factorial. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ 𝑇 = (mulGrp‘ℂfld)    &   ⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}    ⇒   ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))
Theorem	wilth 27041	Wilson's theorem. A number is prime iff it is greater than or equal to 2 and (𝑁 − 1)! is congruent to -1, mod 𝑁, or alternatively if 𝑁 divides (𝑁 − 1)! + 1. In this part of the proof we show the relatively simple reverse implication; see wilthlem3 27040 for the forward implication. This is Metamath 100 proof #51. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)))
Theorem	wilthimp 27042	The forward implication of Wilson's theorem wilth 27041 (see wilthlem3 27040), expressed using the modulo operation: For any prime 𝑝 we have (𝑝 − 1)!≡ − 1 (mod 𝑝), see theorem 5.24 in [ApostolNT] p. 116. (Contributed by AV, 21-Jul-2021.)
⊢ (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) mod 𝑃) = (-1 mod 𝑃))
14.4.2  The Fundamental Theorem of Algebra
Theorem	ftalem1 27043*	Lemma for fta 27050: "growth lemma". There exists some 𝑟 such that 𝐹 is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝑇 = (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))
Theorem	ftalem2 27044*	Lemma for fta 27050. There exists some 𝑟 such that 𝐹 has magnitude greater than 𝐹(0) outside the closed ball B(0,r). (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑈 = if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1))    &   ⊢ 𝑇 = ((abs‘(𝐹‘0)) / ((abs‘(𝐴‘𝑁)) / 2))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))
Theorem	ftalem3 27045*	Lemma for fta 27050. There exists a global minimum of the function abs ∘ 𝐹. The proof uses a circle of radius 𝑟 where 𝑟 is the value coming from ftalem1 27043; since this is a compact set, the minimum on this disk is achieved, and this must then be the global minimum. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐷 = {𝑦 ∈ ℂ ∣ (abs‘𝑦) ≤ 𝑅}    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℂ (𝑅 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥))))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ ℂ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑥)))
Theorem	ftalem4 27046*	Lemma for fta 27050: Closure of the auxiliary variables for ftalem5 27047. (Contributed by Mario Carneiro, 20-Sep-2014.) (Revised by AV, 28-Sep-2020.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐹‘0) ≠ 0)    &   ⊢ 𝐾 = inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < )    &   ⊢ 𝑇 = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))    &   ⊢ 𝑈 = ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))    &   ⊢ 𝑋 = if(1 ≤ 𝑈, 1, 𝑈)    ⇒   ⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+)))
Theorem	ftalem5 27047*	Lemma for fta 27050: Main proof. We have already shifted the minimum found in ftalem3 27045 to zero by a change of variables, and now we show that the minimum value is zero. Expanding in a series about the minimum value, let 𝐾 be the lowest term in the polynomial that is nonzero, and let 𝑇 be a 𝐾-th root of -𝐹(0) / 𝐴(𝐾). Then an evaluation of 𝐹(𝑇𝑋) where 𝑋 is a sufficiently small positive number yields 𝐹(0) for the first term and -𝐹(0) · 𝑋↑𝐾 for the 𝐾-th term, and all higher terms are bounded because 𝑋 is small. Thus, abs(𝐹(𝑇𝑋)) ≤ abs(𝐹(0))(1 − 𝑋↑𝐾) < abs(𝐹(0)), in contradiction to our choice of 𝐹(0) as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014.) (Revised by AV, 28-Sep-2020.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐹‘0) ≠ 0)    &   ⊢ 𝐾 = inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < )    &   ⊢ 𝑇 = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))    &   ⊢ 𝑈 = ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))    &   ⊢ 𝑋 = if(1 ≤ 𝑈, 1, 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))
Theorem	ftalem6 27048*	Lemma for fta 27050: Discharge the auxiliary variables in ftalem5 27047. (Contributed by Mario Carneiro, 20-Sep-2014.) (Proof shortened by AV, 28-Sep-2020.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐹‘0) ≠ 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))
Theorem	ftalem7 27049*	Lemma for fta 27050. Shift the minimum away from zero by a change of variables. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → (𝐹‘𝑋) ≠ 0)    ⇒   ⊢ (𝜑 → ¬ ∀𝑥 ∈ ℂ (abs‘(𝐹‘𝑋)) ≤ (abs‘(𝐹‘𝑥)))
Theorem	fta 27050*	The Fundamental Theorem of Algebra. Any polynomial with positive degree (i.e. non-constant) has a root. This is Metamath 100 proof #2. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) ∈ ℕ) → ∃𝑧 ∈ ℂ (𝐹‘𝑧) = 0)
14.4.3  The Basel problem (ζ(2) = π2/6)
Theorem	basellem1 27051	Lemma for basel 27060. Closure of the sequence of roots. (Contributed by Mario Carneiro, 30-Jul-2014.) Replace OLD theorem. (Revised by Wolf Lammen, 18-Sep-2020.)
⊢ 𝑁 = ((2 · 𝑀) + 1)    ⇒   ⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / 𝑁) ∈ (0(,)(π / 2)))
Theorem	basellem2 27052*	Lemma for basel 27060. Show that 𝑃 is a polynomial of degree 𝑀, and compute its coefficient function. (Contributed by Mario Carneiro, 30-Jul-2014.)
⊢ 𝑁 = ((2 · 𝑀) + 1)    &   ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))    ⇒   ⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (Poly‘ℂ) ∧ (deg‘𝑃) = 𝑀 ∧ (coeff‘𝑃) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))))
Theorem	basellem3 27053*	Lemma for basel 27060. Using the binomial theorem and de Moivre's formula, we have the identity e↑i𝑁𝑥 / (sin𝑥)↑𝑛 = Σ𝑚 ∈ (0...𝑁)(𝑁C𝑚)(i↑𝑚)(cot𝑥)↑(𝑁 − 𝑚), so taking imaginary parts yields sin(𝑁𝑥) / (sin𝑥)↑𝑁 = Σ𝑗 ∈ (0...𝑀)(𝑁C2𝑗)(-1)↑(𝑀 − 𝑗) (cot𝑥)↑(-2𝑗) = 𝑃((cot𝑥)↑2), where 𝑁 = 2𝑀 + 1. (Contributed by Mario Carneiro, 30-Jul-2014.)
⊢ 𝑁 = ((2 · 𝑀) + 1)    &   ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))    ⇒   ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
Theorem	basellem4 27054*	Lemma for basel 27060. By basellem3 27053, the expression 𝑃((cot𝑥)↑2) = sin(𝑁𝑥) / (sin𝑥)↑𝑁 goes to zero whenever 𝑥 = 𝑛π / 𝑁 for some 𝑛 ∈ (1...𝑀), so this function enumerates 𝑀 distinct roots of a degree- 𝑀 polynomial, which must therefore be all the roots by fta1 26276. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ 𝑁 = ((2 · 𝑀) + 1)    &   ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))    ⇒   ⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0}))
Theorem	basellem5 27055*	Lemma for basel 27060. Using vieta1 26280, we can calculate the sum of the roots of 𝑃 as the quotient of the top two coefficients, and since the function 𝑇 enumerates the roots, we are left with an equation that sums the cot↑2 function at the 𝑀 different roots. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ 𝑁 = ((2 · 𝑀) + 1)    &   ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))    ⇒   ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
Theorem	basellem6 27056	Lemma for basel 27060. The function 𝐺 goes to zero because it is bounded by 1 / 𝑛. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))    ⇒   ⊢ 𝐺 ⇝ 0
Theorem	basellem7 27057	Lemma for basel 27060. The function 1 + 𝐴 · 𝐺 for any fixed 𝐴 goes to 1. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))    &   ⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((ℕ × {1}) ∘f + ((ℕ × {𝐴}) ∘f · 𝐺)) ⇝ 1
Theorem	basellem8 27058*	Lemma for basel 27060. The function 𝐹 of partial sums of the inverse squares is bounded below by 𝐽 and above by 𝐾, obtained by summing the inequality cot↑2𝑥 ≤ 1 / 𝑥↑2 ≤ csc↑2𝑥 = cot↑2𝑥 + 1 over the 𝑀 roots of the polynomial 𝑃, and applying the identity basellem5 27055. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))    &   ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))    &   ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘f · ((ℕ × {1}) ∘f − 𝐺))    &   ⊢ 𝐽 = (𝐻 ∘f · ((ℕ × {1}) ∘f + ((ℕ × {-2}) ∘f · 𝐺)))    &   ⊢ 𝐾 = (𝐻 ∘f · ((ℕ × {1}) ∘f + 𝐺))    &   ⊢ 𝑁 = ((2 · 𝑀) + 1)    ⇒   ⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))
Theorem	basellem9 27059*	Lemma for basel 27060. Since by basellem8 27058 𝐹 is bounded by two expressions that tend to π↑2 / 6, 𝐹 must also go to π↑2 / 6 by the squeeze theorem climsqz 15568. But the series 𝐹 is exactly the partial sums of 𝑘↑-2, so it follows that this is also the value of the infinite sum Σ𝑘 ∈ ℕ(𝑘↑-2). (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))    &   ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))    &   ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘f · ((ℕ × {1}) ∘f − 𝐺))    &   ⊢ 𝐽 = (𝐻 ∘f · ((ℕ × {1}) ∘f + ((ℕ × {-2}) ∘f · 𝐺)))    &   ⊢ 𝐾 = (𝐻 ∘f · ((ℕ × {1}) ∘f + 𝐺))    ⇒   ⊢ Σ𝑘 ∈ ℕ (𝑘↑-2) = ((π↑2) / 6)
Theorem	basel 27060	The sum of the inverse squares is π↑2 / 6. This is commonly known as the Basel problem, with the first known proof attributed to Euler. See http://en.wikipedia.org/wiki/Basel_problem. This particular proof approach is due to Cauchy (1821). This is Metamath 100 proof #14. (Contributed by Mario Carneiro, 30-Jul-2014.)
⊢ Σ𝑘 ∈ ℕ (𝑘↑-2) = ((π↑2) / 6)
14.4.4  Number-theoretical functions
Syntax	ccht 27061	Extend class notation with the first Chebyshev function.
class θ
Syntax	cvma 27062	Extend class notation with the von Mangoldt function.
class Λ
Syntax	cchp 27063	Extend class notation with the second Chebyshev function.
class ψ
Syntax	cppi 27064	Extend class notation with the prime-counting function pi.
class π
Syntax	cmu 27065	Extend class notation with the Möbius function.
class μ
Syntax	csgm 27066	Extend class notation with the divisor function.
class σ
Definition	df-cht 27067*	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 27069. See https://en.wikipedia.org/wiki/Chebyshev_function 27069 for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝))
Definition	df-vma 27068*	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 27069*	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 27070	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 27071*	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 27072*	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 27073*	Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (exp‘𝐵) ∈ ℕ)    ⇒   ⊢ (𝜑 → (exp‘Σ𝑘 ∈ 𝐴 𝐵) ∈ ℕ)
Theorem	ppisval 27074	The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ))
Theorem	ppisval2 27075	The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈ (ℤ≥‘𝑀)) → ((0[,]𝐴) ∩ ℙ) = ((𝑀...(⌊‘𝐴)) ∩ ℙ))
Theorem	ppifi 27076	The set of primes less than 𝐴 is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
Theorem	prmdvdsfi 27077*	The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin)
Theorem	chtf 27078	Domain and codoamin of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ θ:ℝ⟶ℝ
Theorem	chtcl 27079	Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ)
Theorem	chtval 27080*	Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
Theorem	efchtcl 27081	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 27082	The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (θ‘𝐴))
Theorem	vmaval 27083*	Value of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ 𝑆 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}    ⇒   ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) = if((♯‘𝑆) = 1, (log‘∪ 𝑆), 0))
Theorem	isppw 27084*	Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝐴))
Theorem	isppw2 27085*	Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)))
Theorem	vmappw 27086	Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (Λ‘(𝑃↑𝐾)) = (log‘𝑃))
Theorem	vmaprm 27087	Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝑃 ∈ ℙ → (Λ‘𝑃) = (log‘𝑃))
Theorem	vmacl 27088	Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ)
Theorem	vmaf 27089	Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ Λ:ℕ⟶ℝ
Theorem	efvmacl 27090	The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → (exp‘(Λ‘𝐴)) ∈ ℕ)
Theorem	vmage0 27091	The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴))
Theorem	chpval 27092*	Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛))
Theorem	chpf 27093	Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ ψ:ℝ⟶ℝ
Theorem	chpcl 27094	Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ)
Theorem	efchpcl 27095	The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → (exp‘(ψ‘𝐴)) ∈ ℕ)
Theorem	chpge0 27096	The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (ψ‘𝐴))
Theorem	ppival 27097	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (π‘𝐴) = (♯‘((0[,]𝐴) ∩ ℙ)))
Theorem	ppival2 27098	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℤ → (π‘𝐴) = (♯‘((2...𝐴) ∩ ℙ)))
Theorem	ppival2g 27099	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 2 ∈ (ℤ≥‘𝑀)) → (π‘𝐴) = (♯‘((𝑀...𝐴) ∩ ℙ)))
Theorem	ppif 27100	Domain and codomain of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ π:ℝ⟶ℕ0