Theorem etransclem34

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

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

Proof

Step	Hyp	Ref	Expression
1		etransclem34.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		etransclem34.a	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3		etransclem34.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4		etransclem34.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5		etransclem34.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ 𝑃 ) ) )
6		etransclem34.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7		etransclem34.h	⊢ 𝐻 = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
8		etransclem34.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) = 𝑛 } )
9	1 2 3 4 5 6 7 8	etransclem30	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ) · ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) ) ) )
10	1 2	dvdmsscn	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
11	8 6	etransclem16	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ∈ Fin )
12	10	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑋 ⊆ ℂ )
13	6	faccld	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
14	13	nncnd	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
16		fzfid	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 0 ... 𝑀 ) ∈ Fin )
17		fzssnn0	⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
18		ssrab2	⊢ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) = 𝑁 } ⊆ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) )
20	8 6	etransclem12	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) = 𝑁 } )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝐶 ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) = 𝑁 } )
22	19 21	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) = 𝑁 } )
23	18 22	sselid	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
24		elmapi	⊢ ( 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
25	23 24	syl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
26	25	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ( 0 ... 𝑁 ) )
27	17 26	sselid	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ℕ0 )
28	27	faccld	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ∈ ℕ )
29	28	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ∈ ℂ )
30	16 29	fprodcl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ∈ ℂ )
31	28	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ≠ 0 )
32	16 29 31	fprodn0	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ≠ 0 )
33	15 30 32	divcld	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ) ∈ ℂ )
34		ssid	⊢ ℂ ⊆ ℂ
35	34	a1i	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ℂ ⊆ ℂ )
36	12 33 35	constcncfg	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ! ‘ 𝑁 ) / ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
37	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑆 ∈ { ℝ , ℂ } )
38	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
39	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
40		etransclem5	⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
41	7 40	eqtri	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
42		simpr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
43	37 38 39 41 42 27	etransclem20	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) : 𝑋 ⟶ ℂ )
44	43	3adant2	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) : 𝑋 ⟶ ℂ )
45		simp2	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ 𝑋 )
46	44 45	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) ∈ ℂ )
47	43	feqmptd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) ) )
48	37 38 39 41 42 27	etransclem22	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
49	47 48	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
50	12 16 46 49	fprodcncf	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
51	36 50	mulcncf	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ) · ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
52	10 11 51	fsumcncf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ) · ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
53	9 52	eqeltrd	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( 𝑋 –cn→ ℂ ) )