Metamath Proof Explorer


Theorem etransclem29

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

Ref Expression
Hypotheses etranslemdvnf2lemlem.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
etransclem29.a ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
etransclem29.p ( 𝜑𝑃 ∈ ℕ )
etransclem29.m ( 𝜑𝑀 ∈ ℕ0 )
etransclem29.f 𝐹 = ( 𝑥𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) )
etransclem29.n ( 𝜑𝑁 ∈ ℕ0 )
etransclem29.h 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
etransclem29.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
etransclem29.e 𝐸 = ( 𝑥𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻𝑗 ) ‘ 𝑥 ) )
Assertion etransclem29 ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( 𝐶𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑗 ) ) ‘ ( 𝑐𝑗 ) ) ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 etranslemdvnf2lemlem.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 etransclem29.a ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem29.p ( 𝜑𝑃 ∈ ℕ )
4 etransclem29.m ( 𝜑𝑀 ∈ ℕ0 )
5 etransclem29.f 𝐹 = ( 𝑥𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) )
6 etransclem29.n ( 𝜑𝑁 ∈ ℕ0 )
7 etransclem29.h 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
8 etransclem29.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
9 etransclem29.e 𝐸 = ( 𝑥𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻𝑗 ) ‘ 𝑥 ) )
10 1 2 dvdmsscn ( 𝜑𝑋 ⊆ ℂ )
11 10 3 4 5 7 9 etransclem4 ( 𝜑𝐹 = 𝐸 )
12 11 oveq2d ( 𝜑 → ( 𝑆 D𝑛 𝐹 ) = ( 𝑆 D𝑛 𝐸 ) )
13 12 fveq1d ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐸 ) ‘ 𝑁 ) )
14 fzfid ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
15 10 adantr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ⊆ ℂ )
16 3 adantr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
17 simpr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
18 15 16 7 17 etransclem1 ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐻𝑗 ) : 𝑋 ⟶ ℂ )
19 1 3ad2ant1 ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
20 2 3ad2ant1 ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
21 3 3ad2ant1 ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑃 ∈ ℕ )
22 etransclem5 ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦𝑋 ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
23 7 22 eqtri 𝐻 = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦𝑋 ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
24 simp2 ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
25 elfznn0 ( 𝑖 ∈ ( 0 ... 𝑁 ) → 𝑖 ∈ ℕ0 )
26 25 3ad2ant3 ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ℕ0 )
27 19 20 21 23 24 26 etransclem20 ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑗 ) ) ‘ 𝑖 ) : 𝑋 ⟶ ℂ )
28 1 2 14 18 6 27 9 8 dvnprod ( 𝜑 → ( ( 𝑆 D𝑛 𝐸 ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( 𝐶𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑗 ) ) ‘ ( 𝑐𝑗 ) ) ‘ 𝑥 ) ) ) )
29 13 28 eqtrd ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( 𝐶𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑗 ) ) ‘ ( 𝑐𝑗 ) ) ‘ 𝑥 ) ) ) )