Metamath Proof Explorer


Theorem etransclem40

Description: The N -th derivative of F is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem40.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
etransclem40.a ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
etransclem40.p ( 𝜑𝑃 ∈ ℕ )
etransclem40.m ( 𝜑𝑀 ∈ ℕ0 )
etransclem40.f 𝐹 = ( 𝑥𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑘 ) ↑ 𝑃 ) ) )
etransclem40.6 ( 𝜑𝑁 ∈ ℕ0 )
Assertion etransclem40 ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( 𝑋cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 etransclem40.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 etransclem40.a ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem40.p ( 𝜑𝑃 ∈ ℕ )
4 etransclem40.m ( 𝜑𝑀 ∈ ℕ0 )
5 etransclem40.f 𝐹 = ( 𝑥𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑘 ) ↑ 𝑃 ) ) )
6 etransclem40.6 ( 𝜑𝑁 ∈ ℕ0 )
7 etransclem5 ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦𝑋 ↦ ( ( 𝑦𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
8 etransclem11 ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑗 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑘 ) = 𝑛 } )
9 1 2 3 4 5 6 7 8 etransclem34 ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( 𝑋cn→ ℂ ) )