etransclem34

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

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

Proof

Step	Hyp	Ref	Expression
1		etransclem34.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem34.a	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem34.p	$⊢ φ \to P \in ℕ$
4		etransclem34.m	$⊢ φ \to M \in ℕ_{0}$
5		etransclem34.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{k = 1}^{M} {(x - k)}^{P})$
6		etransclem34.n	$⊢ φ \to N \in ℕ_{0}$
7		etransclem34.h	$⊢ H = (k \in (0 \dots M) ⟼ (x \in X ⟼ {(x - k)}^{if (k = 0, P - 1, P)}))$
8		etransclem34.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} c (k) = n\})$
9	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_{k = 0}^{M} c (k)!}) \prod_{k = 0}^{M} (S D^{n} H (k)) (c (k)) (x))$
10	1 2	dvdmsscn	$⊢ φ \to X \subseteq ℂ$
11	8 6	etransclem16	$⊢ φ \to C (N) \in Fin$
12	10	adantr	$⊢ (φ \land c \in C (N)) \to X \subseteq ℂ$
13	6	faccld	$⊢ φ \to N! \in ℕ$
14	13	nncnd	$⊢ φ \to N! \in ℂ$
15	14	adantr	$⊢ (φ \land c \in C (N)) \to N! \in ℂ$
16		fzfid	$⊢ (φ \land c \in C (N)) \to (0 \dots M) \in Fin$
17		fzssnn0	$⊢ (0 \dots N) \subseteq ℕ_{0}$
18		ssrab2	$⊢ \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} c (k) = N\} \subseteq {(0 \dots N)}^{(0 \dots M)}$
19		simpr	$⊢ (φ \land c \in C (N)) \to c \in C (N)$
20	8 6	etransclem12	$⊢ φ \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} c (k) = N\}$
21	20	adantr	$⊢ (φ \land c \in C (N)) \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} c (k) = N\}$
22	19 21	eleqtrd	$⊢ (φ \land c \in C (N)) \to c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} c (k) = N\}$
23	18 22	sselid	$⊢ (φ \land c \in C (N)) \to c \in ({(0 \dots N)}^{(0 \dots M)})$
24		elmapi	$⊢ c \in ({(0 \dots N)}^{(0 \dots M)}) \to c : (0 \dots M) ⟶ (0 \dots N)$
25	23 24	syl	$⊢ (φ \land c \in C (N)) \to c : (0 \dots M) ⟶ (0 \dots N)$
26	25	ffvelrnda	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to c (k) \in (0 \dots N)$
27	17 26	sselid	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to c (k) \in ℕ_{0}$
28	27	faccld	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to c (k)! \in ℕ$
29	28	nncnd	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to c (k)! \in ℂ$
30	16 29	fprodcl	$⊢ (φ \land c \in C (N)) \to \prod_{k = 0}^{M} c (k)! \in ℂ$
31	28	nnne0d	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to c (k)! \neq 0$
32	16 29 31	fprodn0	$⊢ (φ \land c \in C (N)) \to \prod_{k = 0}^{M} c (k)! \neq 0$
33	15 30 32	divcld	$⊢ (φ \land c \in C (N)) \to \frac{N!}{\prod_{k = 0}^{M} c (k)!} \in ℂ$
34		ssid	$⊢ ℂ \subseteq ℂ$
35	34	a1i	$⊢ (φ \land c \in C (N)) \to ℂ \subseteq ℂ$
36	12 33 35	constcncfg	$⊢ (φ \land c \in C (N)) \to (x \in X ⟼ \frac{N!}{\prod_{k = 0}^{M} c (k)!}) : X \underset{cn}{⟶} ℂ$
37	1	ad2antrr	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to S \in \{ℝ, ℂ\}$
38	2	ad2antrr	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
39	3	ad2antrr	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to P \in ℕ$
40		etransclem5	$⊢ (k \in (0 \dots M) ⟼ (x \in X ⟼ {(x - k)}^{if (k = 0, P - 1, P)})) = (j \in (0 \dots M) ⟼ (y \in X ⟼ {(y - j)}^{if (j = 0, P - 1, P)}))$
41	7 40	eqtri	$⊢ H = (j \in (0 \dots M) ⟼ (y \in X ⟼ {(y - j)}^{if (j = 0, P - 1, P)}))$
42		simpr	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to k \in (0 \dots M)$
43	37 38 39 41 42 27	etransclem20	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to (S D^{n} H (k)) (c (k)) : X ⟶ ℂ$
44	43	3adant2	$⊢ ((φ \land c \in C (N)) \land x \in X \land k \in (0 \dots M)) \to (S D^{n} H (k)) (c (k)) : X ⟶ ℂ$
45		simp2	$⊢ ((φ \land c \in C (N)) \land x \in X \land k \in (0 \dots M)) \to x \in X$
46	44 45	ffvelrnd	$⊢ ((φ \land c \in C (N)) \land x \in X \land k \in (0 \dots M)) \to (S D^{n} H (k)) (c (k)) (x) \in ℂ$
47	43	feqmptd	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to (S D^{n} H (k)) (c (k)) = (x \in X ⟼ (S D^{n} H (k)) (c (k)) (x))$
48	37 38 39 41 42 27	etransclem22	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to (S D^{n} H (k)) (c (k)) : X \underset{cn}{⟶} ℂ$
49	47 48	eqeltrrd	$⊢ ((φ \land c \in C (N)) \land k \in (0 \dots M)) \to (x \in X ⟼ (S D^{n} H (k)) (c (k)) (x)) : X \underset{cn}{⟶} ℂ$
50	12 16 46 49	fprodcncf	$⊢ (φ \land c \in C (N)) \to (x \in X ⟼ \prod_{k = 0}^{M} (S D^{n} H (k)) (c (k)) (x)) : X \underset{cn}{⟶} ℂ$
51	36 50	mulcncf	$⊢ (φ \land c \in C (N)) \to (x \in X ⟼ (\frac{N!}{\prod_{k = 0}^{M} c (k)!}) \prod_{k = 0}^{M} (S D^{n} H (k)) (c (k)) (x)) : X \underset{cn}{⟶} ℂ$
52	10 11 51	fsumcncf	$⊢ φ \to (x \in X ⟼ \sum_{c \in C (N)} (\frac{N!}{\prod_{k = 0}^{M} c (k)!}) \prod_{k = 0}^{M} (S D^{n} H (k)) (c (k)) (x)) : X \underset{cn}{⟶} ℂ$
53	9 52	eqeltrd	$⊢ φ \to (S D^{n} F) (N) : X \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem etransclem34

Proof