# Metamath Proof Explorer

## Theorem etransclem26

Description: Every term in the sum of the N -th derivative of F applied to J is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem26.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem26.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem26.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
etransclem26.jz ${⊢}{\phi }\to {J}\in ℤ$
etransclem26.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)$
etransclem26.d ${⊢}{\phi }\to {D}\in {C}\left({N}\right)$
Assertion etransclem26 ${⊢}{\phi }\to \left(\frac{{N}!}{\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){{J}}^{{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({J}-{j}\right)}^{{P}-{D}\left({j}\right)}\right)\in ℤ$

### Proof

Step Hyp Ref Expression
1 etransclem26.p ${⊢}{\phi }\to {P}\in ℕ$
2 etransclem26.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
3 etransclem26.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
4 etransclem26.jz ${⊢}{\phi }\to {J}\in ℤ$
5 etransclem26.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)$
6 etransclem26.d ${⊢}{\phi }\to {D}\in {C}\left({N}\right)$
7 5 3 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\}$
8 6 7 eleqtrd ${⊢}{\phi }\to {D}\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\}$
9 fveq1 ${⊢}{c}={D}\to {c}\left({j}\right)={D}\left({j}\right)$
10 9 sumeq2sdv ${⊢}{c}={D}\to \sum _{{j}=0}^{{M}}{c}\left({j}\right)=\sum _{{j}=0}^{{M}}{D}\left({j}\right)$
11 10 eqeq1d ${⊢}{c}={D}\to \left(\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}↔\sum _{{j}=0}^{{M}}{D}\left({j}\right)={N}\right)$
12 11 elrab ${⊢}{D}\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\}↔\left({D}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)\wedge \sum _{{j}=0}^{{M}}{D}\left({j}\right)={N}\right)$
13 8 12 sylib ${⊢}{\phi }\to \left({D}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)\wedge \sum _{{j}=0}^{{M}}{D}\left({j}\right)={N}\right)$
14 13 simprd ${⊢}{\phi }\to \sum _{{j}=0}^{{M}}{D}\left({j}\right)={N}$
15 14 eqcomd ${⊢}{\phi }\to {N}=\sum _{{j}=0}^{{M}}{D}\left({j}\right)$
16 15 fveq2d ${⊢}{\phi }\to {N}!=\sum _{{j}=0}^{{M}}{D}\left({j}\right)!$
17 16 oveq1d ${⊢}{\phi }\to \frac{{N}!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}=\frac{\sum _{{j}=0}^{{M}}{D}\left({j}\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}$
18 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{D}$
19 fzfid ${⊢}{\phi }\to \left(0\dots {M}\right)\in \mathrm{Fin}$
20 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
21 fzssnn0 ${⊢}\left(0\dots {N}\right)\subseteq {ℕ}_{0}$
22 mapss ${⊢}\left({ℕ}_{0}\in \mathrm{V}\wedge \left(0\dots {N}\right)\subseteq {ℕ}_{0}\right)\to {\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\subseteq {{ℕ}_{0}}^{\left(0\dots {M}\right)}$
23 20 21 22 mp2an ${⊢}{\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\subseteq {{ℕ}_{0}}^{\left(0\dots {M}\right)}$
24 13 simpld ${⊢}{\phi }\to {D}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)$
25 23 24 sseldi ${⊢}{\phi }\to {D}\in \left({{ℕ}_{0}}^{\left(0\dots {M}\right)}\right)$
26 18 19 25 mccl ${⊢}{\phi }\to \frac{\sum _{{j}=0}^{{M}}{D}\left({j}\right)!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\in ℕ$
27 17 26 eqeltrd ${⊢}{\phi }\to \frac{{N}!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\in ℕ$
28 27 nnzd ${⊢}{\phi }\to \frac{{N}!}{\prod _{{j}=0}^{{M}}{D}\left({j}\right)!}\in ℤ$
29 elmapi ${⊢}{D}\in \left({\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\right)\to {D}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
30 24 29 syl ${⊢}{\phi }\to {D}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
31 1 2 30 4 etransclem10 ${⊢}{\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){{J}}^{{P}-1-{D}\left(0\right)}\right)\in ℤ$
32 fzfid ${⊢}{\phi }\to \left(1\dots {M}\right)\in \mathrm{Fin}$
33 1 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {P}\in ℕ$
34 30 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {D}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
35 0z ${⊢}0\in ℤ$
36 fzp1ss ${⊢}0\in ℤ\to \left(0+1\dots {M}\right)\subseteq \left(0\dots {M}\right)$
37 35 36 ax-mp ${⊢}\left(0+1\dots {M}\right)\subseteq \left(0\dots {M}\right)$
38 1e0p1 ${⊢}1=0+1$
39 38 oveq1i ${⊢}\left(1\dots {M}\right)=\left(0+1\dots {M}\right)$
40 39 eleq2i ${⊢}{j}\in \left(1\dots {M}\right)↔{j}\in \left(0+1\dots {M}\right)$
41 40 biimpi ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in \left(0+1\dots {M}\right)$
42 37 41 sseldi ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in \left(0\dots {M}\right)$
43 42 adantl ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
44 4 adantr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {J}\in ℤ$
45 33 34 43 44 etransclem3 ${⊢}\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({J}-{j}\right)}^{{P}-{D}\left({j}\right)}\right)\in ℤ$
46 32 45 fprodzcl ${⊢}{\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({J}-{j}\right)}^{{P}-{D}\left({j}\right)}\right)\in ℤ$
47 31 46 zmulcld ${⊢}{\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){{J}}^{{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({J}-{j}\right)}^{{P}-{D}\left({j}\right)}\right)\in ℤ$
48 28 47 zmulcld ${⊢}{\phi }\to \left(\frac{{N}!}{\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){{J}}^{{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({J}-{j}\right)}^{{P}-{D}\left({j}\right)}\right)\in ℤ$