# Metamath Proof Explorer

## Theorem etransclem14

Description: Value of the term T , when J = 0 and ( C0 ) = P - 1 (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem14.n ${⊢}{\phi }\to {P}\in ℕ$
etransclem14.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem14.c ${⊢}{\phi }\to {C}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
etransclem14.t ${⊢}{T}=\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){{J}}^{{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({J}-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$
etransclem14.j ${⊢}{\phi }\to {J}=0$
etransclem14.cpm1 ${⊢}{\phi }\to {C}\left(0\right)={P}-1$
Assertion etransclem14 ${⊢}{\phi }\to {T}=\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{C}\left({j}\right)!}\right)\left({P}-1\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(-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$

### Proof

Step Hyp Ref Expression
1 etransclem14.n ${⊢}{\phi }\to {P}\in ℕ$
2 etransclem14.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
3 etransclem14.c ${⊢}{\phi }\to {C}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
4 etransclem14.t ${⊢}{T}=\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){{J}}^{{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({J}-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$
5 etransclem14.j ${⊢}{\phi }\to {J}=0$
6 etransclem14.cpm1 ${⊢}{\phi }\to {C}\left(0\right)={P}-1$
7 fzssre ${⊢}\left(0\dots {N}\right)\subseteq ℝ$
8 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
9 2 8 eleqtrdi ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
10 eluzfz1 ${⊢}{M}\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {M}\right)$
11 9 10 syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
12 3 11 ffvelrnd ${⊢}{\phi }\to {C}\left(0\right)\in \left(0\dots {N}\right)$
13 7 12 sseldi ${⊢}{\phi }\to {C}\left(0\right)\in ℝ$
14 6 13 eqeltrrd ${⊢}{\phi }\to {P}-1\in ℝ$
15 13 14 lttri3d ${⊢}{\phi }\to \left({C}\left(0\right)={P}-1↔\left(¬{C}\left(0\right)<{P}-1\wedge ¬{P}-1<{C}\left(0\right)\right)\right)$
16 6 15 mpbid ${⊢}{\phi }\to \left(¬{C}\left(0\right)<{P}-1\wedge ¬{P}-1<{C}\left(0\right)\right)$
17 16 simprd ${⊢}{\phi }\to ¬{P}-1<{C}\left(0\right)$
18 17 iffalsed ${⊢}{\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){{J}}^{{P}-1-{C}\left(0\right)}\right)=\left(\frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}\right){{J}}^{{P}-1-{C}\left(0\right)}$
19 14 recnd ${⊢}{\phi }\to {P}-1\in ℂ$
20 6 eqcomd ${⊢}{\phi }\to {P}-1={C}\left(0\right)$
21 19 20 subeq0bd ${⊢}{\phi }\to {P}-1-{C}\left(0\right)=0$
22 21 fveq2d ${⊢}{\phi }\to \left({P}-1-{C}\left(0\right)\right)!=0!$
23 fac0 ${⊢}0!=1$
24 22 23 eqtrdi ${⊢}{\phi }\to \left({P}-1-{C}\left(0\right)\right)!=1$
25 24 oveq2d ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}=\frac{\left({P}-1\right)!}{1}$
26 nnm1nn0 ${⊢}{P}\in ℕ\to {P}-1\in {ℕ}_{0}$
27 1 26 syl ${⊢}{\phi }\to {P}-1\in {ℕ}_{0}$
28 27 faccld ${⊢}{\phi }\to \left({P}-1\right)!\in ℕ$
29 28 nncnd ${⊢}{\phi }\to \left({P}-1\right)!\in ℂ$
30 29 div1d ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{1}=\left({P}-1\right)!$
31 25 30 eqtrd ${⊢}{\phi }\to \frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}=\left({P}-1\right)!$
32 5 21 oveq12d ${⊢}{\phi }\to {{J}}^{{P}-1-{C}\left(0\right)}={0}^{0}$
33 0exp0e1 ${⊢}{0}^{0}=1$
34 32 33 eqtrdi ${⊢}{\phi }\to {{J}}^{{P}-1-{C}\left(0\right)}=1$
35 31 34 oveq12d ${⊢}{\phi }\to \left(\frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}\right){{J}}^{{P}-1-{C}\left(0\right)}=\left({P}-1\right)!\cdot 1$
36 29 mulid1d ${⊢}{\phi }\to \left({P}-1\right)!\cdot 1=\left({P}-1\right)!$
37 18 35 36 3eqtrd ${⊢}{\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){{J}}^{{P}-1-{C}\left(0\right)}\right)=\left({P}-1\right)!$
38 5 oveq1d ${⊢}{\phi }\to {J}-{j}=0-{j}$
39 df-neg ${⊢}-{j}=0-{j}$
40 38 39 eqtr4di ${⊢}{\phi }\to {J}-{j}=-{j}$
41 40 oveq1d ${⊢}{\phi }\to {\left({J}-{j}\right)}^{{P}-{C}\left({j}\right)}={\left(-{j}\right)}^{{P}-{C}\left({j}\right)}$
42 41 oveq2d ${⊢}{\phi }\to \left(\frac{{P}!}{\left({P}-{C}\left({j}\right)\right)!}\right){\left({J}-{j}\right)}^{{P}-{C}\left({j}\right)}=\left(\frac{{P}!}{\left({P}-{C}\left({j}\right)\right)!}\right){\left(-{j}\right)}^{{P}-{C}\left({j}\right)}$
43 42 ifeq2d ${⊢}{\phi }\to if\left({P}<{C}\left({j}\right),0,\left(\frac{{P}!}{\left({P}-{C}\left({j}\right)\right)!}\right){\left({J}-{j}\right)}^{{P}-{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(-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$
44 43 prodeq2ad ${⊢}{\phi }\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({J}-{j}\right)}^{{P}-{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(-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$
45 37 44 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){{J}}^{{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({J}-{j}\right)}^{{P}-{C}\left({j}\right)}\right)=\left({P}-1\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(-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$
46 45 oveq2d ${⊢}{\phi }\to \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){{J}}^{{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({J}-{j}\right)}^{{P}-{C}\left({j}\right)}\right)=\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{C}\left({j}\right)!}\right)\left({P}-1\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(-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$
47 4 46 syl5eq ${⊢}{\phi }\to {T}=\left(\frac{{N}!}{\prod _{{j}=0}^{{M}}{C}\left({j}\right)!}\right)\left({P}-1\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(-{j}\right)}^{{P}-{C}\left({j}\right)}\right)$