etransclem30

Description: The N -th derivative of F . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem30.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	etransclem30.a	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	etransclem30.p	$⊢ φ \to P \in ℕ$
	etransclem30.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem30.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem30.n	$⊢ φ \to N \in ℕ_{0}$
	etransclem30.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
	etransclem30.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
Assertion	etransclem30	$⊢ φ \to (S D^{n} F) (N) = (x \in X ⟼ \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (x))$

Step	Hyp	Ref	Expression
1		etransclem30.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem30.a	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem30.p	$⊢ φ \to P \in ℕ$
4		etransclem30.m	$⊢ φ \to M \in ℕ_{0}$
5		etransclem30.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
6		etransclem30.n	$⊢ φ \to N \in ℕ_{0}$
7		etransclem30.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
8		etransclem30.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
9		eqid	$⊢ (x \in X ⟼ \prod_{j = 0}^{M} H (j) (x)) = (x \in X ⟼ \prod_{j = 0}^{M} H (j) (x))$
10	1 2 3 4 5 6 7 8 9	etransclem29	$⊢ φ \to (S D^{n} F) (N) = (x \in X ⟼ \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (x))$

Metamath Proof Explorer