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