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𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) )