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	$⊢ φ \to S \in \{ℝ, ℂ\}$
	etransclem36.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	etransclem36.p	$⊢ φ \to P \in ℕ$
	etransclem36.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem36.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem36.n	$⊢ φ \to N \in ℕ_{0}$
	etransclem36.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
	etransclem36.jx	$⊢ φ \to J \in X$
	etransclem36.jz	$⊢ φ \to J \in ℤ$
	etransclem36.10	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
Assertion	etransclem36	$⊢ φ \to (S D^{n} F) (N) (J) \in ℤ$

Proof

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

Metamath Proof Explorer

Theorem etransclem36

Proof