Theorem etransclem21

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

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

Proof

Step	Hyp	Ref	Expression
1		etransclem21.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem21.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem21.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem21.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		etransclem21.j	$$⊢\phi \to J\in \left(0\dots M\right)$$
6		etransclem21.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		etransclem21.y	$$⊢\phi \to Y\in X$$
8	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)$$
9		oveq1	$$⊢x=Y\to x-J=Y-J$$
10	9	oveq1d	$$⊢x=Y\to {\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}={\left(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}$$
11	10	oveq2d	$$⊢x=Y\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-J\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(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}$$
12	11	ifeq2d	$$⊢x=Y\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)=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(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)$$
13	12	adantl	$$⊢\left(\phi \wedge x=Y\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)=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(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)$$
14		0cnd	$$⊢\left(\phi \wedge if\left(J=0,P-1,P\right)<N\right)\to 0\in ℂ$$
15		nnm1nn0	$$⊢P\in \mathbb{N}\to P-1\in {\mathbb{N}}_0$$
16	3 15	syl	$$⊢\phi \to P-1\in {\mathbb{N}}_0$$
17	3	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
18	16 17	ifcld	$$⊢\phi \to if\left(J=0,P-1,P\right)\in {\mathbb{N}}_0$$
19	18	faccld	$$⊢\phi \to if\left(J=0,P-1,P\right)!\in \mathbb{N}$$
20	19	nncnd	$$⊢\phi \to if\left(J=0,P-1,P\right)!\in ℂ$$
21	20	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 ℂ$$
22	18	nn0zd	$$⊢\phi \to if\left(J=0,P-1,P\right)\in \mathbb{Z}$$
23	6	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
24	22 23	zsubcld	$$⊢\phi \to if\left(J=0,P-1,P\right)-N\in \mathbb{Z}$$
25	24	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}$$
26	6	nn0red	$$⊢\phi \to N\in ℝ$$
27	26	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to N\in ℝ$$
28	18	nn0red	$$⊢\phi \to if\left(J=0,P-1,P\right)\in ℝ$$
29	28	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 ℝ$$
30		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$$
31	27 29 30	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)$$
32	29 27	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)$$
33	31 32	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$$
34		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)$$
35	25 33 34	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$$
36	35	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}$$
37	36	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 ℂ$$
38	36	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$$
39	21 37 38	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 ℂ$$
40	1 2	dvdmsscn	$$⊢\phi \to X\subseteq ℂ$$
41	40 7	sseldd	$$⊢\phi \to Y\in ℂ$$
42	5	elfzelzd	$$⊢\phi \to J\in \mathbb{Z}$$
43	42	zcnd	$$⊢\phi \to J\in ℂ$$
44	41 43	subcld	$$⊢\phi \to Y-J\in ℂ$$
45	44	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to Y-J\in ℂ$$
46	45 35	expcld	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to {\left(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}\in ℂ$$
47	39 46	mulcld	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\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(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}\in ℂ$$
48	14 47	ifclda	$$⊢\phi \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(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\in ℂ$$
49	8 13 7 48	fvmptd	$$⊢\phi \to \left(S{D}^{n}H\left(J\right)\right)\left(N\right)\left(Y\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(Y-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)$$