Theorem etransclem43

Description: G is a continuous function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		etransclem43.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem43.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem43.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem43.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
5		etransclem43.f	$$⊢F=\left(x\in X⟼x^{P-1}\prod _{j=1}^M{\left(x-j\right)}^P\right)$$
6		etransclem43.g	$$⊢G=\left(x\in X⟼\sum _{i=0}^R\left(S{D}^{n}F\right)\left(i\right)\left(x\right)\right)$$
7	1 2	dvdmsscn	$$⊢\phi \to X\subseteq ℂ$$
8		fzfid	$$⊢\phi \to \left(0\dots R\right)\in \mathrm{Fin}$$
9	1	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to S\in \left\{ℝ,ℂ\right\}$$
10	2	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
11	3	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to P\in \mathbb{N}$$
12	4	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to M\in {\mathbb{N}}_0$$
13		elfznn0	$$⊢i\in \left(0\dots R\right)\to i\in {\mathbb{N}}_0$$
14	13	adantl	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to i\in {\mathbb{N}}_0$$
15	9 10 11 12 5 14	etransclem33	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to \left(S{D}^{n}F\right)\left(i\right):X⟶ℂ$$
16	15	feqmptd	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to \left(S{D}^{n}F\right)\left(i\right)=\left(x\in X⟼\left(S{D}^{n}F\right)\left(i\right)\left(x\right)\right)$$
17	9 10 11 12 5 14	etransclem40	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to \left(S{D}^{n}F\right)\left(i\right):X\underset{cn}{⟶}ℂ$$
18	16 17	eqeltrrd	$$⊢\left(\phi \wedge i\in \left(0\dots R\right)\right)\to \left(x\in X⟼\left(S{D}^{n}F\right)\left(i\right)\left(x\right)\right):X\underset{cn}{⟶}ℂ$$
19	7 8 18	fsumcncf	$$⊢\phi \to \left(x\in X⟼\sum _{i=0}^R\left(S{D}^{n}F\right)\left(i\right)\left(x\right)\right):X\underset{cn}{⟶}ℂ$$
20	6 19	eqeltrid	$$⊢\phi \to G:X\underset{cn}{⟶}ℂ$$