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	$⊢ φ \to P \in ℕ$
	etransclem26.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem26.n	$⊢ φ \to N \in ℕ_{0}$
	etransclem26.jz	$⊢ φ \to J \in ℤ$
	etransclem26.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
	etransclem26.d	$⊢ φ \to D \in C (N)$
Assertion	etransclem26	$⊢ φ \to (\frac{N!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$

Proof

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

Metamath Proof Explorer

Theorem etransclem26

Proof