Theorem etransclem19

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

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

Proof

Step	Hyp	Ref	Expression
1		etransclem19.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem19.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem19.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem19.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		etransclem19.J	$$⊢\phi \to J\in \left(0\dots M\right)$$
6		etransclem19.n	$$⊢\phi \to N\in \mathbb{Z}$$
7		etransclem19.7	$$⊢\phi \to if\left(J=0,P-1,P\right)<N$$
8		0red	$$⊢\phi \to 0\in ℝ$$
9	6	zred	$$⊢\phi \to N\in ℝ$$
10		nnm1nn0	$$⊢P\in \mathbb{N}\to P-1\in {\mathbb{N}}_0$$
11	3 10	syl	$$⊢\phi \to P-1\in {\mathbb{N}}_0$$
12	11	nn0red	$$⊢\phi \to P-1\in ℝ$$
13	3	nnred	$$⊢\phi \to P\in ℝ$$
14	12 13	ifcld	$$⊢\phi \to if\left(J=0,P-1,P\right)\in ℝ$$
15	11	nn0ge0d	$$⊢\phi \to 0\le P-1$$
16	15	adantr	$$⊢\left(\phi \wedge J=0\right)\to 0\le P-1$$
17		iftrue	$$⊢J=0\to if\left(J=0,P-1,P\right)=P-1$$
18	17	eqcomd	$$⊢J=0\to P-1=if\left(J=0,P-1,P\right)$$
19	18	adantl	$$⊢\left(\phi \wedge J=0\right)\to P-1=if\left(J=0,P-1,P\right)$$
20	16 19	breqtrd	$$⊢\left(\phi \wedge J=0\right)\to 0\le if\left(J=0,P-1,P\right)$$
21	3	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
22	21	nn0ge0d	$$⊢\phi \to 0\le P$$
23	22	adantr	$$⊢\left(\phi \wedge \neg J=0\right)\to 0\le P$$
24		iffalse	$$⊢\neg J=0\to if\left(J=0,P-1,P\right)=P$$
25	24	eqcomd	$$⊢\neg J=0\to P=if\left(J=0,P-1,P\right)$$
26	25	adantl	$$⊢\left(\phi \wedge \neg J=0\right)\to P=if\left(J=0,P-1,P\right)$$
27	23 26	breqtrd	$$⊢\left(\phi \wedge \neg J=0\right)\to 0\le if\left(J=0,P-1,P\right)$$
28	20 27	pm2.61dan	$$⊢\phi \to 0\le if\left(J=0,P-1,P\right)$$
29	8 14 9 28 7	lelttrd	$$⊢\phi \to 0<N$$
30	8 9 29	ltled	$$⊢\phi \to 0\le N$$
31		elnn0z	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{Z}\wedge 0\le N\right)$$
32	6 30 31	sylanbrc	$$⊢\phi \to N\in {\mathbb{N}}_0$$
33	1 2 3 4 5 32	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)$$
34	7	iftrued	$$⊢\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(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)=0$$
35	34	mpteq2dv	$$⊢\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)=\left(x\in X⟼0\right)$$
36	33 35	eqtrd	$$⊢\phi \to \left(S{D}^{n}H\left(J\right)\right)\left(N\right)=\left(x\in X⟼0\right)$$