# Metamath Proof Explorer

## Theorem etransclem36

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

Ref Expression
Hypotheses etransclem36.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
etransclem36.x ${⊢}{\phi }\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
etransclem36.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem36.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem36.f ${⊢}{F}=\left({x}\in {X}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
etransclem36.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
etransclem36.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)$
etransclem36.jx ${⊢}{\phi }\to {J}\in {X}$
etransclem36.jz ${⊢}{\phi }\to {J}\in ℤ$
etransclem36.10 ${⊢}{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)$
Assertion etransclem36 ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({J}\right)\in ℤ$

### Proof

Step Hyp Ref Expression
1 etransclem36.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 etransclem36.x ${⊢}{\phi }\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
3 etransclem36.p ${⊢}{\phi }\to {P}\in ℕ$
4 etransclem36.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
5 etransclem36.f ${⊢}{F}=\left({x}\in {X}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
6 etransclem36.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
7 etransclem36.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 etransclem36.jx ${⊢}{\phi }\to {J}\in {X}$
9 etransclem36.jz ${⊢}{\phi }\to {J}\in ℤ$
10 etransclem36.10 ${⊢}{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)$
11 1 2 3 4 5 6 7 10 8 etransclem31 ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({J}\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){{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)$
12 10 6 etransclem16 ${⊢}{\phi }\to {C}\left({N}\right)\in \mathrm{Fin}$
13 3 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {P}\in ℕ$
14 4 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {M}\in {ℕ}_{0}$
15 6 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {N}\in {ℕ}_{0}$
16 9 adantr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {J}\in ℤ$
17 etransclem11 ${⊢}\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)=\left({m}\in {ℕ}_{0}⟼\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right\}\right)$
18 etransclem11 ${⊢}\left({m}\in {ℕ}_{0}⟼\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right\}\right)=\left({n}\in {ℕ}_{0}⟼\left\{{e}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{e}\left({j}\right)={n}\right\}\right)$
19 10 17 18 3eqtri ${⊢}{C}=\left({n}\in {ℕ}_{0}⟼\left\{{e}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{e}\left({j}\right)={n}\right\}\right)$
20 simpr ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\to {c}\in {C}\left({N}\right)$
21 13 14 15 16 19 20 etransclem26 ${⊢}\left({\phi }\wedge {c}\in {C}\left({N}\right)\right)\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)\in ℤ$
22 12 21 fsumzcl ${⊢}{\phi }\to \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){{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)\in ℤ$
23 11 22 eqeltrd ${⊢}{\phi }\to \left({S}{D}^{n}{F}\right)\left({N}\right)\left({J}\right)\in ℤ$