etransclem31

Description: The N -th derivative of H applied to Y . (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		etransclem31.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem31.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem31.p	$⊢ φ \to P \in ℕ$
4		etransclem31.m	$⊢ φ \to M \in ℕ_{0}$
5		etransclem31.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
6		etransclem31.n	$⊢ φ \to N \in ℕ_{0}$
7		etransclem31.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
8		etransclem31.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
9		etransclem31.y	$⊢ φ \to Y \in X$
10	1 2 3 4 5 6 7 8	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))$
11		fveq2	$⊢ x = Y \to (S D^{n} H (j)) (c (j)) (x) = (S D^{n} H (j)) (c (j)) (Y)$
12	11	prodeq2ad	$⊢ x = Y \to \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (x) = \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y)$
13	12	oveq2d	$⊢ x = Y \to (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (x) = (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y)$
14	13	sumeq2sdv	$⊢ x = Y \to \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) = \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y)$
15	14	adantl	$⊢ (φ \land x = Y) \to \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) = \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y)$
16	8 6	etransclem16	$⊢ φ \to C (N) \in Fin$
17	6	faccld	$⊢ φ \to N! \in ℕ$
18	17	nncnd	$⊢ φ \to N! \in ℂ$
19	18	adantr	$⊢ (φ \land c \in C (N)) \to N! \in ℂ$
20		fzfid	$⊢ (φ \land c \in C (N)) \to (0 \dots M) \in Fin$
21		fzssnn0	$⊢ (0 \dots N) \subseteq ℕ_{0}$
22		ssrab2	$⊢ \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \subseteq {(0 \dots N)}^{(0 \dots M)}$
23		simpr	$⊢ (φ \land c \in C (N)) \to c \in C (N)$
24	8 6	etransclem12	$⊢ φ \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
25	24	adantr	$⊢ (φ \land c \in C (N)) \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
26	23 25	eleqtrd	$⊢ (φ \land c \in C (N)) \to c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
27	22 26	sseldi	$⊢ (φ \land c \in C (N)) \to c \in ({(0 \dots N)}^{(0 \dots M)})$
28	27	adantr	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to c \in ({(0 \dots N)}^{(0 \dots M)})$
29		elmapi	$⊢ c \in ({(0 \dots N)}^{(0 \dots M)}) \to c : (0 \dots M) ⟶ (0 \dots N)$
30	28 29	syl	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to c : (0 \dots M) ⟶ (0 \dots N)$
31		simpr	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to j \in (0 \dots M)$
32	30 31	ffvelrnd	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to c (j) \in (0 \dots N)$
33	21 32	sseldi	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to c (j) \in ℕ_{0}$
34	33	faccld	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to c (j)! \in ℕ$
35	34	nncnd	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to c (j)! \in ℂ$
36	20 35	fprodcl	$⊢ (φ \land c \in C (N)) \to \prod_{j = 0}^{M} c (j)! \in ℂ$
37	34	nnne0d	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to c (j)! \neq 0$
38	20 35 37	fprodn0	$⊢ (φ \land c \in C (N)) \to \prod_{j = 0}^{M} c (j)! \neq 0$
39	19 36 38	divcld	$⊢ (φ \land c \in C (N)) \to \frac{N!}{\prod_{j = 0}^{M} c (j)!} \in ℂ$
40	1	ad2antrr	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to S \in \{ℝ, ℂ\}$
41	2	ad2antrr	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
42	3	ad2antrr	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to P \in ℕ$
43		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)}))$
44	7 43	eqtri	$⊢ H = (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)}))$
45	40 41 42 44 31 33	etransclem20	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (c (j)) : X ⟶ ℂ$
46	9	ad2antrr	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to Y \in X$
47	45 46	ffvelrnd	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (c (j)) (Y) \in ℂ$
48	20 47	fprodcl	$⊢ (φ \land c \in C (N)) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y) \in ℂ$
49	39 48	mulcld	$⊢ (φ \land c \in C (N)) \to (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y) \in ℂ$
50	16 49	fsumcl	$⊢ φ \to \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y) \in ℂ$
51	10 15 9 50	fvmptd	$⊢ φ \to (S D^{n} F) (N) (Y) = \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y)$
52	40 41 42 44 31 33 46	etransclem21	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (c (j)) (Y) = if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)})$
53	52	prodeq2dv	$⊢ (φ \land c \in C (N)) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y) = \prod_{j = 0}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)})$
54		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
55	4 54	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
56	55	adantr	$⊢ (φ \land c \in C (N)) \to M \in ℤ_{\geq 0}$
57	52 47	eqeltrrd	$⊢ ((φ \land c \in C (N)) \land j \in (0 \dots M)) \to if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) \in ℂ$
58		iftrue	$⊢ j = 0 \to if (j = 0, P - 1, P) = P - 1$
59		fveq2	$⊢ j = 0 \to c (j) = c (0)$
60	58 59	breq12d	$⊢ j = 0 \to (if (j = 0, P - 1, P) < c (j) \leftrightarrow P - 1 < c (0))$
61	58	fveq2d	$⊢ j = 0 \to if (j = 0, P - 1, P)! = (P - 1)!$
62	58 59	oveq12d	$⊢ j = 0 \to if (j = 0, P - 1, P) - c (j) = P - 1 - c (0)$
63	62	fveq2d	$⊢ j = 0 \to (if (j = 0, P - 1, P) - c (j))! = (P - 1 - c (0))!$
64	61 63	oveq12d	$⊢ j = 0 \to \frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!} = \frac{(P - 1)!}{(P - 1 - c (0))!}$
65		oveq2	$⊢ j = 0 \to Y - j = Y - 0$
66	65 62	oveq12d	$⊢ j = 0 \to {(Y - j)}^{if (j = 0, P - 1, P) - c (j)} = {(Y - 0)}^{P - 1 - c (0)}$
67	64 66	oveq12d	$⊢ j = 0 \to (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)} = (\frac{(P - 1)!}{(P - 1 - c (0))!}) {(Y - 0)}^{P - 1 - c (0)}$
68	60 67	ifbieq2d	$⊢ j = 0 \to if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) {(Y - 0)}^{P - 1 - c (0)})$
69	56 57 68	fprod1p	$⊢ (φ \land c \in C (N)) \to \prod_{j = 0}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) {(Y - 0)}^{P - 1 - c (0)}) \prod_{j = 0 + 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)})$
70	1 2	dvdmsscn	$⊢ φ \to X \subseteq ℂ$
71	70 9	sseldd	$⊢ φ \to Y \in ℂ$
72	71	subid1d	$⊢ φ \to Y - 0 = Y$
73	72	oveq1d	$⊢ φ \to {(Y - 0)}^{P - 1 - c (0)} = Y^{P - 1 - c (0)}$
74	73	oveq2d	$⊢ φ \to (\frac{(P - 1)!}{(P - 1 - c (0))!}) {(Y - 0)}^{P - 1 - c (0)} = (\frac{(P - 1)!}{(P - 1 - c (0))!}) Y^{P - 1 - c (0)}$
75	74	ifeq2d	$⊢ φ \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) {(Y - 0)}^{P - 1 - c (0)}) = if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) Y^{P - 1 - c (0)})$
76		0p1e1	$⊢ 0 + 1 = 1$
77	76	oveq1i	$⊢ (0 + 1 \dots M) = (1 \dots M)$
78	77	prodeq1i	$⊢ \prod_{j = 0 + 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = \prod_{j = 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)})$
79		0red	$⊢ j \in (1 \dots M) \to 0 \in ℝ$
80		1red	$⊢ j \in (1 \dots M) \to 1 \in ℝ$
81		elfzelz	$⊢ j \in (1 \dots M) \to j \in ℤ$
82	81	zred	$⊢ j \in (1 \dots M) \to j \in ℝ$
83		0lt1	$⊢ 0 < 1$
84	83	a1i	$⊢ j \in (1 \dots M) \to 0 < 1$
85		elfzle1	$⊢ j \in (1 \dots M) \to 1 \leq j$
86	79 80 82 84 85	ltletrd	$⊢ j \in (1 \dots M) \to 0 < j$
87	86	gt0ne0d	$⊢ j \in (1 \dots M) \to j \neq 0$
88	87	neneqd	$⊢ j \in (1 \dots M) \to \neg j = 0$
89	88	iffalsed	$⊢ j \in (1 \dots M) \to if (j = 0, P - 1, P) = P$
90	89	breq1d	$⊢ j \in (1 \dots M) \to (if (j = 0, P - 1, P) < c (j) \leftrightarrow P < c (j))$
91	89	fveq2d	$⊢ j \in (1 \dots M) \to if (j = 0, P - 1, P)! = P!$
92	89	oveq1d	$⊢ j \in (1 \dots M) \to if (j = 0, P - 1, P) - c (j) = P - c (j)$
93	92	fveq2d	$⊢ j \in (1 \dots M) \to (if (j = 0, P - 1, P) - c (j))! = (P - c (j))!$
94	91 93	oveq12d	$⊢ j \in (1 \dots M) \to \frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!} = \frac{P!}{(P - c (j))!}$
95	92	oveq2d	$⊢ j \in (1 \dots M) \to {(Y - j)}^{if (j = 0, P - 1, P) - c (j)} = {(Y - j)}^{P - c (j)}$
96	94 95	oveq12d	$⊢ j \in (1 \dots M) \to (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)} = (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)}$
97	90 96	ifbieq2d	$⊢ j \in (1 \dots M) \to if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
98	97	prodeq2i	$⊢ \prod_{j = 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
99	78 98	eqtri	$⊢ \prod_{j = 0 + 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
100	99	a1i	$⊢ φ \to \prod_{j = 0 + 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
101	75 100	oveq12d	$⊢ φ \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) {(Y - 0)}^{P - 1 - c (0)}) \prod_{j = 0 + 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) Y^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
102	101	adantr	$⊢ (φ \land c \in C (N)) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) {(Y - 0)}^{P - 1 - c (0)}) \prod_{j = 0 + 1}^{M} if (if (j = 0, P - 1, P) < c (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - c (j))!}) {(Y - j)}^{if (j = 0, P - 1, P) - c (j)}) = if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) Y^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
103	53 69 102	3eqtrd	$⊢ (φ \land c \in C (N)) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y) = if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) Y^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
104	103	oveq2d	$⊢ (φ \land c \in C (N)) \to (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y) = (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) Y^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
105	104	sumeq2dv	$⊢ φ \to \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (Y) = \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))!}) Y^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$
106	51 105	eqtrd	$⊢ φ \to (S D^{n} F) (N) (Y) = \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))!}) Y^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(Y - j)}^{P - c (j)})$

Metamath Proof Explorer

Theorem etransclem31

Proof