Theorem etransclem40

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

	Ref	Expression
Hypotheses	etransclem40.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	etransclem40.a	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
	etransclem40.p	$$⊢\phi \to P\in \mathbb{N}$$
	etransclem40.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	etransclem40.f	$$⊢F=\left(x\in X⟼x^{P-1}\prod _{k=1}^M{\left(x-k\right)}^P\right)$$
	etransclem40.6	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	etransclem40	$$⊢\phi \to \left(S{D}^{n}F\right)\left(N\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		etransclem40.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem40.a	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem40.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem40.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
5		etransclem40.f	$$⊢F=\left(x\in X⟼x^{P-1}\prod _{k=1}^M{\left(x-k\right)}^P\right)$$
6		etransclem40.6	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		etransclem5	$$⊢\left(j\in \left(0\dots M\right)⟼\left(y\in X⟼{\left(y-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)=\left(k\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-k\right)}^{if\left(k=0,P-1,P\right)}\right)\right)$$
8		etransclem11	$$⊢\left(m\in {\mathbb{N}}_0⟼\left\{d\in \left({\left(0\dots m\right)}^{\left(0\dots M\right)}\right)|\sum _{j=0}^{M}d\left(j\right)=m\right\}\right)=\left(n\in {\mathbb{N}}_0⟼\left\{c\in \left({\left(0\dots n\right)}^{\left(0\dots M\right)}\right)|\sum _{k=0}^{M}c\left(k\right)=n\right\}\right)$$
9	1 2 3 4 5 6 7 8	etransclem34	$$⊢\phi \to \left(S{D}^{n}F\right)\left(N\right):X\underset{cn}{⟶}ℂ$$