Description: The N -th derivative of F . (Contributed by Glauco Siliprandi, 5-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | etransclem30.s | ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) | |
etransclem30.a | ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) | ||
etransclem30.p | ⊢ ( 𝜑 → 𝑃 ∈ ℕ ) | ||
etransclem30.m | ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) | ||
etransclem30.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) | ||
etransclem30.n | ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) | ||
etransclem30.h | ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) | ||
etransclem30.c | ⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) | ||
Assertion | etransclem30 | ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | etransclem30.s | ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) | |
2 | etransclem30.a | ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) | |
3 | etransclem30.p | ⊢ ( 𝜑 → 𝑃 ∈ ℕ ) | |
4 | etransclem30.m | ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) | |
5 | etransclem30.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) | |
6 | etransclem30.n | ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) | |
7 | etransclem30.h | ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) | |
8 | etransclem30.c | ⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) | |
9 | eqid | ⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) ) | |
10 | 1 2 3 4 5 6 7 8 9 | etransclem29 | ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) ) |