Theorem etransclem17

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

	Ref	Expression
Hypotheses	etransclem17.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	etransclem17.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
	etransclem17.p	$$⊢\phi \to P\in \mathbb{N}$$
	etransclem17.1	$$⊢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)$$
	etransclem17.J	$$⊢\phi \to J\in \left(0\dots M\right)$$
	etransclem17.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		etransclem17.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem17.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem17.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem17.1	$$⊢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		etransclem17.J	$$⊢\phi \to J\in \left(0\dots M\right)$$
6		etransclem17.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7	1 2	dvdmsscn	$$⊢\phi \to X\subseteq ℂ$$
8	7	sselda	$$⊢\left(\phi \wedge x\in X\right)\to x\in ℂ$$
9	8	adantlr	$$⊢\left(\left(\phi \wedge j\in \left(0\dots M\right)\right)\wedge x\in X\right)\to x\in ℂ$$
10		elfzelz	$$⊢j\in \left(0\dots M\right)\to j\in \mathbb{Z}$$
11	10	zcnd	$$⊢j\in \left(0\dots M\right)\to j\in ℂ$$
12	11	ad2antlr	$$⊢\left(\left(\phi \wedge j\in \left(0\dots M\right)\right)\wedge x\in X\right)\to j\in ℂ$$
13	9 12	negsubd	$$⊢\left(\left(\phi \wedge j\in \left(0\dots M\right)\right)\wedge x\in X\right)\to x+\left(-j\right)=x-j$$
14	13	eqcomd	$$⊢\left(\left(\phi \wedge j\in \left(0\dots M\right)\right)\wedge x\in X\right)\to x-j=x+\left(-j\right)$$
15	14	oveq1d	$$⊢\left(\left(\phi \wedge j\in \left(0\dots M\right)\right)\wedge x\in X\right)\to {\left(x-j\right)}^{if\left(j=0,P-1,P\right)}={\left(x+\left(-j\right)\right)}^{if\left(j=0,P-1,P\right)}$$
16	15	mpteq2dva	$$⊢\left(\phi \wedge j\in \left(0\dots M\right)\right)\to \left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)=\left(x\in X⟼{\left(x+\left(-j\right)\right)}^{if\left(j=0,P-1,P\right)}\right)$$
17	16	mpteq2dva	$$⊢\phi \to \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)=\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x+\left(-j\right)\right)}^{if\left(j=0,P-1,P\right)}\right)\right)$$
18	4 17	eqtrid	$$⊢\phi \to H=\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x+\left(-j\right)\right)}^{if\left(j=0,P-1,P\right)}\right)\right)$$
19		negeq	$$⊢j=J\to -j=-J$$
20	19	oveq2d	$$⊢j=J\to x+\left(-j\right)=x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}$$
21		eqeq1	$$⊢j=J\to \left(j=0\leftrightarrow J=0\right)$$
22	21	ifbid	$$⊢j=J\to if\left(j=0,P-1,P\right)=if\left(J=0,P-1,P\right)$$
23	20 22	oveq12d	$$⊢j=J\to {\left(x+\left(-j\right)\right)}^{if\left(j=0,P-1,P\right)}={\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}$$
24	23	mpteq2dv	$$⊢j=J\to \left(x\in X⟼{\left(x+\left(-j\right)\right)}^{if\left(j=0,P-1,P\right)}\right)=\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)$$
25	24	adantl	$$⊢\left(\phi \wedge j=J\right)\to \left(x\in X⟼{\left(x+\left(-j\right)\right)}^{if\left(j=0,P-1,P\right)}\right)=\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)$$
26		mptexg	$$⊢X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\to \left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)\in \mathrm{V}$$
27	2 26	syl	$$⊢\phi \to \left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)\in \mathrm{V}$$
28	18 25 5 27	fvmptd	$$⊢\phi \to H\left(J\right)=\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)$$
29	28	oveq2d	$$⊢\phi \to S{D}^{n}H\left(J\right)=S{D}^n\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)$$
30	29	fveq1d	$$⊢\phi \to \left(S{D}^{n}H\left(J\right)\right)\left(N\right)=\left(S{D}^n\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)\right)\left(N\right)$$
31		elfzelz	$$⊢J\in \left(0\dots M\right)\to J\in \mathbb{Z}$$
32	31	zcnd	$$⊢J\in \left(0\dots M\right)\to J\in ℂ$$
33	5 32	syl	$$⊢\phi \to J\in ℂ$$
34	33	negcld	$$⊢\phi \to -J\in ℂ$$
35		nnm1nn0	$$⊢P\in \mathbb{N}\to P-1\in {\mathbb{N}}_0$$
36	3 35	syl	$$⊢\phi \to P-1\in {\mathbb{N}}_0$$
37	3	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
38	36 37	ifcld	$$⊢\phi \to if\left(J=0,P-1,P\right)\in {\mathbb{N}}_0$$
39		eqid	$$⊢\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)=\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\right)$$
40	1 2 34 38 39	dvnxpaek	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to \left(S{D}^n\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\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+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right)$$
41	6 40	mpdan	$$⊢\phi \to \left(S{D}^n\left(x\in X⟼{\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)}\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+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)-N}\right)\right)$$
42	33	adantr	$$⊢\left(\phi \wedge x\in X\right)\to J\in ℂ$$
43	8 42	negsubd	$$⊢\left(\phi \wedge x\in X\right)\to x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}=x-J$$
44	43	oveq1d	$$⊢\left(\phi \wedge x\in X\right)\to {\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)-N}={\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}$$
45	44	oveq2d	$$⊢\left(\phi \wedge x\in X\right)\to \left(\frac{if\left(J=0,P-1,P\right)!}{\left(if\left(J=0,P-1,P\right)-N\right)!}\right){\left(x+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{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}$$
46	45	ifeq2d	$$⊢\left(\phi \wedge x\in X\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+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)-N}\right)=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)$$
47	46	mpteq2dva	$$⊢\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+\mathrm{-\; <mi\; mathcolor="\#808">J</mi>}\right)}^{if\left(J=0,P-1,P\right)-N}\right)\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)$$
48	30 41 47	3eqtrd	$$⊢\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)$$