P. 476 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47501-47600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fourierclim 47501*	Fourier series convergence, for piecewise smooth functions. See fourier 47502 for the analogous Σ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹:ℝ⟶ℝ    &   ⊢ 𝑇 = (2 · π)    &   ⊢ (𝑥 ∈ ℝ → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    &   ⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))    &   ⊢ (( -π(,)π) ∖ dom 𝐺) ∈ Fin    &   ⊢ 𝐺 ∈ (dom 𝐺–cn→ℂ)    &   ⊢ (𝑥 ∈ (( -π[,)π) ∖ dom 𝐺) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅)    &   ⊢ (𝑥 ∈ (( -π(,]π) ∖ dom 𝐺) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅)    &   ⊢ 𝑋 ∈ ℝ    &   ⊢ 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)    &   ⊢ 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))    ⇒   ⊢ seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2))
Theorem	fourier 47502*	Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 47503. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 47504 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 47509. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹:ℝ⟶ℝ    &   ⊢ 𝑇 = (2 · π)    &   ⊢ (𝑥 ∈ ℝ → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    &   ⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))    &   ⊢ (( -π(,)π) ∖ dom 𝐺) ∈ Fin    &   ⊢ 𝐺 ∈ (dom 𝐺–cn→ℂ)    &   ⊢ (𝑥 ∈ (( -π[,)π) ∖ dom 𝐺) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅)    &   ⊢ (𝑥 ∈ (( -π(,]π) ∖ dom 𝐺) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅)    &   ⊢ 𝑋 ∈ ℝ    &   ⊢ 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)    &   ⊢ 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    ⇒   ⊢ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)
Theorem	fouriercnp 47503*	If 𝐹 is continuous at the point 𝑋, then its Fourier series at 𝑋, converges to (𝐹‘𝑋). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ 𝑇 = (2 · π)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    &   ⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))    &   ⊢ (𝜑 → (( -π(,)π) ∖ dom 𝐺) ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 CnP 𝐽)‘𝑋))    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    ⇒   ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝐹‘𝑋))
Theorem	fourier2 47504*	Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of 𝐹 at any given point 𝑋. See fourierd 47499 for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ 𝑇 = (2 · π)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    &   ⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))    &   ⊢ (𝜑 → (( -π(,)π) ∖ dom 𝐺) ∈ Fin)    &   ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    ⇒   ⊢ (𝜑 → ∃𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2))
Theorem	sqwvfoura 47505*	Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the 𝐴 coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (2 · π)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)
Theorem	sqwvfourb 47506*	Fourier series 𝐵 coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (2 · π)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
Theorem	fourierswlem 47507*	The Fourier series for the square wave 𝐹 converges to 𝑌, a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (2 · π)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))    &   ⊢ 𝑋 ∈ ℝ    &   ⊢ 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋))    ⇒   ⊢ 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)
Theorem	fouriersw 47508*	Fourier series convergence, for the square wave function. Where 𝐹 is discontinuous, the series converges to 0, the average value of the left and the right limits. Notice that 𝐹 is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (2 · π)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))    &   ⊢ 𝑋 ∈ ℝ    &   ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((sin‘(((2 · 𝑛) − 1) · 𝑋)) / ((2 · 𝑛) − 1)))    &   ⊢ 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋))    ⇒   ⊢ (((4 / π) · Σ𝑘 ∈ ℕ ((sin‘(((2 · 𝑘) − 1) · 𝑋)) / ((2 · 𝑘) − 1))) = 𝑌 ∧ seq1( + , 𝑆) ⇝ ((π / 4) · 𝑌))
Theorem	fouriercn 47509*	If the derivative of 𝐹 is continuous, then the Fourier series for 𝐹 converges to 𝐹 everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function (see fourierd 47499 for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ 𝑇 = (2 · π)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (ℝ–cn→ℂ))    &   ⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    ⇒   ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝐹‘𝑋))
21.47.17  e is transcendental
Theorem	elaa2lem 47510*	Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 47511. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝔸)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ (𝜑 → (𝐺‘𝐴) = 0)    &   ⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )    &   ⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))    &   ⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)))    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))
Theorem	elaa2 47511*	Elementhood in the set of nonzero algebraic numbers: when 𝐴 is nonzero, the polynomial 𝑓 can be chosen with a nonzero constant term. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 1-Oct-2020.)
⊢ (𝐴 ∈ (𝔸 ∖ {0}) ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)))
Theorem	etransclem1 47512*	𝐻 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    ⇒   ⊢ (𝜑 → (𝐻‘𝐽):𝑋⟶ℂ)
Theorem	etransclem2 47513*	Derivative of 𝐺. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))    ⇒   ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
Theorem	etransclem3 47514	The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ)
Theorem	etransclem4 47515*	𝐹 expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ 𝐸 = (𝑥 ∈ 𝐴 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐸)
Theorem	etransclem5 47516*	A change of bound variable, often used in proofs for etransc 47560. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
Theorem	etransclem6 47517*	A change of bound variable, often used in proofs for etransc 47560. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
Theorem	etransclem7 47518*	The given product is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ)
Theorem	etransclem8 47519*	𝐹 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
Theorem	etransclem9 47520	If 𝐾 divides 𝑁 but 𝐾 does not divide 𝑀 then 𝑀 + 𝑁 cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≠ 0)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → ¬ 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀 + 𝑁) ≠ 0)
Theorem	etransclem10 47521	The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈ ℤ)
Theorem	etransclem11 47522*	A change of bound variable, often used in proofs for etransc 47560. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})
Theorem	etransclem12 47523*	𝐶 applied to 𝑁. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) = {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁})
Theorem	etransclem13 47524*	𝐹 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘𝑌) = ∏𝑗 ∈ (0...𝑀)((𝑌 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))
Theorem	etransclem14 47525*	Value of the term 𝑇, when 𝐽 = 0 and (𝐶‘0) = 𝑃 − 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁))    &   ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))    &   ⊢ (𝜑 → 𝐽 = 0)    &   ⊢ (𝜑 → (𝐶‘0) = (𝑃 − 1))    ⇒   ⊢ (𝜑 → 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ( -𝑗↑(𝑃 − (𝐶‘𝑗))))))))
Theorem	etransclem15 47526*	Value of the term 𝑇, when 𝐽 = 0 and (𝐶‘0) = 𝑃 − 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁))    &   ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))    &   ⊢ (𝜑 → 𝐽 = 0)    &   ⊢ (𝜑 → (𝐶‘0) ≠ (𝑃 − 1))    ⇒   ⊢ (𝜑 → 𝑇 = 0)
Theorem	etransclem16 47527*	Every element in the range of 𝐶 is a finite set. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin)
Theorem	etransclem17 47528*	The 𝑁-th derivative of 𝐻. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))))
Theorem	etransclem18 47529*	The given function is integrable. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((e↑𝑐 -𝑥) · (𝐹‘𝑥))) ∈ 𝐿1)
Theorem	etransclem19 47530*	The 𝑁-th derivative of 𝐻 is 0 if 𝑁 is large enough. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0))
Theorem	etransclem20 47531*	𝐻 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁):𝑋⟶ℂ)
Theorem	etransclem21 47532*	The 𝑁-th derivative of 𝐻 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁)‘𝑌) = if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))
Theorem	etransclem22 47533*	The 𝑁-th derivative of 𝐻 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) ∈ (𝑋–cn→ℂ))
Theorem	etransclem23 47534*	This is the claim proof in [Juillerat] p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)    &   ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐 -𝑥) · (𝐹‘𝑥)) d𝑥)    &   ⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1)))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1)    ⇒   ⊢ (𝜑 → (abs‘𝐾) < 1)
Theorem	etransclem24 47535*	𝑃 divides the I -th derivative of 𝐹 applied to 𝐽. when 𝐽 = 0 and 𝐼 is not equal to 𝑃 − 1. This is the second part of case 2 proven in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐼 ≠ (𝑃 − 1))    &   ⊢ (𝜑 → 𝐽 = 0)    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝐼))    ⇒   ⊢ (𝜑 → 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) / (!‘(𝑃 − 1))))
Theorem	etransclem25 47536*	𝑃 factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁))    &   ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗) = 𝑁)    &   ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (!‘𝑃) ∥ 𝑇)
Theorem	etransclem26 47537*	Every term in the sum of the 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝑁))    ⇒   ⊢ (𝜑 → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) ∈ ℤ)
Theorem	etransclem27 47538*	The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → 𝐶:dom 𝐶⟶(ℕ0 ↑m (0...𝑀)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ Σ𝑙 ∈ dom 𝐶∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘((𝐶‘𝑙)‘𝑗))‘𝑥))    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐺‘𝐽) ∈ ℤ)
Theorem	etransclem28 47539*	(𝑃 − 1) factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))))    ⇒   ⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ 𝑇)
Theorem	etransclem29 47540*	The 𝑁-th derivative of 𝐹. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ 𝐸 = (𝑥 ∈ 𝑋 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥))    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥))))
Theorem	etransclem30 47541*	The 𝑁-th derivative of 𝐹. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥))))
Theorem	etransclem31 47542*	The 𝑁-th derivative of 𝐻 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑌) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝑌↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝑌 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))))
Theorem	etransclem32 47543*	This is the proof for the last equation in the proof of the derivative calculated in [Juillerat] p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < 𝑁)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0))
Theorem	etransclem33 47544*	𝐹 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝑋⟶ℂ)
Theorem	etransclem34 47545*	The 𝑁-th derivative of 𝐹 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐻 = (𝑘 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) = 𝑛})    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (𝑋–cn→ℂ))
Theorem	etransclem35 47546*	𝑃 does not divide the P-1 -th derivative of 𝐹 applied to 0. This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0))    ⇒   ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀) -𝑗↑𝑃)))
Theorem	etransclem36 47547*	The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    ⇒   ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽) ∈ ℤ)
Theorem	etransclem37 47548*	(𝑃 − 1) factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽))
Theorem	etransclem38 47549*	𝑃 divides the I -th derivative of 𝐹 applied to 𝐽. if it is not the case that 𝐼 = 𝑃 − 1 and 𝐽 = 0. This is case 1 and the second part of case 2 proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝐼 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → ¬ (𝐼 = (𝑃 − 1) ∧ 𝐽 = 0))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})    ⇒   ⊢ (𝜑 → 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘𝐼)‘𝐽) / (!‘(𝑃 − 1))))
Theorem	etransclem39 47550*	𝐺 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐺:ℝ⟶ℂ)
Theorem	etransclem40 47551*	The 𝑁-th derivative of 𝐹 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (𝑋–cn→ℂ))
Theorem	etransclem41 47552*	𝑃 does not divide the P-1 -th derivative of 𝐹 applied to 0. This is the first part of case 2: proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (!‘𝑀) < 𝑃)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))
Theorem	etransclem42 47553*	The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽) ∈ ℤ)
Theorem	etransclem43 47554*	𝐺 is a continuous function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (0...𝑅)(((𝑆 D𝑛 𝐹)‘𝑖)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))
Theorem	etransclem44 47555*	The given finite sum is nonzero. This is the claim proved after equation (7) in [Juillerat] p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)    &   ⊢ (𝜑 → (𝐴‘0) ≠ 0)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃)    &   ⊢ (𝜑 → (!‘𝑀) < 𝑃)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1)))    ⇒   ⊢ (𝜑 → 𝐾 ≠ 0)
Theorem	etransclem45 47556*	𝐾 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)    &   ⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1)))    ⇒   ⊢ (𝜑 → 𝐾 ∈ ℤ)
Theorem	etransclem46 47557*	This is the proof for equation *(7) in [Juillerat] p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to 0 for large 𝑃, but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝑄‘e) = 0)    &   ⊢ 𝐴 = (coeff‘𝑄)    &   ⊢ 𝑀 = (deg‘𝑄)    &   ⊢ (𝜑 → ℝ ⊆ ℝ)    &   ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐 -𝑥) · (𝐹‘𝑥)) d𝑥)    &   ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))    &   ⊢ 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐 -𝑥) · (𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = ( -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1))))
Theorem	etransclem47 47558*	e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝑄‘e) = 0)    &   ⊢ 𝐴 = (coeff‘𝑄)    &   ⊢ (𝜑 → (𝐴‘0) ≠ 0)    &   ⊢ 𝑀 = (deg‘𝑄)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃)    &   ⊢ (𝜑 → (!‘𝑀) < 𝑃)    &   ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐 -𝑥) · (𝐹‘𝑥)) d𝑥)    &   ⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1)))    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
Theorem	etransclem48 47559*	e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. In this lemma, a large enough prime 𝑝 is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 28-Sep-2020.)
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝑄‘e) = 0)    &   ⊢ 𝐴 = (coeff‘𝑄)    &   ⊢ (𝜑 → (𝐴‘0) ≠ 0)    &   ⊢ 𝑀 = (deg‘𝑄)    &   ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))    &   ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )    &   ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
Theorem	etransc 47560	e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. This is Metamath 100 proof #67. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 28-Sep-2020.)
⊢ e ∈ (ℂ ∖ 𝔸)
21.47.18  n-dimensional Euclidean space
Theorem	rrxtopn 47561*	The topology of the generalized real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))))
Theorem	rrxngp 47562	Generalized Euclidean real spaces are normed groups. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ NrmGrp)
Theorem	rrxtps 47563	Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ TopSp)
Theorem	rrxtopnfi 47564*	The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    ⇒   ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))))
Theorem	rrxtopon 47565	The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ (TopOn‘(Base‘(ℝ^‘𝐼))))
Theorem	rrxtop 47566	The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ Top)
Theorem	rrndistlt 47567*	Given two points in the space of n-dimensional real numbers, if every component is closer than 𝐸 then the distance between the two points is less than ((√‘𝑛) · 𝐸). (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ≠ ∅)    &   ⊢ 𝑁 = (♯‘𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼))    &   ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝐼))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑌‘𝑖))) < 𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝜑 → (𝑋𝐷𝑌) < ((√‘𝑁) · 𝐸))
Theorem	rrxtoponfi 47568	The topology on n-dimensional Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ Fin → 𝐽 ∈ (TopOn‘(ℝ ↑m 𝐼)))
Theorem	rrxunitopnfi 47569	The base set of the standard topology on the space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝑋 ∈ Fin → ∪ (TopOpen‘(ℝ^‘𝑋)) = (ℝ ↑m 𝑋))
Theorem	rrxtopn0 47570	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (TopOpen‘(ℝ^‘∅)) = 𝒫 {∅}
Theorem	qndenserrnbllem 47571*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ≠ ∅)    &   ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼))    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸))
Theorem	qndenserrnbl 47572*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼))    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸))
Theorem	rrxtopn0b 47573	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (TopOpen‘(ℝ^‘∅)) = {∅, {∅}}
Theorem	qndenserrnopnlem 47574*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ 𝑉)
Theorem	qndenserrnopn 47575*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ 𝑉)
Theorem	qndenserrn 47576	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝜑 → ((cls‘𝐽)‘(ℚ ↑m 𝐼)) = (ℝ ↑m 𝐼))
Theorem	rrxsnicc 47577*	A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴})
Theorem	rrnprjdstle 47578	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝑋))    ⇒   ⊢ (𝜑 → (abs‘((𝐹‘𝐼) − (𝐺‘𝐼))) ≤ (𝐹𝐷𝐺))
Theorem	rrndsmet 47579*	𝐷 is a metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (Met‘(ℝ ↑m 𝑋)))
Theorem	rrndsxmet 47580*	𝐷 is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋)))
Theorem	ioorrnopnlem 47581*	The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))    &   ⊢ 𝐻 = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))))    &   ⊢ 𝐸 = inf(𝐻, ℝ, < )    &   ⊢ 𝑉 = (𝐹(ball‘𝐷)𝐸)    &   ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))
Theorem	ioorrnopn 47582*	The indexed product of open intervals is an open set in (ℝ^‘𝑋). (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)    ⇒   ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋)))
Theorem	ioorrnopnxrlem 47583*	Given a point 𝐹 that belongs to an indexed product of (possibly unbounded) open intervals, then 𝐹 belongs to an open product of bounded open intervals that's a subset of the original indexed product. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*)    &   ⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))    &   ⊢ 𝐿 = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)))    &   ⊢ 𝑅 = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)))    &   ⊢ 𝑉 = X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖))    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))
Theorem	ioorrnopnxr 47584*	The indexed product of open intervals is an open set in (ℝ^‘𝑋). Similar to ioorrnopn 47582 but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*)    ⇒   ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋)))
21.47.19  Basic measure theory
21.47.19.1  σ-Algebras Proofs for most of the theorems in section 111 of [Fremlin1]
Syntax	csalg 47585	Extend class notation with the class of all sigma-algebras.
class SAlg
Definition	df-salg 47586*	Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))}
Syntax	csalon 47587	Extend class notation with the class of sigma-algebras on a set.
class SalOn
Definition	df-salon 47588*	Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥})
Syntax	csalgen 47589	Extend class notation with the class of sigma-algebra generator.
class SalGen
Definition	df-salgen 47590*	Define the sigma-algebra generated by a given set. Definition 111G (b) of [Fremlin1] p. 13. The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set, see dfsalgen2 47618. The base set of the sigma-algebras used for the intersection needs to be the same, otherwise the resulting set is not guaranteed to be a sigma-algebra, as shown in the counterexample salgencntex 47620. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.)
⊢ SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)})
Theorem	issal 47591*	Express the predicate "𝑆 is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆))))
Theorem	pwsal 47592	The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg)
Theorem	salunicl 47593	SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆)    &   ⊢ (𝜑 → 𝑇 ≼ ω)    ⇒   ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆)
Theorem	saluncl 47594	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	prsal 47595	The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)
Theorem	saldifcl 47596	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	0sal 47597	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆)
Theorem	salgenval 47598*	The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)})
Theorem	saliunclf 47599	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝑆    &   ⊢ Ⅎ𝑘𝐾    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saliuncl 47600*	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)