Theorem etransclem20

Description: H is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		etransclem20.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem20.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem20.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem20.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		etransclem20.J	$$⊢\phi \to J\in \left(0\dots M\right)$$
6		etransclem20.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		iftrue	$$⊢if\left(J=0,P-1,P\right)<N\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$$
8		0cnd	$$⊢if\left(J=0,P-1,P\right)<N\to 0\in ℂ$$
9	7 8	eqeltrd	$$⊢if\left(J=0,P-1,P\right)<N\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)\in ℂ$$
10	9	adantl	$$⊢\left(\left(\phi \wedge x\in X\right)\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)\in ℂ$$
11		simpr	$$⊢\left(\left(\phi \wedge x\in X\right)\wedge \neg if\left(J=0,P-1,P\right)<N\right)\to \neg if\left(J=0,P-1,P\right)<N$$
12	11	iffalsed	$$⊢\left(\left(\phi \wedge x\in X\right)\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}$$
13		nnm1nn0	$$⊢P\in \mathbb{N}\to P-1\in {\mathbb{N}}_0$$
14	3 13	syl	$$⊢\phi \to P-1\in {\mathbb{N}}_0$$
15	3	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
16	14 15	ifcld	$$⊢\phi \to if\left(J=0,P-1,P\right)\in {\mathbb{N}}_0$$
17	16	faccld	$$⊢\phi \to if\left(J=0,P-1,P\right)!\in \mathbb{N}$$
18	17	nncnd	$$⊢\phi \to if\left(J=0,P-1,P\right)!\in ℂ$$
19	18	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 ℂ$$
20	16	nn0zd	$$⊢\phi \to if\left(J=0,P-1,P\right)\in \mathbb{Z}$$
21	6	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
22	20 21	zsubcld	$$⊢\phi \to if\left(J=0,P-1,P\right)-N\in \mathbb{Z}$$
23	22	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}$$
24	6	nn0red	$$⊢\phi \to N\in ℝ$$
25	24	adantr	$$⊢\left(\phi \wedge \neg if\left(J=0,P-1,P\right)<N\right)\to N\in ℝ$$
26	16	nn0red	$$⊢\phi \to if\left(J=0,P-1,P\right)\in ℝ$$
27	26	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 ℝ$$
28		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$$
29	25 27 28	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)$$
30	27 25	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)$$
31	29 30	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$$
32		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)$$
33	23 31 32	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$$
34	33	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}$$
35	34	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 ℂ$$
36	34	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$$
37	19 35 36	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 ℂ$$
38	37	adantlr	$$⊢\left(\left(\phi \wedge x\in X\right)\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 ℂ$$
39	1 2	dvdmsscn	$$⊢\phi \to X\subseteq ℂ$$
40	39	sselda	$$⊢\left(\phi \wedge x\in X\right)\to x\in ℂ$$
41		elfzelz	$$⊢J\in \left(0\dots M\right)\to J\in \mathbb{Z}$$
42	41	zcnd	$$⊢J\in \left(0\dots M\right)\to J\in ℂ$$
43	5 42	syl	$$⊢\phi \to J\in ℂ$$
44	43	adantr	$$⊢\left(\phi \wedge x\in X\right)\to J\in ℂ$$
45	40 44	subcld	$$⊢\left(\phi \wedge x\in X\right)\to x-J\in ℂ$$
46	45	adantr	$$⊢\left(\left(\phi \wedge x\in X\right)\wedge \neg if\left(J=0,P-1,P\right)<N\right)\to x-J\in ℂ$$
47	33	adantlr	$$⊢\left(\left(\phi \wedge x\in X\right)\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$$
48	46 47	expcld	$$⊢\left(\left(\phi \wedge x\in X\right)\wedge \neg if\left(J=0,P-1,P\right)<N\right)\to {\left(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\in ℂ$$
49	38 48	mulcld	$$⊢\left(\left(\phi \wedge x\in X\right)\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(x-J\right)}^{if\left(J=0,P-1,P\right)-N}\in ℂ$$
50	12 49	eqeltrd	$$⊢\left(\left(\phi \wedge x\in X\right)\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)\in ℂ$$
51	10 50	pm2.61dan	$$⊢\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-J\right)}^{if\left(J=0,P-1,P\right)-N}\right)\in ℂ$$
52		eqid	$$⊢\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⟼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)$$
53	51 52	fmptd	$$⊢\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⟶ℂ$$
54	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)$$
55	54	feq1d	$$⊢\phi \to \left(\left(S{D}^{n}H\left(J\right)\right)\left(N\right):X⟶ℂ\leftrightarrow \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⟶ℂ\right)$$
56	53 55	mpbird	$$⊢\phi \to \left(S{D}^{n}H\left(J\right)\right)\left(N\right):X⟶ℂ$$