etransclem29

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

	Ref	Expression
Hypotheses	etranslemdvnf2lemlem.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	etransclem29.a	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	etransclem29.p	$⊢ φ \to P \in ℕ$
	etransclem29.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem29.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem29.n	$⊢ φ \to N \in ℕ_{0}$
	etransclem29.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
	etransclem29.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
	etransclem29.e	$⊢ E = (x \in X ⟼ \prod_{j = 0}^{M} H (j) (x))$
Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		etranslemdvnf2lemlem.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem29.a	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem29.p	$⊢ φ \to P \in ℕ$
4		etransclem29.m	$⊢ φ \to M \in ℕ_{0}$
5		etransclem29.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
6		etransclem29.n	$⊢ φ \to N \in ℕ_{0}$
7		etransclem29.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
8		etransclem29.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
9		etransclem29.e	$⊢ E = (x \in X ⟼ \prod_{j = 0}^{M} H (j) (x))$
10	1 2	dvdmsscn	$⊢ φ \to X \subseteq ℂ$
11	10 3 4 5 7 9	etransclem4	$⊢ φ \to F = E$
12	11	oveq2d	$⊢ φ \to S D^{n} F = S D^{n} E$
13	12	fveq1d	$⊢ φ \to (S D^{n} F) (N) = (S D^{n} E) (N)$
14		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
15	10	adantr	$⊢ (φ \land j \in (0 \dots M)) \to X \subseteq ℂ$
16	3	adantr	$⊢ (φ \land j \in (0 \dots M)) \to P \in ℕ$
17		simpr	$⊢ (φ \land j \in (0 \dots M)) \to j \in (0 \dots M)$
18	15 16 7 17	etransclem1	$⊢ (φ \land j \in (0 \dots M)) \to H (j) : X ⟶ ℂ$
19	1	3ad2ant1	$⊢ (φ \land j \in (0 \dots M) \land i \in (0 \dots N)) \to S \in \{ℝ, ℂ\}$
20	2	3ad2ant1	$⊢ (φ \land j \in (0 \dots M) \land i \in (0 \dots N)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
21	3	3ad2ant1	$⊢ (φ \land j \in (0 \dots M) \land i \in (0 \dots N)) \to P \in ℕ$
22		etransclem5	$⊢ (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)})) = (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)}))$
23	7 22	eqtri	$⊢ H = (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)}))$
24		simp2	$⊢ (φ \land j \in (0 \dots M) \land i \in (0 \dots N)) \to j \in (0 \dots M)$
25		elfznn0	$⊢ i \in (0 \dots N) \to i \in ℕ_{0}$
26	25	3ad2ant3	$⊢ (φ \land j \in (0 \dots M) \land i \in (0 \dots N)) \to i \in ℕ_{0}$
27	19 20 21 23 24 26	etransclem20	$⊢ (φ \land j \in (0 \dots M) \land i \in (0 \dots N)) \to (S D^{n} H (j)) (i) : X ⟶ ℂ$
28	1 2 14 18 6 27 9 8	dvnprod	$⊢ φ \to (S D^{n} E) (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))$
29	13 28	eqtrd	$⊢ φ \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

Theorem etransclem29

Proof