# Metamath Proof Explorer

## Theorem etransclem35

Description: P does not divide the P-1 -th derivative of F applied to 0 . This is case 2 of the proof in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem35.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem35.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem35.f ${⊢}{F}=\left({x}\in ℝ⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
etransclem35.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)$
etransclem35.d ${⊢}{D}=\left({j}\in \left(0\dots {M}\right)⟼if\left({j}=0,{P}-1,0\right)\right)$
Assertion etransclem35 ${⊢}{\phi }\to \left(ℝ{D}^{n}{F}\right)\left({P}-1\right)\left(0\right)=\left({P}-1\right)!{\prod _{{j}=1}^{{M}}\left(-{j}\right)}^{{P}}$

### Proof

Step Hyp Ref Expression
1 etransclem35.p ${⊢}{\phi }\to {P}\in ℕ$
2 etransclem35.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
3 etransclem35.f ${⊢}{F}=\left({x}\in ℝ⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
4 etransclem35.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)$
5 etransclem35.d ${⊢}{D}=\left({j}\in \left(0\dots {M}\right)⟼if\left({j}=0,{P}-1,0\right)\right)$
6 reelprrecn ${⊢}ℝ\in \left\{ℝ,ℂ\right\}$
7 6 a1i ${⊢}{\phi }\to ℝ\in \left\{ℝ,ℂ\right\}$
8 reopn ${⊢}ℝ\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
9 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
10 9 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
11 8 10 eleqtri ${⊢}ℝ\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
12 11 a1i ${⊢}{\phi }\to ℝ\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
13 nnm1nn0 ${⊢}{P}\in ℕ\to {P}-1\in {ℕ}_{0}$
14 1 13 syl ${⊢}{\phi }\to {P}-1\in {ℕ}_{0}$
15 etransclem5 ${⊢}\left({k}\in \left(0\dots {M}\right)⟼\left({y}\in ℝ⟼{\left({y}-{k}\right)}^{if\left({k}=0,{P}-1,{P}\right)}\right)\right)=\left({j}\in \left(0\dots {M}\right)⟼\left({x}\in ℝ⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\right)$
16 0red ${⊢}{\phi }\to 0\in ℝ$
17 7 12 1 2 3 14 15 4 16 etransclem31 ${⊢}{\phi }\to \left(ℝ{D}^{n}{F}\right)\left({P}-1\right)\left(0\right)=\sum _{{c}\in {C}\left({P}-1\right)}\left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
18 nfv ${⊢}Ⅎ{c}\phantom{\rule{.4em}{0ex}}{\phi }$
19 nfcv ${⊢}\underset{_}{Ⅎ}{c}\phantom{\rule{.4em}{0ex}}\left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\right)if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)$
20 4 14 etransclem16 ${⊢}{\phi }\to {C}\left({P}-1\right)\in \mathrm{Fin}$
21 simpr ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {c}\in {C}\left({P}-1\right)$
22 4 14 etransclem12 ${⊢}{\phi }\to {C}\left({P}-1\right)=\left\{{c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right\}$
23 22 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {C}\left({P}-1\right)=\left\{{c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right\}$
24 21 23 eleqtrd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {c}\in \left\{{c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right\}$
25 rabid ${⊢}{c}\in \left\{{c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right\}↔\left({c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)\wedge \sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right)$
26 24 25 sylib ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \left({c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)\wedge \sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right)$
27 26 simprd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1$
28 27 eqcomd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {P}-1=\sum _{{j}=0}^{{M}}{c}\left({j}\right)$
29 28 fveq2d ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \left({P}-1\right)!=\sum _{{j}=0}^{{M}}{c}\left({j}\right)!$
30 29 oveq1d ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}=\frac{\sum _{{j}=0}^{{M}}{c}\left({j}\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}$
31 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{c}$
32 fzfid ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \left(0\dots {M}\right)\in \mathrm{Fin}$
33 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
34 fzssnn0 ${⊢}\left(0\dots {P}-1\right)\subseteq {ℕ}_{0}$
35 mapss ${⊢}\left({ℕ}_{0}\in \mathrm{V}\wedge \left(0\dots {P}-1\right)\subseteq {ℕ}_{0}\right)\to {\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\subseteq {{ℕ}_{0}}^{\left(0\dots {M}\right)}$
36 33 34 35 mp2an ${⊢}{\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\subseteq {{ℕ}_{0}}^{\left(0\dots {M}\right)}$
37 26 simpld ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)$
38 36 37 sseldi ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {c}\in \left({{ℕ}_{0}}^{\left(0\dots {M}\right)}\right)$
39 31 32 38 mccl ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \frac{\sum _{{j}=0}^{{M}}{c}\left({j}\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\in ℕ$
40 30 39 eqeltrd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\in ℕ$
41 40 nnzd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\in ℤ$
42 1 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {P}\in ℕ$
43 2 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {M}\in {ℕ}_{0}$
44 elmapi ${⊢}{c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)\to {c}:\left(0\dots {M}\right)⟶\left(0\dots {P}-1\right)$
45 37 44 syl ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {c}:\left(0\dots {M}\right)⟶\left(0\dots {P}-1\right)$
46 0zd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to 0\in ℤ$
47 42 43 45 46 etransclem10 ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\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){0}^{{P}-1-{c}\left(0\right)}\right)\in ℤ$
48 fzfid ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \left(1\dots {M}\right)\in \mathrm{Fin}$
49 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}\in ℕ$
50 45 adantr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {c}:\left(0\dots {M}\right)⟶\left(0\dots {P}-1\right)$
51 fz1ssfz0 ${⊢}\left(1\dots {M}\right)\subseteq \left(0\dots {M}\right)$
52 51 sseli ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in \left(0\dots {M}\right)$
53 52 adantl ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
54 0zd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to 0\in ℤ$
55 49 50 53 54 etransclem3 ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)\in ℤ$
56 48 55 fprodzcl ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)\in ℤ$
57 47 56 zmulcld ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)\in ℤ$
58 41 57 zmulcld ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)\in ℤ$
59 58 zcnd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)\in ℂ$
60 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
61 14 60 eleqtrdi ${⊢}{\phi }\to {P}-1\in {ℤ}_{\ge 0}$
62 eluzfz2 ${⊢}{P}-1\in {ℤ}_{\ge 0}\to {P}-1\in \left(0\dots {P}-1\right)$
63 61 62 syl ${⊢}{\phi }\to {P}-1\in \left(0\dots {P}-1\right)$
64 eluzfz1 ${⊢}{P}-1\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {P}-1\right)$
65 61 64 syl ${⊢}{\phi }\to 0\in \left(0\dots {P}-1\right)$
66 63 65 ifcld ${⊢}{\phi }\to if\left({j}=0,{P}-1,0\right)\in \left(0\dots {P}-1\right)$
67 66 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to if\left({j}=0,{P}-1,0\right)\in \left(0\dots {P}-1\right)$
68 67 5 fmptd ${⊢}{\phi }\to {D}:\left(0\dots {M}\right)⟶\left(0\dots {P}-1\right)$
69 ovex ${⊢}\left(0\dots {P}-1\right)\in \mathrm{V}$
70 ovex ${⊢}\left(0\dots {M}\right)\in \mathrm{V}$
71 69 70 elmap ${⊢}{D}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)↔{D}:\left(0\dots {M}\right)⟶\left(0\dots {P}-1\right)$
72 68 71 sylibr ${⊢}{\phi }\to {D}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)$
73 2 60 eleqtrdi ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
74 fzsscn ${⊢}\left(0\dots {P}-1\right)\subseteq ℂ$
75 68 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {D}\left({j}\right)\in \left(0\dots {P}-1\right)$
76 74 75 sseldi ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {D}\left({j}\right)\in ℂ$
77 fveq2 ${⊢}{j}=0\to {D}\left({j}\right)={D}\left(0\right)$
78 73 76 77 fsum1p ${⊢}{\phi }\to \sum _{{j}=0}^{{M}}{D}\left({j}\right)={D}\left(0\right)+\sum _{{j}=0+1}^{{M}}{D}\left({j}\right)$
79 5 a1i ${⊢}{\phi }\to {D}=\left({j}\in \left(0\dots {M}\right)⟼if\left({j}=0,{P}-1,0\right)\right)$
80 simpr ${⊢}\left({\phi }\wedge {j}=0\right)\to {j}=0$
81 80 iftrued ${⊢}\left({\phi }\wedge {j}=0\right)\to if\left({j}=0,{P}-1,0\right)={P}-1$
82 eluzfz1 ${⊢}{M}\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {M}\right)$
83 73 82 syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
84 79 81 83 14 fvmptd ${⊢}{\phi }\to {D}\left(0\right)={P}-1$
85 0p1e1 ${⊢}0+1=1$
86 85 oveq1i ${⊢}\left(0+1\dots {M}\right)=\left(1\dots {M}\right)$
87 86 sumeq1i ${⊢}\sum _{{j}=0+1}^{{M}}{D}\left({j}\right)=\sum _{{j}=1}^{{M}}{D}\left({j}\right)$
88 87 a1i ${⊢}{\phi }\to \sum _{{j}=0+1}^{{M}}{D}\left({j}\right)=\sum _{{j}=1}^{{M}}{D}\left({j}\right)$
89 5 fvmpt2 ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge if\left({j}=0,{P}-1,0\right)\in \left(0\dots {P}-1\right)\right)\to {D}\left({j}\right)=if\left({j}=0,{P}-1,0\right)$
90 52 66 89 syl2anr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}\left({j}\right)=if\left({j}=0,{P}-1,0\right)$
91 0red ${⊢}{j}\in \left(1\dots {M}\right)\to 0\in ℝ$
92 1red ${⊢}{j}\in \left(1\dots {M}\right)\to 1\in ℝ$
93 elfzelz ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in ℤ$
94 93 zred ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in ℝ$
95 0lt1 ${⊢}0<1$
96 95 a1i ${⊢}{j}\in \left(1\dots {M}\right)\to 0<1$
97 elfzle1 ${⊢}{j}\in \left(1\dots {M}\right)\to 1\le {j}$
98 91 92 94 96 97 ltletrd ${⊢}{j}\in \left(1\dots {M}\right)\to 0<{j}$
99 91 98 gtned ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\ne 0$
100 99 neneqd ${⊢}{j}\in \left(1\dots {M}\right)\to ¬{j}=0$
101 100 iffalsed ${⊢}{j}\in \left(1\dots {M}\right)\to if\left({j}=0,{P}-1,0\right)=0$
102 101 adantl ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to if\left({j}=0,{P}-1,0\right)=0$
103 90 102 eqtrd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}\left({j}\right)=0$
104 103 sumeq2dv ${⊢}{\phi }\to \sum _{{j}=1}^{{M}}{D}\left({j}\right)=\sum _{{j}=1}^{{M}}0$
105 fzfi ${⊢}\left(1\dots {M}\right)\in \mathrm{Fin}$
106 105 olci ${⊢}\left(\left(1\dots {M}\right)\subseteq {ℤ}_{\ge {A}}\vee \left(1\dots {M}\right)\in \mathrm{Fin}\right)$
107 sumz ${⊢}\left(\left(1\dots {M}\right)\subseteq {ℤ}_{\ge {A}}\vee \left(1\dots {M}\right)\in \mathrm{Fin}\right)\to \sum _{{j}=1}^{{M}}0=0$
108 106 107 mp1i ${⊢}{\phi }\to \sum _{{j}=1}^{{M}}0=0$
109 88 104 108 3eqtrd ${⊢}{\phi }\to \sum _{{j}=0+1}^{{M}}{D}\left({j}\right)=0$
110 84 109 oveq12d ${⊢}{\phi }\to {D}\left(0\right)+\sum _{{j}=0+1}^{{M}}{D}\left({j}\right)={P}-1+0$
111 1 nncnd ${⊢}{\phi }\to {P}\in ℂ$
112 1cnd ${⊢}{\phi }\to 1\in ℂ$
113 111 112 subcld ${⊢}{\phi }\to {P}-1\in ℂ$
114 113 addid1d ${⊢}{\phi }\to {P}-1+0={P}-1$
115 78 110 114 3eqtrd ${⊢}{\phi }\to \sum _{{j}=0}^{{M}}{D}\left({j}\right)={P}-1$
116 fveq1 ${⊢}{c}={D}\to {c}\left({j}\right)={D}\left({j}\right)$
117 116 sumeq2sdv ${⊢}{c}={D}\to \sum _{{j}=0}^{{M}}{c}\left({j}\right)=\sum _{{j}=0}^{{M}}{D}\left({j}\right)$
118 117 eqeq1d ${⊢}{c}={D}\to \left(\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1↔\sum _{{j}=0}^{{M}}{D}\left({j}\right)={P}-1\right)$
119 118 elrab ${⊢}{D}\in \left\{{c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right\}↔\left({D}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)\wedge \sum _{{j}=0}^{{M}}{D}\left({j}\right)={P}-1\right)$
120 72 115 119 sylanbrc ${⊢}{\phi }\to {D}\in \left\{{c}\in \left({\left(0\dots {P}-1\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1\right\}$
121 120 22 eleqtrrd ${⊢}{\phi }\to {D}\in {C}\left({P}-1\right)$
122 116 fveq2d ${⊢}{c}={D}\to {c}\left({j}\right)!={D}\left({j}\right)!$
123 122 prodeq2ad ${⊢}{c}={D}\to \prod _{{j}=0}^{{M}}{c}\left({j}\right)!=\prod _{{j}=0}^{{M}}{D}\left({j}\right)!$
124 123 oveq2d ${⊢}{c}={D}\to \frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}=\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}$
125 fveq1 ${⊢}{c}={D}\to {c}\left(0\right)={D}\left(0\right)$
126 125 breq2d ${⊢}{c}={D}\to \left({P}-1<{c}\left(0\right)↔{P}-1<{D}\left(0\right)\right)$
127 125 oveq2d ${⊢}{c}={D}\to {P}-1-{c}\left(0\right)={P}-1-{D}\left(0\right)$
128 127 fveq2d ${⊢}{c}={D}\to \left({P}-1-{c}\left(0\right)\right)!=\left({P}-1-{D}\left(0\right)\right)!$
129 128 oveq2d ${⊢}{c}={D}\to \frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}=\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}$
130 127 oveq2d ${⊢}{c}={D}\to {0}^{{P}-1-{c}\left(0\right)}={0}^{{P}-1-{D}\left(0\right)}$
131 129 130 oveq12d ${⊢}{c}={D}\to \left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){0}^{{P}-1-{c}\left(0\right)}=\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}$
132 126 131 ifbieq2d ${⊢}{c}={D}\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){0}^{{P}-1-{c}\left(0\right)}\right)=if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)$
133 116 breq2d ${⊢}{c}={D}\to \left({P}<{c}\left({j}\right)↔{P}<{D}\left({j}\right)\right)$
134 116 oveq2d ${⊢}{c}={D}\to {P}-{c}\left({j}\right)={P}-{D}\left({j}\right)$
135 134 fveq2d ${⊢}{c}={D}\to \left({P}-{c}\left({j}\right)\right)!=\left({P}-{D}\left({j}\right)\right)!$
136 135 oveq2d ${⊢}{c}={D}\to \frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}=\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}$
137 134 oveq2d ${⊢}{c}={D}\to {\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}={\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}$
138 136 137 oveq12d ${⊢}{c}={D}\to \left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}=\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}$
139 133 138 ifbieq2d ${⊢}{c}={D}\to if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)$
140 139 prodeq2ad ${⊢}{c}={D}\to \prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)$
141 132 140 oveq12d ${⊢}{c}={D}\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)$
142 124 141 oveq12d ${⊢}{c}={D}\to \left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=\left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\right)if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)$
143 18 19 20 59 121 142 fsumsplit1 ${⊢}{\phi }\to \sum _{{c}\in {C}\left({P}-1\right)}\left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=\left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\right)if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)+\sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}\left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
144 34 75 sseldi ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {D}\left({j}\right)\in {ℕ}_{0}$
145 144 faccld ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {D}\left({j}\right)!\in ℕ$
146 145 nncnd ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {D}\left({j}\right)!\in ℂ$
147 77 fveq2d ${⊢}{j}=0\to {D}\left({j}\right)!={D}\left(0\right)!$
148 73 146 147 fprod1p ${⊢}{\phi }\to \prod _{{j}=0}^{{M}}{D}\left({j}\right)!={D}\left(0\right)!\prod _{{j}=0+1}^{{M}}{D}\left({j}\right)!$
149 84 fveq2d ${⊢}{\phi }\to {D}\left(0\right)!=\left({P}-1\right)!$
150 86 prodeq1i ${⊢}\prod _{{j}=0+1}^{{M}}{D}\left({j}\right)!=\prod _{{j}=1}^{{M}}{D}\left({j}\right)!$
151 150 a1i ${⊢}{\phi }\to \prod _{{j}=0+1}^{{M}}{D}\left({j}\right)!=\prod _{{j}=1}^{{M}}{D}\left({j}\right)!$
152 103 fveq2d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}\left({j}\right)!=0!$
153 fac0 ${⊢}0!=1$
154 152 153 syl6eq ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}\left({j}\right)!=1$
155 154 prodeq2dv ${⊢}{\phi }\to \prod _{{j}=1}^{{M}}{D}\left({j}\right)!=\prod _{{j}=1}^{{M}}1$
156 prod1 ${⊢}\left(\left(1\dots {M}\right)\subseteq {ℤ}_{\ge {A}}\vee \left(1\dots {M}\right)\in \mathrm{Fin}\right)\to \prod _{{j}=1}^{{M}}1=1$
157 106 156 mp1i ${⊢}{\phi }\to \prod _{{j}=1}^{{M}}1=1$
158 151 155 157 3eqtrd ${⊢}{\phi }\to \prod _{{j}=0+1}^{{M}}{D}\left({j}\right)!=1$
159 149 158 oveq12d ${⊢}{\phi }\to {D}\left(0\right)!\prod _{{j}=0+1}^{{M}}{D}\left({j}\right)!=\left({P}-1\right)!\cdot 1$
160 14 faccld ${⊢}{\phi }\to \left({P}-1\right)!\in ℕ$
161 160 nncnd ${⊢}{\phi }\to \left({P}-1\right)!\in ℂ$
162 161 mulid1d ${⊢}{\phi }\to \left({P}-1\right)!\cdot 1=\left({P}-1\right)!$
163 148 159 162 3eqtrd ${⊢}{\phi }\to \prod _{{j}=0}^{{M}}{D}\left({j}\right)!=\left({P}-1\right)!$
164 163 oveq2d ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}=\frac{\left({P}-1\right)!}{\left({P}-1\right)!}$
165 160 nnne0d ${⊢}{\phi }\to \left({P}-1\right)!\ne 0$
166 161 165 dividd ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{\left({P}-1\right)!}=1$
167 164 166 eqtrd ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}=1$
168 14 nn0red ${⊢}{\phi }\to {P}-1\in ℝ$
169 84 168 eqeltrd ${⊢}{\phi }\to {D}\left(0\right)\in ℝ$
170 169 168 lttri3d ${⊢}{\phi }\to \left({D}\left(0\right)={P}-1↔\left(¬{D}\left(0\right)<{P}-1\wedge ¬{P}-1<{D}\left(0\right)\right)\right)$
171 84 170 mpbid ${⊢}{\phi }\to \left(¬{D}\left(0\right)<{P}-1\wedge ¬{P}-1<{D}\left(0\right)\right)$
172 171 simprd ${⊢}{\phi }\to ¬{P}-1<{D}\left(0\right)$
173 172 iffalsed ${⊢}{\phi }\to if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)=\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}$
174 84 eqcomd ${⊢}{\phi }\to {P}-1={D}\left(0\right)$
175 113 174 subeq0bd ${⊢}{\phi }\to {P}-1-{D}\left(0\right)=0$
176 175 fveq2d ${⊢}{\phi }\to \left({P}-1-{D}\left(0\right)\right)!=0!$
177 176 153 syl6eq ${⊢}{\phi }\to \left({P}-1-{D}\left(0\right)\right)!=1$
178 177 oveq2d ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}=\frac{\left({P}-1\right)!}{1}$
179 161 div1d ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{1}=\left({P}-1\right)!$
180 178 179 eqtrd ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}=\left({P}-1\right)!$
181 175 oveq2d ${⊢}{\phi }\to {0}^{{P}-1-{D}\left(0\right)}={0}^{0}$
182 0cnd ${⊢}{\phi }\to 0\in ℂ$
183 182 exp0d ${⊢}{\phi }\to {0}^{0}=1$
184 181 183 eqtrd ${⊢}{\phi }\to {0}^{{P}-1-{D}\left(0\right)}=1$
185 180 184 oveq12d ${⊢}{\phi }\to \left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}=\left({P}-1\right)!\cdot 1$
186 173 185 162 3eqtrd ${⊢}{\phi }\to if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)=\left({P}-1\right)!$
187 fzssre ${⊢}\left(0\dots {P}-1\right)\subseteq ℝ$
188 68 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}:\left(0\dots {M}\right)⟶\left(0\dots {P}-1\right)$
189 52 adantl ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
190 188 189 ffvelrnd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}\left({j}\right)\in \left(0\dots {P}-1\right)$
191 187 190 sseldi ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}\left({j}\right)\in ℝ$
192 1 nnred ${⊢}{\phi }\to {P}\in ℝ$
193 192 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}\in ℝ$
194 1 nngt0d ${⊢}{\phi }\to 0<{P}$
195 16 192 194 ltled ${⊢}{\phi }\to 0\le {P}$
196 195 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to 0\le {P}$
197 103 196 eqbrtrd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}\left({j}\right)\le {P}$
198 191 193 197 lensymd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to ¬{P}<{D}\left({j}\right)$
199 198 iffalsed ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)=\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}$
200 103 oveq2d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}-{D}\left({j}\right)={P}-0$
201 111 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}\in ℂ$
202 201 subid1d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}-0={P}$
203 200 202 eqtrd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}-{D}\left({j}\right)={P}$
204 203 fveq2d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \left({P}-{D}\left({j}\right)\right)!={P}!$
205 204 oveq2d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}=\frac{{P}!}{{P}!}$
206 1 nnnn0d ${⊢}{\phi }\to {P}\in {ℕ}_{0}$
207 206 faccld ${⊢}{\phi }\to {P}!\in ℕ$
208 207 nncnd ${⊢}{\phi }\to {P}!\in ℂ$
209 207 nnne0d ${⊢}{\phi }\to {P}!\ne 0$
210 208 209 dividd ${⊢}{\phi }\to \frac{{P}!}{{P}!}=1$
211 210 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \frac{{P}!}{{P}!}=1$
212 205 211 eqtrd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}=1$
213 df-neg ${⊢}-{j}=0-{j}$
214 213 eqcomi ${⊢}0-{j}=-{j}$
215 214 a1i ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to 0-{j}=-{j}$
216 215 203 oveq12d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}={\left(-{j}\right)}^{{P}}$
217 212 216 oveq12d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}=1{\left(-{j}\right)}^{{P}}$
218 93 znegcld ${⊢}{j}\in \left(1\dots {M}\right)\to -{j}\in ℤ$
219 218 zcnd ${⊢}{j}\in \left(1\dots {M}\right)\to -{j}\in ℂ$
220 219 adantl ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to -{j}\in ℂ$
221 206 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}\in {ℕ}_{0}$
222 220 221 expcld ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {\left(-{j}\right)}^{{P}}\in ℂ$
223 222 mulid2d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to 1{\left(-{j}\right)}^{{P}}={\left(-{j}\right)}^{{P}}$
224 199 217 223 3eqtrd ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)={\left(-{j}\right)}^{{P}}$
225 224 prodeq2dv ${⊢}{\phi }\to \prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)=\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}$
226 186 225 oveq12d ${⊢}{\phi }\to if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)=\left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}$
227 167 226 oveq12d ${⊢}{\phi }\to \left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\right)if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)=1\left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}$
228 fzfid ${⊢}{\phi }\to \left(1\dots {M}\right)\in \mathrm{Fin}$
229 zexpcl ${⊢}\left(-{j}\in ℤ\wedge {P}\in {ℕ}_{0}\right)\to {\left(-{j}\right)}^{{P}}\in ℤ$
230 218 206 229 syl2anr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {\left(-{j}\right)}^{{P}}\in ℤ$
231 228 230 fprodzcl ${⊢}{\phi }\to \prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}\in ℤ$
232 231 zcnd ${⊢}{\phi }\to \prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}\in ℂ$
233 161 232 mulcld ${⊢}{\phi }\to \left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}\in ℂ$
234 233 mulid2d ${⊢}{\phi }\to 1\left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}=\left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}$
235 227 234 eqtrd ${⊢}{\phi }\to \left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\right)if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)=\left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}$
236 eldifi ${⊢}{c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\to {c}\in {C}\left({P}-1\right)$
237 83 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to 0\in \left(0\dots {M}\right)$
238 45 237 ffvelrnd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {c}\left(0\right)\in \left(0\dots {P}-1\right)$
239 236 238 sylan2 ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {c}\left(0\right)\in \left(0\dots {P}-1\right)$
240 187 239 sseldi ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {c}\left(0\right)\in ℝ$
241 168 adantr ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {P}-1\in ℝ$
242 elfzle2 ${⊢}{c}\left(0\right)\in \left(0\dots {P}-1\right)\to {c}\left(0\right)\le {P}-1$
243 239 242 syl ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {c}\left(0\right)\le {P}-1$
244 240 241 243 lensymd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to ¬{P}-1<{c}\left(0\right)$
245 244 iffalsed ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\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){0}^{{P}-1-{c}\left(0\right)}\right)=\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){0}^{{P}-1-{c}\left(0\right)}$
246 14 nn0zd ${⊢}{\phi }\to {P}-1\in ℤ$
247 246 adantr ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {P}-1\in ℤ$
248 239 elfzelzd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {c}\left(0\right)\in ℤ$
249 247 248 zsubcld ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {P}-1-{c}\left(0\right)\in ℤ$
250 45 ffnd ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to {c}Fn\left(0\dots {M}\right)$
251 250 adantr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\to {c}Fn\left(0\dots {M}\right)$
252 68 ffnd ${⊢}{\phi }\to {D}Fn\left(0\dots {M}\right)$
253 252 ad2antrr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\to {D}Fn\left(0\dots {M}\right)$
254 fveq2 ${⊢}{j}=0\to {c}\left({j}\right)={c}\left(0\right)$
255 254 adantl ${⊢}\left(\left({\phi }\wedge {P}-1={c}\left(0\right)\right)\wedge {j}=0\right)\to {c}\left({j}\right)={c}\left(0\right)$
256 id ${⊢}{P}-1={c}\left(0\right)\to {P}-1={c}\left(0\right)$
257 256 eqcomd ${⊢}{P}-1={c}\left(0\right)\to {c}\left(0\right)={P}-1$
258 257 ad2antlr ${⊢}\left(\left({\phi }\wedge {P}-1={c}\left(0\right)\right)\wedge {j}=0\right)\to {c}\left(0\right)={P}-1$
259 77 adantl ${⊢}\left({\phi }\wedge {j}=0\right)\to {D}\left({j}\right)={D}\left(0\right)$
260 84 adantr ${⊢}\left({\phi }\wedge {j}=0\right)\to {D}\left(0\right)={P}-1$
261 259 260 eqtr2d ${⊢}\left({\phi }\wedge {j}=0\right)\to {P}-1={D}\left({j}\right)$
262 261 adantlr ${⊢}\left(\left({\phi }\wedge {P}-1={c}\left(0\right)\right)\wedge {j}=0\right)\to {P}-1={D}\left({j}\right)$
263 255 258 262 3eqtrd ${⊢}\left(\left({\phi }\wedge {P}-1={c}\left(0\right)\right)\wedge {j}=0\right)\to {c}\left({j}\right)={D}\left({j}\right)$
264 263 adantllr ${⊢}\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}=0\right)\to {c}\left({j}\right)={D}\left({j}\right)$
265 264 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {j}=0\right)\to {c}\left({j}\right)={D}\left({j}\right)$
266 27 ad4antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1$
267 168 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {P}-1\in ℝ$
268 168 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {P}-1\in ℝ$
269 45 adantr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to {c}:\left(0\dots {M}\right)⟶\left(0\dots {P}-1\right)$
270 51 sseli ${⊢}{k}\in \left(1\dots {M}\right)\to {k}\in \left(0\dots {M}\right)$
271 270 adantl ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to {k}\in \left(0\dots {M}\right)$
272 269 271 ffvelrnd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to {c}\left({k}\right)\in \left(0\dots {P}-1\right)$
273 34 272 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to {c}\left({k}\right)\in {ℕ}_{0}$
274 48 273 fsumnn0cl ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \sum _{{k}=1}^{{M}}{c}\left({k}\right)\in {ℕ}_{0}$
275 274 nn0red ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \sum _{{k}=1}^{{M}}{c}\left({k}\right)\in ℝ$
276 275 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{k}=1}^{{M}}{c}\left({k}\right)\in ℝ$
277 0red ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to 0\in ℝ$
278 45 ffvelrnda ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)\in \left(0\dots {P}-1\right)$
279 187 278 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)\in ℝ$
280 279 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {c}\left({j}\right)\in ℝ$
281 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)$
282 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{c}\left({j}\right)$
283 fzfid ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \left(1\dots {M}\right)\in \mathrm{Fin}$
284 simp-4l ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to \left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)$
285 74 272 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to {c}\left({k}\right)\in ℂ$
286 284 285 sylancom ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to {c}\left({k}\right)\in ℂ$
287 1zzd ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to 1\in ℤ$
288 elfzel2 ${⊢}{j}\in \left(0\dots {M}\right)\to {M}\in ℤ$
289 288 adantr ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to {M}\in ℤ$
290 elfzelz ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in ℤ$
291 290 adantr ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to {j}\in ℤ$
292 287 289 291 3jca ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to \left(1\in ℤ\wedge {M}\in ℤ\wedge {j}\in ℤ\right)$
293 elfznn0 ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in {ℕ}_{0}$
294 293 adantr ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to {j}\in {ℕ}_{0}$
295 neqne ${⊢}¬{j}=0\to {j}\ne 0$
296 295 adantl ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to {j}\ne 0$
297 elnnne0 ${⊢}{j}\in ℕ↔\left({j}\in {ℕ}_{0}\wedge {j}\ne 0\right)$
298 294 296 297 sylanbrc ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to {j}\in ℕ$
299 298 nnge1d ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to 1\le {j}$
300 elfzle2 ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\le {M}$
301 300 adantr ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to {j}\le {M}$
302 292 299 301 jca32 ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to \left(\left(1\in ℤ\wedge {M}\in ℤ\wedge {j}\in ℤ\right)\wedge \left(1\le {j}\wedge {j}\le {M}\right)\right)$
303 elfz2 ${⊢}{j}\in \left(1\dots {M}\right)↔\left(\left(1\in ℤ\wedge {M}\in ℤ\wedge {j}\in ℤ\right)\wedge \left(1\le {j}\wedge {j}\le {M}\right)\right)$
304 302 303 sylibr ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\to {j}\in \left(1\dots {M}\right)$
305 304 adantr ${⊢}\left(\left({j}\in \left(0\dots {M}\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {j}\in \left(1\dots {M}\right)$
306 305 adantlll ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {j}\in \left(1\dots {M}\right)$
307 fveq2 ${⊢}{k}={j}\to {c}\left({k}\right)={c}\left({j}\right)$
308 281 282 283 286 306 307 fsumsplit1 ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{k}=1}^{{M}}{c}\left({k}\right)={c}\left({j}\right)+\sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)$
309 308 eqcomd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {c}\left({j}\right)+\sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)=\sum _{{k}=1}^{{M}}{c}\left({k}\right)$
310 309 276 eqeltrd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {c}\left({j}\right)+\sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)\in ℝ$
311 elfzle1 ${⊢}{c}\left({j}\right)\in \left(0\dots {P}-1\right)\to 0\le {c}\left({j}\right)$
312 278 311 syl ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to 0\le {c}\left({j}\right)$
313 312 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to 0\le {c}\left({j}\right)$
314 neqne ${⊢}¬{c}\left({j}\right)=0\to {c}\left({j}\right)\ne 0$
315 314 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {c}\left({j}\right)\ne 0$
316 277 280 313 315 leneltd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to 0<{c}\left({j}\right)$
317 diffi ${⊢}\left(1\dots {M}\right)\in \mathrm{Fin}\to \left(1\dots {M}\right)\setminus \left\{{j}\right\}\in \mathrm{Fin}$
318 105 317 mp1i ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \left(1\dots {M}\right)\setminus \left\{{j}\right\}\in \mathrm{Fin}$
319 eldifi ${⊢}{k}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\to {k}\in \left(1\dots {M}\right)$
320 319 adantl ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to {k}\in \left(1\dots {M}\right)$
321 51 320 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to {k}\in \left(0\dots {M}\right)$
322 45 ffvelrnda ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(0\dots {M}\right)\right)\to {c}\left({k}\right)\in \left(0\dots {P}-1\right)$
323 187 322 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(0\dots {M}\right)\right)\to {c}\left({k}\right)\in ℝ$
324 321 323 syldan ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to {c}\left({k}\right)\in ℝ$
325 elfzle1 ${⊢}{c}\left({k}\right)\in \left(0\dots {P}-1\right)\to 0\le {c}\left({k}\right)$
326 322 325 syl ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(0\dots {M}\right)\right)\to 0\le {c}\left({k}\right)$
327 321 326 syldan ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(\left(1\dots {M}\right)\setminus \left\{{j}\right\}\right)\right)\to 0\le {c}\left({k}\right)$
328 318 324 327 fsumge0 ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to 0\le \sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)$
329 328 adantr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to 0\le \sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)$
330 318 324 fsumrecl ${⊢}\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\to \sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)\in ℝ$
331 330 adantr ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)\in ℝ$
332 279 331 addge01d ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(0\le \sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)↔{c}\left({j}\right)\le {c}\left({j}\right)+\sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)\right)$
333 329 332 mpbid ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)\le {c}\left({j}\right)+\sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)$
334 333 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {c}\left({j}\right)\le {c}\left({j}\right)+\sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)$
335 277 280 310 316 334 ltletrd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to 0<{c}\left({j}\right)+\sum _{{k}\in \left(1\dots {M}\right)\setminus \left\{{j}\right\}}{c}\left({k}\right)$
336 335 309 breqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to 0<\sum _{{k}=1}^{{M}}{c}\left({k}\right)$
337 276 336 elrpd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{k}=1}^{{M}}{c}\left({k}\right)\in {ℝ}^{+}$
338 268 337 ltaddrpd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {P}-1<{P}-1+\sum _{{k}=1}^{{M}}{c}\left({k}\right)$
339 338 adantl3r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {P}-1<{P}-1+\sum _{{k}=1}^{{M}}{c}\left({k}\right)$
340 fveq2 ${⊢}{j}={k}\to {c}\left({j}\right)={c}\left({k}\right)$
341 340 cbvsumv ${⊢}\sum _{{j}=0}^{{M}}{c}\left({j}\right)=\sum _{{k}=0}^{{M}}{c}\left({k}\right)$
342 341 a1i ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{j}=0}^{{M}}{c}\left({j}\right)=\sum _{{k}=0}^{{M}}{c}\left({k}\right)$
343 73 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {M}\in {ℤ}_{\ge 0}$
344 simp-5l ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\wedge {k}\in \left(0\dots {M}\right)\right)\to \left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)$
345 74 322 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {k}\in \left(0\dots {M}\right)\right)\to {c}\left({k}\right)\in ℂ$
346 344 345 sylancom ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\wedge {k}\in \left(0\dots {M}\right)\right)\to {c}\left({k}\right)\in ℂ$
347 fveq2 ${⊢}{k}=0\to {c}\left({k}\right)={c}\left(0\right)$
348 343 346 347 fsum1p ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{k}=0}^{{M}}{c}\left({k}\right)={c}\left(0\right)+\sum _{{k}=0+1}^{{M}}{c}\left({k}\right)$
349 257 ad4antlr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {c}\left(0\right)={P}-1$
350 86 sumeq1i ${⊢}\sum _{{k}=0+1}^{{M}}{c}\left({k}\right)=\sum _{{k}=1}^{{M}}{c}\left({k}\right)$
351 350 a1i ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{k}=0+1}^{{M}}{c}\left({k}\right)=\sum _{{k}=1}^{{M}}{c}\left({k}\right)$
352 349 351 oveq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {c}\left(0\right)+\sum _{{k}=0+1}^{{M}}{c}\left({k}\right)={P}-1+\sum _{{k}=1}^{{M}}{c}\left({k}\right)$
353 342 348 352 3eqtrrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {P}-1+\sum _{{k}=1}^{{M}}{c}\left({k}\right)=\sum _{{j}=0}^{{M}}{c}\left({j}\right)$
354 339 353 breqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to {P}-1<\sum _{{j}=0}^{{M}}{c}\left({j}\right)$
355 267 354 gtned ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to \sum _{{j}=0}^{{M}}{c}\left({j}\right)\ne {P}-1$
356 355 neneqd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\wedge ¬{c}\left({j}\right)=0\right)\to ¬\sum _{{j}=0}^{{M}}{c}\left({j}\right)={P}-1$
357 266 356 condan ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to {c}\left({j}\right)=0$
358 simpr ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
359 34 67 sseldi ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to if\left({j}=0,{P}-1,0\right)\in {ℕ}_{0}$
360 5 fvmpt2 ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge if\left({j}=0,{P}-1,0\right)\in {ℕ}_{0}\right)\to {D}\left({j}\right)=if\left({j}=0,{P}-1,0\right)$
361 358 359 360 syl2anc ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {D}\left({j}\right)=if\left({j}=0,{P}-1,0\right)$
362 361 adantr ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to {D}\left({j}\right)=if\left({j}=0,{P}-1,0\right)$
363 simpr ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to ¬{j}=0$
364 363 iffalsed ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to if\left({j}=0,{P}-1,0\right)=0$
365 362 364 eqtr2d ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to 0={D}\left({j}\right)$
366 365 adantllr ${⊢}\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to 0={D}\left({j}\right)$
367 366 adantllr ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to 0={D}\left({j}\right)$
368 357 367 eqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge ¬{j}=0\right)\to {c}\left({j}\right)={D}\left({j}\right)$
369 265 368 pm2.61dan ${⊢}\left(\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)={D}\left({j}\right)$
370 251 253 369 eqfnfvd ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {P}-1={c}\left(0\right)\right)\to {c}={D}$
371 236 370 sylanl2 ${⊢}\left(\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\wedge {P}-1={c}\left(0\right)\right)\to {c}={D}$
372 eldifsni ${⊢}{c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\to {c}\ne {D}$
373 372 neneqd ${⊢}{c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\to ¬{c}={D}$
374 373 ad2antlr ${⊢}\left(\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\wedge {P}-1={c}\left(0\right)\right)\to ¬{c}={D}$
375 371 374 pm2.65da ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to ¬{P}-1={c}\left(0\right)$
376 375 neqned ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {P}-1\ne {c}\left(0\right)$
377 240 241 243 376 leneltd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {c}\left(0\right)<{P}-1$
378 240 241 posdifd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left({c}\left(0\right)<{P}-1↔0<{P}-1-{c}\left(0\right)\right)$
379 377 378 mpbid ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to 0<{P}-1-{c}\left(0\right)$
380 elnnz ${⊢}{P}-1-{c}\left(0\right)\in ℕ↔\left({P}-1-{c}\left(0\right)\in ℤ\wedge 0<{P}-1-{c}\left(0\right)\right)$
381 249 379 380 sylanbrc ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {P}-1-{c}\left(0\right)\in ℕ$
382 381 0expd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {0}^{{P}-1-{c}\left(0\right)}=0$
383 382 oveq2d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right){0}^{{P}-1-{c}\left(0\right)}=\left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right)\cdot 0$
384 161 adantr ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left({P}-1\right)!\in ℂ$
385 381 nnnn0d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to {P}-1-{c}\left(0\right)\in {ℕ}_{0}$
386 385 faccld ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left({P}-1-{c}\left(0\right)\right)!\in ℕ$
387 386 nncnd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left({P}-1-{c}\left(0\right)\right)!\in ℂ$
388 386 nnne0d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left({P}-1-{c}\left(0\right)\right)!\ne 0$
389 384 387 388 divcld ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\in ℂ$
390 389 mul01d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left(\frac{\left({P}-1\right)!}{\left({P}-1-{c}\left(0\right)\right)!}\right)\cdot 0=0$
391 245 383 390 3eqtrd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\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){0}^{{P}-1-{c}\left(0\right)}\right)=0$
392 391 oveq1d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=0\cdot \prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)$
393 236 56 sylan2 ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)\in ℤ$
394 393 zcnd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)\in ℂ$
395 394 mul02d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to 0\cdot \prod _{{j}=1}^{{M}}if\left({P}<{c}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{c}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=0$
396 392 395 eqtrd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=0$
397 396 oveq2d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=\left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\cdot 0$
398 fzfid ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left(0\dots {M}\right)\in \mathrm{Fin}$
399 34 278 sseldi ${⊢}\left(\left({\phi }\wedge {c}\in {C}\left({P}-1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)\in {ℕ}_{0}$
400 236 399 sylanl2 ${⊢}\left(\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)\in {ℕ}_{0}$
401 400 faccld ${⊢}\left(\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {c}\left({j}\right)!\in ℕ$
402 398 401 fprodnncl ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \prod _{{j}=0}^{{M}}{c}\left({j}\right)!\in ℕ$
403 402 nncnd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \prod _{{j}=0}^{{M}}{c}\left({j}\right)!\in ℂ$
404 402 nnne0d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \prod _{{j}=0}^{{M}}{c}\left({j}\right)!\ne 0$
405 384 403 404 divcld ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\in ℂ$
406 405 mul01d ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{c}\left({j}\right)!}\right)\cdot 0=0$
407 397 406 eqtrd ${⊢}\left({\phi }\wedge {c}\in \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\right)\right)\to \left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=0$
408 407 sumeq2dv ${⊢}{\phi }\to \sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}\left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=\sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}0$
409 diffi ${⊢}{C}\left({P}-1\right)\in \mathrm{Fin}\to {C}\left({P}-1\right)\setminus \left\{{D}\right\}\in \mathrm{Fin}$
410 20 409 syl ${⊢}{\phi }\to {C}\left({P}-1\right)\setminus \left\{{D}\right\}\in \mathrm{Fin}$
411 410 olcd ${⊢}{\phi }\to \left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\subseteq {ℤ}_{\ge 0}\vee {C}\left({P}-1\right)\setminus \left\{{D}\right\}\in \mathrm{Fin}\right)$
412 sumz ${⊢}\left({C}\left({P}-1\right)\setminus \left\{{D}\right\}\subseteq {ℤ}_{\ge 0}\vee {C}\left({P}-1\right)\setminus \left\{{D}\right\}\in \mathrm{Fin}\right)\to \sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}0=0$
413 411 412 syl ${⊢}{\phi }\to \sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}0=0$
414 408 413 eqtrd ${⊢}{\phi }\to \sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}\left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=0$
415 235 414 oveq12d ${⊢}{\phi }\to \left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\right)if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)+\sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}\left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=\left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}+0$
416 233 addid1d ${⊢}{\phi }\to \left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}+0=\left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}$
417 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
418 417 206 228 220 fprodexp ${⊢}{\phi }\to \prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}={\prod _{{j}=1}^{{M}}\left(-{j}\right)}^{{P}}$
419 418 oveq2d ${⊢}{\phi }\to \left({P}-1\right)!\prod _{{j}=1}^{{M}}{\left(-{j}\right)}^{{P}}=\left({P}-1\right)!{\prod _{{j}=1}^{{M}}\left(-{j}\right)}^{{P}}$
420 415 416 419 3eqtrd ${⊢}{\phi }\to \left(\frac{\left({P}-1\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\right)if\left({P}-1<{D}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{D}\left(0\right)\right)!}\right){0}^{{P}-1-{D}\left(0\right)}\right)\prod _{{j}=1}^{{M}}if\left({P}<{D}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{D}\left({j}\right)\right)!}\right){\left(0-{j}\right)}^{{P}-{D}\left({j}\right)}\right)+\sum _{{c}\in {C}\left({P}-1\right)\setminus \left\{{D}\right\}}\left(\frac{\left({P}-1\right)!}{\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){0}^{{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(0-{j}\right)}^{{P}-{c}\left({j}\right)}\right)=\left({P}-1\right)!{\prod _{{j}=1}^{{M}}\left(-{j}\right)}^{{P}}$
421 17 143 420 3eqtrd ${⊢}{\phi }\to \left(ℝ{D}^{n}{F}\right)\left({P}-1\right)\left(0\right)=\left({P}-1\right)!{\prod _{{j}=1}^{{M}}\left(-{j}\right)}^{{P}}$