Home | Metamath
Proof Explorer Theorem List (p. 256 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | emcllem1 25501* | Lemma for emcl 25508. The series 𝐹 and 𝐺 are sequences of real numbers that approach γ from above and below, respectively. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) ⇒ ⊢ (𝐹:ℕ⟶ℝ ∧ 𝐺:ℕ⟶ℝ) | ||
Theorem | emcllem2 25502* | Lemma for emcl 25508. 𝐹 is increasing, and 𝐺 is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) ⇒ ⊢ (𝑁 ∈ ℕ → ((𝐹‘(𝑁 + 1)) ≤ (𝐹‘𝑁) ∧ (𝐺‘𝑁) ≤ (𝐺‘(𝑁 + 1)))) | ||
Theorem | emcllem3 25503* | Lemma for emcl 25508. The function 𝐻 is the difference between 𝐹 and 𝐺. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝐻‘𝑁) = ((𝐹‘𝑁) − (𝐺‘𝑁))) | ||
Theorem | emcllem4 25504* | Lemma for emcl 25508. The difference between series 𝐹 and 𝐺 tends to zero. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) ⇒ ⊢ 𝐻 ⇝ 0 | ||
Theorem | emcllem5 25505* | Lemma for emcl 25508. The partial sums of the series 𝑇, which is used in the definition df-em 25498, is in fact the same as 𝐺. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛))))) ⇒ ⊢ 𝐺 = seq1( + , 𝑇) | ||
Theorem | emcllem6 25506* | Lemma for emcl 25508. By the previous lemmas, 𝐹 and 𝐺 must approach a common limit, which is γ by definition. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛))))) ⇒ ⊢ (𝐹 ⇝ γ ∧ 𝐺 ⇝ γ) | ||
Theorem | emcllem7 25507* | Lemma for emcl 25508 and harmonicbnd 25509. Derive bounds on γ as 𝐹(1) and 𝐺(1). (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 9-Apr-2016.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛))))) ⇒ ⊢ (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ)) | ||
Theorem | emcl 25508 | Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ γ ∈ ((1 − (log‘2))[,]1) | ||
Theorem | harmonicbnd 25509* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁)) ∈ (γ[,]1)) | ||
Theorem | harmonicbnd2 25510* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ ((1 − (log‘2))[,]γ)) | ||
Theorem | emre 25511 | The Euler-Mascheroni constant is a real number. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ γ ∈ ℝ | ||
Theorem | emgt0 25512 | The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 0 < γ | ||
Theorem | harmonicbnd3 25513* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝑁 ∈ ℕ0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ)) | ||
Theorem | harmoniclbnd 25514* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ≤ Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚)) | ||
Theorem | harmonicubnd 25515* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) ≤ ((log‘𝐴) + 1)) | ||
Theorem | harmonicbnd4 25516* | The asymptotic behavior of Σ𝑚 ≤ 𝐴, 1 / 𝑚 = log𝐴 + γ + 𝑂(1 / 𝐴). (Contributed by Mario Carneiro, 14-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴)) | ||
Theorem | fsumharmonic 25517* | Bound a finite sum based on the harmonic series, where the "strong" bound 𝐶 only applies asymptotically, and there is a "weak" bound 𝑅 for the remaining values. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 1 ≤ 𝑇)) & ⊢ (𝜑 → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 0 ≤ 𝐶) & ⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑇 ≤ (𝐴 / 𝑛)) → (abs‘𝐵) ≤ (𝐶 · 𝑛)) & ⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝐴 / 𝑛) < 𝑇) → (abs‘𝐵) ≤ 𝑅) ⇒ ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) | ||
Syntax | czeta 25518 | The Riemann zeta function. |
class ζ | ||
Definition | df-zeta 25519* | Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except 1, but going from the alternating zeta function to the regular zeta function requires dividing by 1 − 2↑(1 − 𝑠), which has zeroes other than 1. To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))) | ||
Theorem | zetacvg 25520* | The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 1 < (ℜ‘𝑆)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑘↑𝑐-𝑆)) ⇒ ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ ) | ||
Syntax | clgam 25521 | Logarithm of the Gamma function. |
class log Γ | ||
Syntax | cgam 25522 | The Gamma function. |
class Γ | ||
Syntax | cigam 25523 | The inverse Gamma function. |
class 1/Γ | ||
Definition | df-lgam 25524* | Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to log(Γ(𝑥)) because the branch cuts are placed differently (we do have exp(log Γ(𝑥)) = Γ(𝑥), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers ℤ ∖ ℕ, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))) | ||
Definition | df-gam 25525 | Define the Gamma function. See df-lgam 25524 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ Γ = (exp ∘ log Γ) | ||
Definition | df-igam 25526 | Define the inverse Gamma function, which is defined everywhere, unlike the Gamma function itself. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ 1/Γ = (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥)))) | ||
Theorem | eldmgm 25527 | Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (𝐴 ∈ ℂ ∧ ¬ -𝐴 ∈ ℕ0)) | ||
Theorem | dmgmaddn0 25528 | If 𝐴 is not a nonpositive integer, then 𝐴 + 𝑁 is nonzero for any nonnegative integer 𝑁. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ 𝑁 ∈ ℕ0) → (𝐴 + 𝑁) ≠ 0) | ||
Theorem | dmlogdmgm 25529 | 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 25530 | A positive real number is in the domain of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | dmgmn0 25531 | If 𝐴 is not a nonpositive integer, then 𝐴 is nonzero. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | dmgmaddnn0 25532 | 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 25533 | Lemma for lgamf 25547. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝐴 / 𝑀) + 1) ≠ 0) | ||
Theorem | lgamgulmlem1 25534* | Lemma for lgamgulm 25540. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} ⇒ ⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | lgamgulmlem2 25535* | Lemma for lgamgulm 25540. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁) ⇒ ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) | ||
Theorem | lgamgulmlem3 25536* | Lemma for lgamgulm 25540. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁) ⇒ ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2)))) | ||
Theorem | lgamgulmlem4 25537* | Lemma for lgamgulm 25540. (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 25538* | Lemma for lgamgulm 25540. (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 25539* | 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 25540* | 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 25541* | 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 25542* | 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 25543* | The 𝑈 regions used in the proof of lgamgulm 25540 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 25544* | The 𝑈 regions used in the proof of lgamgulm 25540 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈) | ||
Theorem | lgamcvglem 25545* | Lemma for lgamf 25547 and lgamcvg 25559. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) ⇒ ⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴)))) | ||
Theorem | lgamcl 25546 | 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 25547 | 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 25548 | 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 25549 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℂ) | ||
Theorem | eflgam 25550 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴)) | ||
Theorem | gamne0 25551 | The Gamma function is never zero. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ≠ 0) | ||
Theorem | igamval 25552 | Value of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) = if(𝐴 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝐴)))) | ||
Theorem | igamz 25553 | Value of the inverse Gamma function on nonpositive integers. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℤ ∖ ℕ) → (1/Γ‘𝐴) = 0) | ||
Theorem | igamgam 25554 | Value of the inverse Gamma function in terms of the Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (1 / (Γ‘𝐴))) | ||
Theorem | igamlgam 25555 | 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 25556 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ 1/Γ:ℂ⟶ℂ | ||
Theorem | igamcl 25557 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) ∈ ℂ) | ||
Theorem | gamigam 25558 | The Gamma function is the inverse of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) = (1 / (1/Γ‘𝐴))) | ||
Theorem | lgamcvg 25559* | The series 𝐺 converges to log Γ(𝐴) + log(𝐴). (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | lgamcvg2 25560* | The series 𝐺 converges to log Γ(𝐴 + 1). (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1))) | ||
Theorem | gamcvg 25561* | The pointwise exponential of the series 𝐺 converges to Γ(𝐴) · 𝐴. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | lgamp1 25562 | The functional equation of the (log) Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) = ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | gamp1 25563 | The functional equation of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘(𝐴 + 1)) = ((Γ‘𝐴) · 𝐴)) | ||
Theorem | gamcvg2lem 25564* | Lemma for gamcvg2 25565. (Contributed by Mario Carneiro, 10-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) = seq1( · , 𝐹)) | ||
Theorem | gamcvg2 25565* | An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( · , 𝐹) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | regamcl 25566 | The Gamma function is real for real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℝ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℝ) | ||
Theorem | relgamcl 25567 | The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (log Γ‘𝐴) ∈ ℝ) | ||
Theorem | rpgamcl 25568 | The log-Gamma function is positive real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (Γ‘𝐴) ∈ ℝ+) | ||
Theorem | lgam1 25569 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (log Γ‘1) = 0 | ||
Theorem | gam1 25570 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (Γ‘1) = 1 | ||
Theorem | facgam 25571 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) = (Γ‘(𝑁 + 1))) | ||
Theorem | gamfac 25572 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ → (Γ‘𝑁) = (!‘(𝑁 − 1))) | ||
Theorem | wilthlem1 25573 | 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 16113, (𝑁↑(𝑃 − 2)) mod 𝑃 is the modular inverse of 𝑁 in ℤ / 𝑃ℤ. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) | ||
Theorem | wilthlem2 25574* |
Lemma for wilth 25576: 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 25573 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 25575* | Lemma for wilth 25576. Here we round out the argument of wilthlem2 25574 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 25576 | 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 25575 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 25577 | The forward implication of Wilson's theorem wilth 25576 (see wilthlem3 25575), 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 25578* | Lemma for fta 25585: "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 25579* | Lemma for fta 25585. 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 25580* | Lemma for fta 25585. There exists a global minimum of the function abs ∘ 𝐹. The proof uses a circle of radius 𝑟 where 𝑟 is the value coming from ftalem1 25578; 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 25581* | Lemma for fta 25585: Closure of the auxiliary variables for ftalem5 25582. (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 25582* | Lemma for fta 25585: Main proof. We have already shifted the minimum found in ftalem3 25580 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 25583* | Lemma for fta 25585: Discharge the auxiliary variables in ftalem5 25582. (Contributed by Mario Carneiro, 20-Sep-2014.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐹‘0) ≠ 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0))) | ||
Theorem | ftalem7 25584* | Lemma for fta 25585. 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 25585* | 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 25586 | Lemma for basel 25595. 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 25587* | Lemma for basel 25595. 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 25588* | Lemma for basel 25595. 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 25589* | Lemma for basel 25595. By basellem3 25588, 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 24826. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝑁 = ((2 · 𝑀) + 1) & ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) & ⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) ⇒ ⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0})) | ||
Theorem | basellem5 25590* | Lemma for basel 25595. Using vieta1 24830, 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 25591 | Lemma for basel 25595. The function 𝐺 goes to zero because it is bounded by 1 / 𝑛. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ⇒ ⊢ 𝐺 ⇝ 0 | ||
Theorem | basellem7 25592 | Lemma for basel 25595. 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 25593* | Lemma for basel 25595. 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 25590. (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 25594* | Lemma for basel 25595. Since by basellem8 25593 𝐹 is bounded by two expressions that tend to π↑2 / 6, 𝐹 must also go to π↑2 / 6 by the squeeze theorem climsqz 14987. 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 25595 | 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 25596 | Extend class notation with the first Chebyshev function. |
class θ | ||
Syntax | cvma 25597 | Extend class notation with the von Mangoldt function. |
class Λ | ||
Syntax | cchp 25598 | Extend class notation with the second Chebyshev function. |
class ψ | ||
Syntax | cppi 25599 | Extend class notation with the prime-counting function pi. |
class π | ||
Syntax | cmu 25600 | Extend class notation with the Möbius function. |
class μ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |