Theorem etransclem42

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

	Ref	Expression
Hypotheses	etransclem42.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	etransclem42.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
	etransclem42.p	$$⊢\phi \to P\in \mathbb{N}$$
	etransclem42.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	etransclem42.f	$$⊢F=\left(x\in X⟼x^{P-1}\prod _{j=1}^M{\left(x-j\right)}^P\right)$$
	etransclem42.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	etransclem42.jx	$$⊢\phi \to J\in X$$
	etransclem42.jz	$$⊢\phi \to J\in \mathbb{Z}$$
Assertion	etransclem42	$$⊢\phi \to \left(S{D}^{n}F\right)\left(N\right)\left(J\right)\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		etransclem42.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		etransclem42.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		etransclem42.p	$$⊢\phi \to P\in \mathbb{N}$$
4		etransclem42.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
5		etransclem42.f	$$⊢F=\left(x\in X⟼x^{P-1}\prod _{j=1}^M{\left(x-j\right)}^P\right)$$
6		etransclem42.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		etransclem42.jx	$$⊢\phi \to J\in X$$
8		etransclem42.jz	$$⊢\phi \to J\in \mathbb{Z}$$
9		etransclem5	$$⊢\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)=\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)$$
10		etransclem11	$$⊢\left(m\in {\mathbb{N}}_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 {\mathbb{N}}_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 9 7 8 10	etransclem36	$$⊢\phi \to \left(S{D}^{n}F\right)\left(N\right)\left(J\right)\in \mathbb{Z}$$