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→ ℂ ) ) |