Theorem etransclem22

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

	Ref	Expression
Hypotheses	etransclem22.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	etransclem22.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
	etransclem22.p	$$⊢\phi \to P\in \mathbb{N}$$
	etransclem22.h	$$⊢H=\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)$$
	etransclem22.J	$$⊢\phi \to J\in \left(0\dots M\right)$$
	etransclem22.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	etransclem22	$$⊢\phi \to \left(S{D}^{n}H\left(J\right)\right)\left(N\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		etransclem22.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem22.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem22.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem22.h	$$⊢H=\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)$$
5		etransclem22.J	$$⊢\phi \to J\in \left(0\dots M\right)$$
6		etransclem22.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7	1 2 3 4 5 6	etransclem17	$$⊢\phi \to \left(S{D}^{n}H\left(J\right)\right)\left(N\right)=\left(x\in X⟼if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right)$$
8		simpr	$$⊢\left(\phi \wedge if\left(J=0,P-1,P\right)<N\right)\to if\left(J=0,P-1,P\right)<N$$
9	8	iftrued	$$⊢\left(\phi \wedge if\left(J=0,P-1,P\right)<N\right)\to if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)=0$$
10	9	mpteq2dv	$$⊢\left(\phi \wedge if\left(J=0,P-1,P\right)<N\right)\to \left(x\in X⟼if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right)=\left(x\in X⟼0\right)$$
11	1 2	dvdmsscn	$$⊢\phi \to X\subseteq ℂ$$
12		0cnd	$$⊢\phi \to 0\in ℂ$$
13		ssid	$$⊢ℂ\subseteq ℂ$$
14	13	a1i	$$⊢\phi \to ℂ\subseteq ℂ$$
15	11 12 14	constcncfg	$$⊢\phi \to \left(x\in X⟼0\right):X\underset{cn}{⟶}ℂ$$
16	15	adantr	$$⊢\left(\phi \wedge if\left(J=0,P-1,P\right)<N\right)\to \left(x\in X⟼0\right):X\underset{cn}{⟶}ℂ$$
17	10 16	eqeltrd	$$⊢\left(\phi \wedge if\left(J=0,P-1,P\right)<N\right)\to \left(x\in X⟼if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right):X\underset{cn}{⟶}ℂ$$
18		simpr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \neg if\left(J=0,P-1,P\right)<N$$
19	18	iffalsed	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)=\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}$$
20	19	mpteq2dv	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(x\in X⟼if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right)=\left(x\in X⟼\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)$$
21		nfv	$$⊢Ⅎx\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)$$
22	11 14	idcncfg	$$⊢\phi \to \left(x\in X⟼x\right):X\underset{cn}{⟶}ℂ$$
23	5	elfzelzd	$$⊢\phi \to J\in \mathbb{Z}$$
24	23	zcnd	$$⊢\phi \to J\in ℂ$$
25	11 24 14	constcncfg	$$⊢\phi \to \left(x\in X⟼J\right):X\underset{cn}{⟶}ℂ$$
26	22 25	subcncf	$$⊢\phi \to \left(x\in X⟼x-J\right):X\underset{cn}{⟶}ℂ$$
27	26	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(x\in X⟼x-J\right):X\underset{cn}{⟶}ℂ$$
28	13	a1i	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to ℂ\subseteq ℂ$$
29		nnm1nn0	$$⊢P\in \mathbb{N}\to P-1\in {\mathbb{N}}_0$$
30	3 29	syl	$$⊢\phi \to P-1\in {\mathbb{N}}_0$$
31	3	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
32	30 31	ifcld	$$⊢\phi \to if\left(J=0,P-1,P\right)\in {\mathbb{N}}_0$$
33	32	faccld	$$⊢\phi \to if\left(J=0,P-1,P\right)!\in \mathbb{N}$$
34	33	nncnd	$$⊢\phi \to if\left(J=0,P-1,P\right)!\in ℂ$$
35	34	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to if\left(J=0,P-1,P\right)!\in ℂ$$
36	32	nn0zd	$$⊢\phi \to if\left(J=0,P-1,P\right)\in \mathbb{Z}$$
37	6	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
38	36 37	zsubcld	$$⊢\phi \to if\left(J=0,P-1,P\right)-N\in \mathbb{Z}$$
39	38	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to if\left(J=0,P-1,P\right)-N\in \mathbb{Z}$$
40	6	nn0red	$$⊢\phi \to N\in ℝ$$
41	40	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to N\in ℝ$$
42	32	nn0red	$$⊢\phi \to if\left(J=0,P-1,P\right)\in ℝ$$
43	42	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to if\left(J=0,P-1,P\right)\in ℝ$$
44	41 43 18	nltled	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to N\le if\left(J=0,P-1,P\right)$$
45	43 41	subge0d	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(0\le if\left(J=0,P-1,P\right)-N\leftrightarrow N\le if\left(J=0,P-1,P\right)\right)$$
46	44 45	mpbird	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to 0\le if\left(J=0,P-1,P\right)-N$$
47		elnn0z	$$⊢if\left(J=0,P-1,P\right)-N\in {\mathbb{N}}_0\leftrightarrow \left(if\left(J=0,P-1,P\right)-N\in \mathbb{Z}\wedge 0\le if\left(J=0,P-1,P\right)-N\right)$$
48	39 46 47	sylanbrc	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to if\left(J=0,P-1,P\right)-N\in {\mathbb{N}}_0$$
49	48	faccld	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(if\left(J=0,P-1,P\right)-N\right)!\in \mathbb{N}$$
50	49	nncnd	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(if\left(J=0,P-1,P\right)-N\right)!\in ℂ$$
51	49	nnne0d	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(if\left(J=0,P-1,P\right)-N\right)!\ne 0$$
52	35 50 51	divcld	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\in ℂ$$
53	28 52 28	constcncfg	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(y\in ℂ⟼\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right):ℂ\underset{cn}{⟶}ℂ$$
54		expcncf	$$⊢if\left(J=0,P-1,P\right)-N\in {\mathbb{N}}_0\to \left(y\in ℂ⟼y^{if\left(J=0,P-1,P\right)-N}\right):ℂ\underset{cn}{⟶}ℂ$$
55	48 54	syl	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(y\in ℂ⟼y^{if\left(J=0,P-1,P\right)-N}\right):ℂ\underset{cn}{⟶}ℂ$$
56	53 55	mulcncf	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(y\in ℂ⟼\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right)y^{if\left(J=0,P-1,P\right)-N}\right):ℂ\underset{cn}{⟶}ℂ$$
57		oveq1	$$⊢y=x-J\to y^{if\left(J=0,P-1,P\right)-N}={\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}$$
58	57	oveq2d	$$⊢y=x-J\to \left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right)y^{if\left(J=0,P-1,P\right)-N}=\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}$$
59	21 27 56 28 58	cncfcompt2	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(x\in X⟼\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right):X\underset{cn}{⟶}ℂ$$
60	20 59	eqeltrd	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \left(x\in X⟼if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right):X\underset{cn}{⟶}ℂ$$
61	17 60	pm2.61dan	$$⊢\phi \to \left(x\in X⟼if\left(if\left(J=0,P-1,P\right)<N,0,\left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right):X\underset{cn}{⟶}ℂ$$
62	7 61	eqeltrd	$$⊢\phi \to \left(S{D}^{n}H\left(J\right)\right)\left(N\right):X\underset{cn}{⟶}ℂ$$