# Metamath Proof Explorer

## Theorem etransclem31

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

Ref Expression
Hypotheses etransclem31.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
etransclem31.x ${⊢}{\phi }\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
etransclem31.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem31.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem31.f ${⊢}{F}=\left({x}\in {X}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
etransclem31.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
etransclem31.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)$
etransclem31.c ${⊢}{C}=\left({n}\in {ℕ}_{0}⟼\left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}\right)$
etransclem31.y ${⊢}{\phi }\to {Y}\in {X}$
Assertion etransclem31 ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({Y}\right)=\sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$

### Proof

Step Hyp Ref Expression
1 etransclem31.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 etransclem31.x ${⊢}{\phi }\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
3 etransclem31.p ${⊢}{\phi }\to {P}\in ℕ$
4 etransclem31.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
5 etransclem31.f ${⊢}{F}=\left({x}\in {X}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
6 etransclem31.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
7 etransclem31.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)$
8 etransclem31.c ${⊢}{C}=\left({n}\in {ℕ}_{0}⟼\left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}\right)$
9 etransclem31.y ${⊢}{\phi }\to {Y}\in {X}$
10 1 2 3 4 5 6 7 8 etransclem30 ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)=\left({x}\in {X}⟼\sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({x}\right)\right)$
11 fveq2 ${⊢}{x}={Y}\to \left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({x}\right)=\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)$
12 11 prodeq2ad ${⊢}{x}={Y}\to \prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({x}\right)=\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)$
13 12 oveq2d ${⊢}{x}={Y}\to \left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({x}\right)=\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)$
14 13 sumeq2sdv ${⊢}{x}={Y}\to \sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({x}\right)=\sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)$
15 14 adantl ${⊢}\left({\phi }\wedge {x}={Y}\right)\to \sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({x}\right)=\sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)$
16 8 6 etransclem16 ${⊢}{\phi }\to {C}\left({N}\right)\in \mathrm{Fin}$
17 6 faccld ${⊢}{\phi }\to {N}!\in ℕ$
18 17 nncnd ${⊢}{\phi }\to {N}!\in ℂ$
19 18 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {N}!\in ℂ$
20 fzfid ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \left(0\dots {M}\right)\in \mathrm{Fin}$
21 fzssnn0 ${⊢}\left(0\dots {N}\right)\subseteq {ℕ}_{0}$
22 ssrab2 ${⊢}\left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}\subseteq {\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}$
23 simpr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {c}\in {C}\left({N}\right)$
24 8 6 etransclem12 ${⊢}{\phi }\to {C}\left({N}\right)=\left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}$
25 24 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {C}\left({N}\right)=\left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}$
26 23 25 eleqtrd ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {c}\in \left\{{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}$
27 22 26 sseldi ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)$
28 27 adantr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)$
29 elmapi ${⊢}{c}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)\to {c}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
30 28 29 syl ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
31 simpr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
32 30 31 ffvelrnd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)\in \left(0\dots {N}\right)$
33 21 32 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)\in {ℕ}_{0}$
34 33 faccld ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)!\in ℕ$
35 34 nncnd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)!\in ℂ$
36 20 35 fprodcl ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \prod _{{j}=0}^{{M}}{c}\left({j}\right)!\in ℂ$
37 34 nnne0d ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)!\ne 0$
38 20 35 37 fprodn0 ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \prod _{{j}=0}^{{M}}{c}\left({j}\right)!\ne 0$
39 19 36 38 divcld ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\in ℂ$
40 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {S}\in \left\{ℝ,ℂ\right\}$
41 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
42 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {P}\in ℕ$
43 etransclem5 ${⊢}\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({k}\in \left(0\dots {M}\right)⟼\left({y}\in {X}⟼{\left({y}-{k}\right)}^{if\left({k}=0,{P}-1,{P}\right)}\right)\right)$
44 7 43 eqtri ${⊢}{H}=\left({k}\in \left(0\dots {M}\right)⟼\left({y}\in {X}⟼{\left({y}-{k}\right)}^{if\left({k}=0,{P}-1,{P}\right)}\right)\right)$
45 40 41 42 44 31 33 etransclem20 ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right):{X}⟶ℂ$
46 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {Y}\in {X}$
47 45 46 ffvelrnd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)\in ℂ$
48 20 47 fprodcl ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)\in ℂ$
49 39 48 mulcld ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)\in ℂ$
50 16 49 fsumcl ${⊢}{\phi }\to \sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)\in ℂ$
51 10 15 9 50 fvmptd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({Y}\right)=\sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)$
52 40 41 42 44 31 33 46 etransclem21 ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)=if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)$
53 52 prodeq2dv ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)=\prod _{{j}=0}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)$
54 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
55 4 54 syl6eleq ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
56 55 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {M}\in {ℤ}_{\ge 0}$
57 52 47 eqeltrrd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)\in ℂ$
58 iftrue ${⊢}{j}=0\to if\left({j}=0,{P}-1,{P}\right)={P}-1$
59 fveq2 ${⊢}{j}=0\to {c}\left({j}\right)={c}\left(0\right)$
60 58 59 breq12d ${⊢}{j}=0\to \left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right)↔{P}-1<{c}\left(0\right)\right)$
61 58 fveq2d ${⊢}{j}=0\to if\left({j}=0,{P}-1,{P}\right)!=\left({P}-1\right)!$
62 58 59 oveq12d ${⊢}{j}=0\to if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)={P}-1-{c}\left(0\right)$
63 62 fveq2d ${⊢}{j}=0\to \left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!=\left({P}-1-{c}\left(0\right)\right)!$
64 61 63 oveq12d ${⊢}{j}=0\to \frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}=\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}$
65 oveq2 ${⊢}{j}=0\to {Y}-{j}={Y}-0$
66 65 62 oveq12d ${⊢}{j}=0\to {\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}={\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}$
67 64 66 oveq12d ${⊢}{j}=0\to \left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}=\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}$
68 60 67 ifbieq2d ${⊢}{j}=0\to if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}\right)$
69 56 57 68 fprod1p ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \prod _{{j}=0}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=0+1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)$
70 1 2 dvdmsscn ${⊢}{\phi }\to {X}\subseteq ℂ$
71 70 9 sseldd ${⊢}{\phi }\to {Y}\in ℂ$
72 71 subid1d ${⊢}{\phi }\to {Y}-0={Y}$
73 72 oveq1d ${⊢}{\phi }\to {\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}={{Y}}^{{P}-1-{c}\left(0\right)}$
74 73 oveq2d ${⊢}{\phi }\to \left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}=\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}$
75 74 ifeq2d ${⊢}{\phi }\to if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}\right)=if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)$
76 0p1e1 ${⊢}0+1=1$
77 76 oveq1i ${⊢}\left(0+1\dots {M}\right)=\left(1\dots {M}\right)$
78 77 prodeq1i ${⊢}\prod _{{j}=0+1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=\prod _{{j}=1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)$
79 0red ${⊢}{j}\in \left(1\dots {M}\right)\to 0\in ℝ$
80 1red ${⊢}{j}\in \left(1\dots {M}\right)\to 1\in ℝ$
81 elfzelz ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in ℤ$
82 81 zred ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in ℝ$
83 0lt1 ${⊢}0<1$
84 83 a1i ${⊢}{j}\in \left(1\dots {M}\right)\to 0<1$
85 elfzle1 ${⊢}{j}\in \left(1\dots {M}\right)\to 1\le {j}$
86 79 80 82 84 85 ltletrd ${⊢}{j}\in \left(1\dots {M}\right)\to 0<{j}$
87 86 gt0ne0d ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\ne 0$
88 87 neneqd ${⊢}{j}\in \left(1\dots {M}\right)\to ¬{j}=0$
89 88 iffalsed ${⊢}{j}\in \left(1\dots {M}\right)\to if\left({j}=0,{P}-1,{P}\right)={P}$
90 89 breq1d ${⊢}{j}\in \left(1\dots {M}\right)\to \left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right)↔{P}<{c}\left({j}\right)\right)$
91 89 fveq2d ${⊢}{j}\in \left(1\dots {M}\right)\to if\left({j}=0,{P}-1,{P}\right)!={P}!$
92 89 oveq1d ${⊢}{j}\in \left(1\dots {M}\right)\to if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)={P}-{c}\left({j}\right)$
93 92 fveq2d ${⊢}{j}\in \left(1\dots {M}\right)\to \left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!=\left({P}-{c}\left({j}\right)\right)!$
94 91 93 oveq12d ${⊢}{j}\in \left(1\dots {M}\right)\to \frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}=\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}$
95 92 oveq2d ${⊢}{j}\in \left(1\dots {M}\right)\to {\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}={\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}$
96 94 95 oveq12d ${⊢}{j}\in \left(1\dots {M}\right)\to \left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}=\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}$
97 90 96 ifbieq2d ${⊢}{j}\in \left(1\dots {M}\right)\to if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
98 97 prodeq2i ${⊢}\prod _{{j}=1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
99 78 98 eqtri ${⊢}\prod _{{j}=0+1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
100 99 a1i ${⊢}{\phi }\to \prod _{{j}=0+1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
101 75 100 oveq12d ${⊢}{\phi }\to if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=0+1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
102 101 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){\left({Y}-0\right)}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=0+1}^{{M}}if\left(if\left({j}=0,{P}-1,{P}\right)<{c}\left({j}\right),0,\left(\frac{if\left({j}=0,{P}-1,{P}\right)!}{\left(if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)-{c}\left({j}\right)}\right)=if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
103 53 69 102 3eqtrd ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)=if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
104 103 oveq2d ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to \left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)=\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
105 104 sumeq2dv ${⊢}{\phi }\to \sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\prod _{{j}=0}^{{M}}\left({S}{D}^{n}{H}\left({j}\right)\right)\left({c}\left({j}\right)\right)\left({Y}\right)=\sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
106 51 105 eqtrd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({Y}\right)=\sum _{{c}\in {C}\left({N}\right)}\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)if\left({P}-1<{c}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){{Y}}^{{P}-1-{c}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left({Y}-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$