![]() |
Metamath
Proof Explorer Theorem List (p. 272 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gamcl 27101 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℂ) | ||
Theorem | eflgam 27102 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴)) | ||
Theorem | gamne0 27103 | The Gamma function is never zero. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ≠ 0) | ||
Theorem | igamval 27104 | Value of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) = if(𝐴 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝐴)))) | ||
Theorem | igamz 27105 | Value of the inverse Gamma function on nonpositive integers. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℤ ∖ ℕ) → (1/Γ‘𝐴) = 0) | ||
Theorem | igamgam 27106 | Value of the inverse Gamma function in terms of the Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (1 / (Γ‘𝐴))) | ||
Theorem | igamlgam 27107 | 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 27108 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ 1/Γ:ℂ⟶ℂ | ||
Theorem | igamcl 27109 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) ∈ ℂ) | ||
Theorem | gamigam 27110 | The Gamma function is the inverse of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) = (1 / (1/Γ‘𝐴))) | ||
Theorem | lgamcvg 27111* | The series 𝐺 converges to log Γ(𝐴) + log(𝐴). (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | lgamcvg2 27112* | The series 𝐺 converges to log Γ(𝐴 + 1). (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1))) | ||
Theorem | gamcvg 27113* | The pointwise exponential of the series 𝐺 converges to Γ(𝐴) · 𝐴. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | lgamp1 27114 | The functional equation of the (log) Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) = ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | gamp1 27115 | The functional equation of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘(𝐴 + 1)) = ((Γ‘𝐴) · 𝐴)) | ||
Theorem | gamcvg2lem 27116* | Lemma for gamcvg2 27117. (Contributed by Mario Carneiro, 10-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) = seq1( · , 𝐹)) | ||
Theorem | gamcvg2 27117* | An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( · , 𝐹) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | regamcl 27118 | The Gamma function is real for real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℝ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℝ) | ||
Theorem | relgamcl 27119 | The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (log Γ‘𝐴) ∈ ℝ) | ||
Theorem | rpgamcl 27120 | The log-Gamma function is positive real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (Γ‘𝐴) ∈ ℝ+) | ||
Theorem | lgam1 27121 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (log Γ‘1) = 0 | ||
Theorem | gam1 27122 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (Γ‘1) = 1 | ||
Theorem | facgam 27123 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) = (Γ‘(𝑁 + 1))) | ||
Theorem | gamfac 27124 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ → (Γ‘𝑁) = (!‘(𝑁 − 1))) | ||
Theorem | wilthlem1 27125 | 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 16819, (𝑁↑(𝑃 − 2)) mod 𝑃 is the modular inverse of 𝑁 in ℤ / 𝑃ℤ. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) | ||
Theorem | wilthlem2 27126* |
Lemma for wilth 27128: 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 27125 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 27127* | Lemma for wilth 27128. Here we round out the argument of wilthlem2 27126 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 27128 | 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 27127 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 27129 | The forward implication of Wilson's theorem wilth 27128 (see wilthlem3 27127), 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 27130* | Lemma for fta 27137: "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 27131* | Lemma for fta 27137. 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 27132* | Lemma for fta 27137. There exists a global minimum of the function abs ∘ 𝐹. The proof uses a circle of radius 𝑟 where 𝑟 is the value coming from ftalem1 27130; 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 27133* | Lemma for fta 27137: Closure of the auxiliary variables for ftalem5 27134. (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 27134* | Lemma for fta 27137: Main proof. We have already shifted the minimum found in ftalem3 27132 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 27135* | Lemma for fta 27137: Discharge the auxiliary variables in ftalem5 27134. (Contributed by Mario Carneiro, 20-Sep-2014.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐹‘0) ≠ 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0))) | ||
Theorem | ftalem7 27136* | Lemma for fta 27137. 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 27137* | 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 27138 | Lemma for basel 27147. 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 27139* | Lemma for basel 27147. 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 27140* | Lemma for basel 27147. 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 27141* | Lemma for basel 27147. By basellem3 27140, 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 26364. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝑁 = ((2 · 𝑀) + 1) & ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) & ⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) ⇒ ⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0})) | ||
Theorem | basellem5 27142* | Lemma for basel 27147. Using vieta1 26368, 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 27143 | Lemma for basel 27147. The function 𝐺 goes to zero because it is bounded by 1 / 𝑛. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ⇒ ⊢ 𝐺 ⇝ 0 | ||
Theorem | basellem7 27144 | Lemma for basel 27147. 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 27145* | Lemma for basel 27147. 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 27142. (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 27146* | Lemma for basel 27147. Since by basellem8 27145 𝐹 is bounded by two expressions that tend to π↑2 / 6, 𝐹 must also go to π↑2 / 6 by the squeeze theorem climsqz 15673. 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 27147 | 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 27148 | Extend class notation with the first Chebyshev function. |
class θ | ||
Syntax | cvma 27149 | Extend class notation with the von Mangoldt function. |
class Λ | ||
Syntax | cchp 27150 | Extend class notation with the second Chebyshev function. |
class ψ | ||
Syntax | cppi 27151 | Extend class notation with the prime-counting function pi. |
class π | ||
Syntax | cmu 27152 | Extend class notation with the Möbius function. |
class μ | ||
Syntax | csgm 27153 | Extend class notation with the divisor function. |
class σ | ||
Definition | df-cht 27154* | 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 27156. See https://en.wikipedia.org/wiki/Chebyshev_function 27156 for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝)) | ||
Definition | df-vma 27155* | 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 27156* | 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 27157 | 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 27158* | 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 27159* | 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 27160* | Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (exp‘𝐵) ∈ ℕ) ⇒ ⊢ (𝜑 → (exp‘Σ𝑘 ∈ 𝐴 𝐵) ∈ ℕ) | ||
Theorem | ppisval 27161 | The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ)) | ||
Theorem | ppisval2 27162 | The set of primes less than 𝐴 expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈ (ℤ≥‘𝑀)) → ((0[,]𝐴) ∩ ℙ) = ((𝑀...(⌊‘𝐴)) ∩ ℙ)) | ||
Theorem | ppifi 27163 | The set of primes less than 𝐴 is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin) | ||
Theorem | prmdvdsfi 27164* | The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin) | ||
Theorem | chtf 27165 | Domain and codoamin of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ θ:ℝ⟶ℝ | ||
Theorem | chtcl 27166 | Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ) | ||
Theorem | chtval 27167* | Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) | ||
Theorem | efchtcl 27168 | 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 27169 | The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (θ‘𝐴)) | ||
Theorem | vmaval 27170* | Value of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ 𝑆 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ⇒ ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) = if((♯‘𝑆) = 1, (log‘∪ 𝑆), 0)) | ||
Theorem | isppw 27171* | Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝐴)) | ||
Theorem | isppw2 27172* | Two ways to say that 𝐴 is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | ||
Theorem | vmappw 27173 | Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (Λ‘(𝑃↑𝐾)) = (log‘𝑃)) | ||
Theorem | vmaprm 27174 | Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝑃 ∈ ℙ → (Λ‘𝑃) = (log‘𝑃)) | ||
Theorem | vmacl 27175 | Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ) | ||
Theorem | vmaf 27176 | Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ Λ:ℕ⟶ℝ | ||
Theorem | efvmacl 27177 | The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → (exp‘(Λ‘𝐴)) ∈ ℕ) | ||
Theorem | vmage0 27178 | The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℕ → 0 ≤ (Λ‘𝐴)) | ||
Theorem | chpval 27179* | Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(Λ‘𝑛)) | ||
Theorem | chpf 27180 | Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ ψ:ℝ⟶ℝ | ||
Theorem | chpcl 27181 | Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ) | ||
Theorem | efchpcl 27182 | The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → (exp‘(ψ‘𝐴)) ∈ ℕ) | ||
Theorem | chpge0 27183 | The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (ψ‘𝐴)) | ||
Theorem | ppival 27184 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) = (♯‘((0[,]𝐴) ∩ ℙ))) | ||
Theorem | ppival2 27185 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (π‘𝐴) = (♯‘((2...𝐴) ∩ ℙ))) | ||
Theorem | ppival2g 27186 | Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 2 ∈ (ℤ≥‘𝑀)) → (π‘𝐴) = (♯‘((𝑀...𝐴) ∩ ℙ))) | ||
Theorem | ppif 27187 | Domain and codomain of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ π:ℝ⟶ℕ0 | ||
Theorem | ppicl 27188 | Real closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (π‘𝐴) ∈ ℕ0) | ||
Theorem | muval 27189* | The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) = if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴})))) | ||
Theorem | muval1 27190 | The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑃 ∈ (ℤ≥‘2) ∧ (𝑃↑2) ∥ 𝐴) → (μ‘𝐴) = 0) | ||
Theorem | muval2 27191* | The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) → (μ‘𝐴) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}))) | ||
Theorem | isnsqf 27192* | Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) = 0 ↔ ∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝐴)) | ||
Theorem | issqf 27193* | Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝐴 ∈ ℕ → ((μ‘𝐴) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1)) | ||
Theorem | sqfpc 27194 | The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt 𝐴) ≤ 1) | ||
Theorem | dvdssqf 27195 | A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → ((μ‘𝐴) ≠ 0 → (μ‘𝐵) ≠ 0)) | ||
Theorem | sqf11 27196* | A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015.) |
⊢ (((𝐴 ∈ ℕ ∧ (μ‘𝐴) ≠ 0) ∧ (𝐵 ∈ ℕ ∧ (μ‘𝐵) ≠ 0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) | ||
Theorem | muf 27197 | The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ μ:ℕ⟶ℤ | ||
Theorem | mucl 27198 | Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → (μ‘𝐴) ∈ ℤ) | ||
Theorem | sgmval 27199* | The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝑐𝐴)) | ||
Theorem | sgmval2 27200* | The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 σ 𝐵) = Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} (𝑘↑𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |