![]() |
Metamath
Proof Explorer Theorem List (p. 253 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmgmaddn0 25201 | If 𝐴 is not a nonpositive integer, then 𝐴 + 𝑁 is nonzero for any nonnegative integer 𝑁. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ 𝑁 ∈ ℕ0) → (𝐴 + 𝑁) ≠ 0) | ||
Theorem | dmlogdmgm 25202 | If 𝐴 is in the continuous domain of the logarithm, then it is in the domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (-∞(,]0)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | rpdmgm 25203 | A positive real number is in the domain of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | dmgmn0 25204 | If 𝐴 is not a nonpositive integer, then 𝐴 is nonzero. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | dmgmaddnn0 25205 | If 𝐴 is not a nonpositive integer and 𝑁 is a nonnegative integer, then 𝐴 + 𝑁 is also not a nonpositive integer. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴 + 𝑁) ∈ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | dmgmdivn0 25206 | Lemma for lgamf 25220. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝐴 / 𝑀) + 1) ≠ 0) | ||
Theorem | lgamgulmlem1 25207* | Lemma for lgamgulm 25213. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} ⇒ ⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | lgamgulmlem2 25208* | Lemma for lgamgulm 25213. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁) ⇒ ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) | ||
Theorem | lgamgulmlem3 25209* | Lemma for lgamgulm 25213. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁) ⇒ ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2)))) | ||
Theorem | lgamgulmlem4 25210* | Lemma for lgamgulm 25213. (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 25211* | Lemma for lgamgulm 25213. (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 25212* | 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( ∘𝑓 + , 𝐺) ∈ dom (⇝𝑢‘𝑈) ∧ (seq1( ∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ 𝑂) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘𝑂) ≤ 𝑟))) | ||
Theorem | lgamgulm 25213* | 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( ∘𝑓 + , 𝐺) ∈ dom (⇝𝑢‘𝑈)) | ||
Theorem | lgamgulm2 25214* | 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( ∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) | ||
Theorem | lgambdd 25215* | 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 25216* | The 𝑈 regions used in the proof of lgamgulm 25213 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 25217* | The 𝑈 regions used in the proof of lgamgulm 25213 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈) | ||
Theorem | lgamcvglem 25218* | Lemma for lgamf 25220 and lgamcvg 25232. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) ⇒ ⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴)))) | ||
Theorem | lgamcl 25219 | 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 25220 | 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 25221 | 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 25222 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℂ) | ||
Theorem | eflgam 25223 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴)) | ||
Theorem | gamne0 25224 | The Gamma function is never zero. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ≠ 0) | ||
Theorem | igamval 25225 | Value of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) = if(𝐴 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝐴)))) | ||
Theorem | igamz 25226 | Value of the inverse Gamma function on nonpositive integers. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℤ ∖ ℕ) → (1/Γ‘𝐴) = 0) | ||
Theorem | igamgam 25227 | Value of the inverse Gamma function in terms of the Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (1 / (Γ‘𝐴))) | ||
Theorem | igamlgam 25228 | 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 25229 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ 1/Γ:ℂ⟶ℂ | ||
Theorem | igamcl 25230 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) ∈ ℂ) | ||
Theorem | gamigam 25231 | The Gamma function is the inverse of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) = (1 / (1/Γ‘𝐴))) | ||
Theorem | lgamcvg 25232* | The series 𝐺 converges to log Γ(𝐴) + log(𝐴). (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | lgamcvg2 25233* | The series 𝐺 converges to log Γ(𝐴 + 1). (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1))) | ||
Theorem | gamcvg 25234* | The pointwise exponential of the series 𝐺 converges to Γ(𝐴) · 𝐴. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | lgamp1 25235 | The functional equation of the (log) Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) = ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | gamp1 25236 | The functional equation of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘(𝐴 + 1)) = ((Γ‘𝐴) · 𝐴)) | ||
Theorem | gamcvg2lem 25237* | Lemma for gamcvg2 25238. (Contributed by Mario Carneiro, 10-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) = seq1( · , 𝐹)) | ||
Theorem | gamcvg2 25238* | An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( · , 𝐹) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | regamcl 25239 | The Gamma function is real for real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℝ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℝ) | ||
Theorem | relgamcl 25240 | The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (log Γ‘𝐴) ∈ ℝ) | ||
Theorem | rpgamcl 25241 | The log-Gamma function is positive real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (Γ‘𝐴) ∈ ℝ+) | ||
Theorem | lgam1 25242 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (log Γ‘1) = 0 | ||
Theorem | gam1 25243 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (Γ‘1) = 1 | ||
Theorem | facgam 25244 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) = (Γ‘(𝑁 + 1))) | ||
Theorem | gamfac 25245 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ → (Γ‘𝑁) = (!‘(𝑁 − 1))) | ||
Theorem | wilthlem1 25246 | 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 15895, (𝑁↑(𝑃 − 2)) mod 𝑃 is the modular inverse of 𝑁 in ℤ / 𝑃ℤ. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) | ||
Theorem | wilthlem2 25247* |
Lemma for wilth 25249: 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 25246 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 25248* | Lemma for wilth 25249. Here we round out the argument of wilthlem2 25247 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 25249 | 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 25248 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 25250 | The forward implication of Wilson's theorem wilth 25249 (see wilthlem3 25248), 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 𝑃)) | ||
Theorem | ftalem1 25251* | Lemma for fta 25258: "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 25252* | Lemma for fta 25258. 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 25253* | Lemma for fta 25258. There exists a global minimum of the function abs ∘ 𝐹. The proof uses a circle of radius 𝑟 where 𝑟 is the value coming from ftalem1 25251; 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 25254* | Lemma for fta 25258: Closure of the auxiliary variables for ftalem5 25255. (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 25255* | Lemma for fta 25258: Main proof. We have already shifted the minimum found in ftalem3 25253 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 25256* | Lemma for fta 25258: Discharge the auxiliary variables in ftalem5 25255. (Contributed by Mario Carneiro, 20-Sep-2014.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐹‘0) ≠ 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0))) | ||
Theorem | ftalem7 25257* | Lemma for fta 25258. 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 25258* | 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) | ||
Theorem | basellem1 25259 | Lemma for basel 25268. Closure of the sequence of roots. (Contributed by Mario Carneiro, 30-Jul-2014.) Replace OLD theorem. (Revised ba Wolf Lammen, 18-Sep-2020.) |
⊢ 𝑁 = ((2 · 𝑀) + 1) ⇒ ⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ (1...𝑀)) → ((𝐾 · π) / 𝑁) ∈ (0(,)(π / 2))) | ||
Theorem | basellem2 25260* | Lemma for basel 25268. 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 25261* | Lemma for basel 25268. 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 25262* | Lemma for basel 25268. By basellem3 25261, 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 24500. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝑁 = ((2 · 𝑀) + 1) & ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) & ⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) ⇒ ⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0})) | ||
Theorem | basellem5 25263* | Lemma for basel 25268. Using vieta1 24504, 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 25264 | Lemma for basel 25268. The function 𝐺 goes to zero because it is bounded by 1 / 𝑛. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ⇒ ⊢ 𝐺 ⇝ 0 | ||
Theorem | basellem7 25265 | Lemma for basel 25268. The function 1 + 𝐴 · 𝐺 for any fixed 𝐴 goes to 1. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) & ⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((ℕ × {1}) ∘𝑓 + ((ℕ × {𝐴}) ∘𝑓 · 𝐺)) ⇝ 1 | ||
Theorem | basellem8 25266* | Lemma for basel 25268. 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 25263. (Contributed by Mario Carneiro, 29-Jul-2014.) |
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) & ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2))) & ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘𝑓 · ((ℕ × {1}) ∘𝑓 − 𝐺)) & ⊢ 𝐽 = (𝐻 ∘𝑓 · ((ℕ × {1}) ∘𝑓 + ((ℕ × {-2}) ∘𝑓 · 𝐺))) & ⊢ 𝐾 = (𝐻 ∘𝑓 · ((ℕ × {1}) ∘𝑓 + 𝐺)) & ⊢ 𝑁 = ((2 · 𝑀) + 1) ⇒ ⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀))) | ||
Theorem | basellem9 25267* | Lemma for basel 25268. Since by basellem8 25266 𝐹 is bounded by two expressions that tend to π↑2 / 6, 𝐹 must also go to π↑2 / 6 by the squeeze theorem climsqz 14779. 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)}) ∘𝑓 · ((ℕ × {1}) ∘𝑓 − 𝐺)) & ⊢ 𝐽 = (𝐻 ∘𝑓 · ((ℕ × {1}) ∘𝑓 + ((ℕ × {-2}) ∘𝑓 · 𝐺))) & ⊢ 𝐾 = (𝐻 ∘𝑓 · ((ℕ × {1}) ∘𝑓 + 𝐺)) ⇒ ⊢ Σ𝑘 ∈ ℕ (𝑘↑-2) = ((π↑2) / 6) | ||
Theorem | basel 25268 | 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) | ||
Syntax | ccht 25269 | Extend class notation with the first Chebyshev function. |
class θ | ||
Syntax | cvma 25270 | Extend class notation with the von Mangoldt function. |
class Λ | ||
Syntax | cchp 25271 | Extend class notation with the second Chebyshev function. |
class ψ | ||
Syntax | cppi 25272 | Extend class notation with the prime-counting function pi. |
class π | ||
Syntax | cmu 25273 | Extend class notation with the Möbius function. |
class μ | ||
Syntax | csgm 25274 | Extend class notation with the divisor function. |
class σ | ||
Definition | df-cht 25275* | 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 25277. See https://en.wikipedia.org/wiki/Chebyshev_function for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝)) | ||
Definition | df-vma 25276* | 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 25277* | 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 25278 | 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 25279* | 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 25280* | 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 25281* | Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (exp‘𝐵) ∈ ℕ) ⇒ ⊢ (𝜑 → (exp‘Σ𝑘 ∈ 𝐴 𝐵) ∈ ℕ) | ||
Theorem | ppisval 25282 | The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ)) | ||
Theorem | ppisval2 25283 | The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈ (ℤ≥‘𝑀)) → ((0[,]𝐴) ∩ ℙ) = ((𝑀...(⌊‘𝐴)) ∩ ℙ)) | ||
Theorem | ppifi 25284 | The set of primes less than 𝐴 is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin) | ||
Theorem | prmdvdsfi 25285* | The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin) | ||
Theorem | chtf 25286 | Domain and range of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ θ:ℝ⟶ℝ | ||
Theorem | chtcl 25287 | Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ) | ||
Theorem | chtval 25288* | Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) | ||
Theorem | efchtcl 25289 | 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 25290 | The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (θ‘𝐴)) | ||
Theorem | vmaval 25291* | Value of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ 𝑆 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ⇒ ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) = if((♯‘𝑆) = 1, (log‘∪ 𝑆), 0)) | ||
Theorem | isppw 25292* | Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝐴)) | ||
Theorem | isppw2 25293* | Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | ||
Theorem | vmappw 25294 | Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (Λ‘(𝑃↑𝐾)) = (log‘𝑃)) | ||
Theorem | vmaprm 25295 | Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝑃 ∈ ℙ → (Λ‘𝑃) = (log‘𝑃)) | ||
Theorem | vmacl 25296 | Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ) | ||
Theorem | vmaf 25297 | Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ Λ:ℕ⟶ℝ | ||
Theorem | efvmacl 25298 | The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (exp‘(Λ‘𝐴)) ∈ ℕ) | ||
Theorem | vmage0 25299 | The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴)) | ||
Theorem | chpval 25300* | Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |