dvtaylp

Description: The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016)

	Ref	Expression
Hypotheses	dvtaylp.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvtaylp.f	$⊢ φ \to F : A ⟶ ℂ$
	dvtaylp.a	$⊢ φ \to A \subseteq S$
	dvtaylp.n	$⊢ φ \to N \in ℕ_{0}$
	dvtaylp.b	$⊢ φ \to B \in dom (S D^{n} F) (N + 1)$
Assertion	dvtaylp	$⊢ φ \to ℂ D ((N + 1) (S Tayl F) B) = N (S Tayl F_{S}^{'}) B$

Proof

Step	Hyp	Ref	Expression
1		dvtaylp.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvtaylp.f	$⊢ φ \to F : A ⟶ ℂ$
3		dvtaylp.a	$⊢ φ \to A \subseteq S$
4		dvtaylp.n	$⊢ φ \to N \in ℕ_{0}$
5		dvtaylp.b	$⊢ φ \to B \in dom (S D^{n} F) (N + 1)$
6		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
7	6	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
8	7	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
9		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
10	9	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
11		toponmax	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ) \to ℂ \in TopOpen (ℂ_{fld})$
12	7 11	mp1i	$⊢ φ \to ℂ \in TopOpen (ℂ_{fld})$
13		fzfid	$⊢ φ \to (0 \dots N + 1) \in Fin$
14		cnex	$⊢ ℂ \in V$
15	14	a1i	$⊢ φ \to ℂ \in V$
16		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
17	15 1 2 3 16	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
18		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
19		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
20	1 17 18 19	syl2an3an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
21		0z	$⊢ 0 \in ℤ$
22		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
23	4 22	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
24	23	nn0zd	$⊢ φ \to N + 1 \in ℤ$
25		fzval2	$⊢ (0 \in ℤ \land N + 1 \in ℤ) \to (0 \dots N + 1) = [0, N + 1] \cap ℤ$
26	21 24 25	sylancr	$⊢ φ \to (0 \dots N + 1) = [0, N + 1] \cap ℤ$
27	26	eleq2d	$⊢ φ \to (k \in (0 \dots N + 1) \leftrightarrow k \in ([0, N + 1] \cap ℤ))$
28	27	biimpa	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ([0, N + 1] \cap ℤ)$
29	1 2 3 23 5	taylplem1	$⊢ (φ \land k \in ([0, N + 1] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
30	28 29	syldan	$⊢ (φ \land k \in (0 \dots N + 1)) \to B \in dom (S D^{n} F) (k)$
31	20 30	ffvelrnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (S D^{n} F) (k) (B) \in ℂ$
32	18	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℕ_{0}$
33	32	faccld	$⊢ (φ \land k \in (0 \dots N + 1)) \to k! \in ℕ$
34	33	nncnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to k! \in ℂ$
35	33	nnne0d	$⊢ (φ \land k \in (0 \dots N + 1)) \to k! \neq 0$
36	31 34 35	divcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
37	36	3adant3	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
38		simp3	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to x \in ℂ$
39		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
40	1 39	syl	$⊢ φ \to S \subseteq ℂ$
41	3 40	sstrd	$⊢ φ \to A \subseteq ℂ$
42		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N + 1 \in ℕ_{0}) \to dom (S D^{n} F) (N + 1) \subseteq dom F$
43	1 17 23 42	syl3anc	$⊢ φ \to dom (S D^{n} F) (N + 1) \subseteq dom F$
44	2 43	fssdmd	$⊢ φ \to dom (S D^{n} F) (N + 1) \subseteq A$
45	44 5	sseldd	$⊢ φ \to B \in A$
46	41 45	sseldd	$⊢ φ \to B \in ℂ$
47	46	3ad2ant1	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to B \in ℂ$
48	38 47	subcld	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to x - B \in ℂ$
49	18	3ad2ant2	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to k \in ℕ_{0}$
50	48 49	expcld	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to {(x - B)}^{k} \in ℂ$
51	37 50	mulcld	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} \in ℂ$
52		0cnd	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land k = 0) \to 0 \in ℂ$
53	49	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to k \in ℂ$
54	53	adantr	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to k \in ℂ$
55	48	adantr	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to x - B \in ℂ$
56	49	adantr	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to k \in ℕ_{0}$
57		simpr	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to \neg k = 0$
58	57	neqned	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to k \neq 0$
59		elnnne0	$⊢ k \in ℕ \leftrightarrow (k \in ℕ_{0} \land k \neq 0)$
60	56 58 59	sylanbrc	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to k \in ℕ$
61		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
62	60 61	syl	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to k - 1 \in ℕ_{0}$
63	55 62	expcld	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to {(x - B)}^{k - 1} \in ℂ$
64	54 63	mulcld	$⊢ ((φ \land k \in (0 \dots N + 1) \land x \in ℂ) \land \neg k = 0) \to k {(x - B)}^{k - 1} \in ℂ$
65	52 64	ifclda	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to if (k = 0, 0, k {(x - B)}^{k - 1}) \in ℂ$
66	37 65	mulcld	$⊢ (φ \land k \in (0 \dots N + 1) \land x \in ℂ) \to (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) \in ℂ$
67	9	a1i	$⊢ (φ \land k \in (0 \dots N + 1)) \to ℂ \in \{ℝ, ℂ\}$
68	50	3expa	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to {(x - B)}^{k} \in ℂ$
69	65	3expa	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to if (k = 0, 0, k {(x - B)}^{k - 1}) \in ℂ$
70	48	3expa	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to x - B \in ℂ$
71		1cnd	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to 1 \in ℂ$
72		simpr	$⊢ ((φ \land k \in (0 \dots N + 1)) \land y \in ℂ) \to y \in ℂ$
73	32	adantr	$⊢ ((φ \land k \in (0 \dots N + 1)) \land y \in ℂ) \to k \in ℕ_{0}$
74	72 73	expcld	$⊢ ((φ \land k \in (0 \dots N + 1)) \land y \in ℂ) \to y^{k} \in ℂ$
75		c0ex	$⊢ 0 \in V$
76		ovex	$⊢ k y^{k - 1} \in V$
77	75 76	ifex	$⊢ if (k = 0, 0, k y^{k - 1}) \in V$
78	77	a1i	$⊢ ((φ \land k \in (0 \dots N + 1)) \land y \in ℂ) \to if (k = 0, 0, k y^{k - 1}) \in V$
79		simpr	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to x \in ℂ$
80	67	dvmptid	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (x \in ℂ⟼ x)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
81	46	ad2antrr	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to B \in ℂ$
82		0cnd	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to 0 \in ℂ$
83	46	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to B \in ℂ$
84	67 83	dvmptc	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (x \in ℂ⟼ B)}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
85	67 79 71 80 81 82 84	dvmptsub	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (x \in ℂ⟼ x - B)}{d_{ℂ} x} = (x \in ℂ ⟼ 1 - 0)$
86		1m0e1	$⊢ 1 - 0 = 1$
87	86	mpteq2i	$⊢ (x \in ℂ ⟼ 1 - 0) = (x \in ℂ ⟼ 1)$
88	85 87	eqtrdi	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (x \in ℂ⟼ x - B)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
89		dvexp2	$⊢ k \in ℕ_{0} \to \frac{d (y \in ℂ⟼ y^{k})}{d_{ℂ} y} = (y \in ℂ ⟼ if (k = 0, 0, k y^{k - 1}))$
90	32 89	syl	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (y \in ℂ⟼ y^{k})}{d_{ℂ} y} = (y \in ℂ ⟼ if (k = 0, 0, k y^{k - 1}))$
91		oveq1	$⊢ y = x - B \to y^{k} = {(x - B)}^{k}$
92		oveq1	$⊢ y = x - B \to y^{k - 1} = {(x - B)}^{k - 1}$
93	92	oveq2d	$⊢ y = x - B \to k y^{k - 1} = k {(x - B)}^{k - 1}$
94	93	ifeq2d	$⊢ y = x - B \to if (k = 0, 0, k y^{k - 1}) = if (k = 0, 0, k {(x - B)}^{k - 1})$
95	67 67 70 71 74 78 88 90 91 94	dvmptco	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (x \in ℂ⟼ {(x - B)}^{k})}{d_{ℂ} x} = (x \in ℂ ⟼ if (k = 0, 0, k {(x - B)}^{k - 1}) \cdot 1)$
96	69	mulid1d	$⊢ ((φ \land k \in (0 \dots N + 1)) \land x \in ℂ) \to if (k = 0, 0, k {(x - B)}^{k - 1}) \cdot 1 = if (k = 0, 0, k {(x - B)}^{k - 1})$
97	96	mpteq2dva	$⊢ (φ \land k \in (0 \dots N + 1)) \to (x \in ℂ ⟼ if (k = 0, 0, k {(x - B)}^{k - 1}) \cdot 1) = (x \in ℂ ⟼ if (k = 0, 0, k {(x - B)}^{k - 1}))$
98	95 97	eqtrd	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (x \in ℂ⟼ {(x - B)}^{k})}{d_{ℂ} x} = (x \in ℂ ⟼ if (k = 0, 0, k {(x - B)}^{k - 1}))$
99	67 68 69 98 36	dvmptcmul	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{d (x \in ℂ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})}{d_{ℂ} x} = (x \in ℂ ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}))$
100	8 6 10 12 13 51 66 99	dvmptfsum	$⊢ φ \to \frac{d (x \in ℂ⟼ \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})}{d_{ℂ} x} = (x \in ℂ ⟼ \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}))$
101		1zzd	$⊢ (φ \land x \in ℂ) \to 1 \in ℤ$
102		0zd	$⊢ (φ \land x \in ℂ) \to 0 \in ℤ$
103	4	nn0zd	$⊢ φ \to N \in ℤ$
104	103	adantr	$⊢ (φ \land x \in ℂ) \to N \in ℤ$
105		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
106	1 105	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
107	40 2 3	dvbss	$⊢ φ \to dom F_{S}^{'} \subseteq A$
108	107 3	sstrd	$⊢ φ \to dom F_{S}^{'} \subseteq S$
109		1nn0	$⊢ 1 \in ℕ_{0}$
110	109	a1i	$⊢ φ \to 1 \in ℕ_{0}$
111		dvnadd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (1 \in ℕ_{0} \land N \in ℕ_{0})) \to (S D^{n} (S D^{n} F) (1)) (N) = (S D^{n} F) (1 + N)$
112	1 17 110 4 111	syl22anc	$⊢ φ \to (S D^{n} (S D^{n} F) (1)) (N) = (S D^{n} F) (1 + N)$
113		dvn1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (1) = S D F$
114	40 17 113	syl2anc	$⊢ φ \to (S D^{n} F) (1) = S D F$
115	114	oveq2d	$⊢ φ \to S D^{n} (S D^{n} F) (1) = S D^{n} F_{S}^{'}$
116	115	fveq1d	$⊢ φ \to (S D^{n} (S D^{n} F) (1)) (N) = (S D^{n} F_{S}^{'}) (N)$
117		1cnd	$⊢ φ \to 1 \in ℂ$
118	4	nn0cnd	$⊢ φ \to N \in ℂ$
119	117 118	addcomd	$⊢ φ \to 1 + N = N + 1$
120	119	fveq2d	$⊢ φ \to (S D^{n} F) (1 + N) = (S D^{n} F) (N + 1)$
121	112 116 120	3eqtr3d	$⊢ φ \to (S D^{n} F_{S}^{'}) (N) = (S D^{n} F) (N + 1)$
122	121	dmeqd	$⊢ φ \to dom (S D^{n} F_{S}^{'}) (N) = dom (S D^{n} F) (N + 1)$
123	5 122	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} F_{S}^{'}) (N)$
124	1 106 108 4 123	taylplem2	$⊢ ((φ \land x \in ℂ) \land j \in (0 \dots N)) \to (\frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!}) {(x - B)}^{j} \in ℂ$
125		fveq2	$⊢ j = k - 1 \to (S D^{n} F_{S}^{'}) (j) = (S D^{n} F_{S}^{'}) (k - 1)$
126	125	fveq1d	$⊢ j = k - 1 \to (S D^{n} F_{S}^{'}) (j) (B) = (S D^{n} F_{S}^{'}) (k - 1) (B)$
127		fveq2	$⊢ j = k - 1 \to j! = (k - 1)!$
128	126 127	oveq12d	$⊢ j = k - 1 \to \frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!} = \frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}$
129		oveq2	$⊢ j = k - 1 \to {(x - B)}^{j} = {(x - B)}^{k - 1}$
130	128 129	oveq12d	$⊢ j = k - 1 \to (\frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!}) {(x - B)}^{j} = (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1}$
131	101 102 104 124 130	fsumshft	$⊢ (φ \land x \in ℂ) \to \sum_{j = 0}^{N} (\frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!}) {(x - B)}^{j} = \sum_{k = 0 + 1}^{N + 1} (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1}$
132		elfznn	$⊢ k \in (1 \dots N + 1) \to k \in ℕ$
133	132	adantl	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to k \in ℕ$
134	133	nnne0d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to k \neq 0$
135		ifnefalse	$⊢ k \neq 0 \to if (k = 0, 0, k {(x - B)}^{k - 1}) = k {(x - B)}^{k - 1}$
136	134 135	syl	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to if (k = 0, 0, k {(x - B)}^{k - 1}) = k {(x - B)}^{k - 1}$
137	136	oveq2d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = (\frac{(S D^{n} F) (k) (B)}{k!}) k {(x - B)}^{k - 1}$
138		simpll	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to φ$
139		fz1ssfz0	$⊢ (1 \dots N + 1) \subseteq (0 \dots N + 1)$
140	139	sseli	$⊢ k \in (1 \dots N + 1) \to k \in (0 \dots N + 1)$
141	140	adantl	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to k \in (0 \dots N + 1)$
142	138 141 36	syl2anc	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
143	133	nncnd	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to k \in ℂ$
144		simplr	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to x \in ℂ$
145	46	ad2antrr	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to B \in ℂ$
146	144 145	subcld	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to x - B \in ℂ$
147	133 61	syl	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to k - 1 \in ℕ_{0}$
148	146 147	expcld	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to {(x - B)}^{k - 1} \in ℂ$
149	142 143 148	mulassd	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) k {(x - B)}^{k - 1} = (\frac{(S D^{n} F) (k) (B)}{k!}) k {(x - B)}^{k - 1}$
150		facp1	$⊢ k - 1 \in ℕ_{0} \to (k - 1 + 1)! = (k - 1)! (k - 1 + 1)$
151	147 150	syl	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (k - 1 + 1)! = (k - 1)! (k - 1 + 1)$
152		1cnd	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to 1 \in ℂ$
153	143 152	npcand	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to k - 1 + 1 = k$
154	153	fveq2d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (k - 1 + 1)! = k!$
155	153	oveq2d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (k - 1)! (k - 1 + 1) = (k - 1)! k$
156	151 154 155	3eqtr3d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to k! = (k - 1)! k$
157	156	oveq2d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B) k}{k!} = \frac{(S D^{n} F) (k) (B) k}{(k - 1)! k}$
158	32	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℂ$
159	31 158 34 35	div23d	$⊢ (φ \land k \in (0 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B) k}{k!} = (\frac{(S D^{n} F) (k) (B)}{k!}) k$
160	138 141 159	syl2anc	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B) k}{k!} = (\frac{(S D^{n} F) (k) (B)}{k!}) k$
161	138 141 31	syl2anc	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (S D^{n} F) (k) (B) \in ℂ$
162	147	faccld	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (k - 1)! \in ℕ$
163	162	nncnd	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (k - 1)! \in ℂ$
164	162	nnne0d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (k - 1)! \neq 0$
165	161 163 143 164 134	divcan5rd	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B) k}{(k - 1)! k} = \frac{(S D^{n} F) (k) (B)}{(k - 1)!}$
166	1	ad2antrr	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to S \in \{ℝ, ℂ\}$
167	17	ad2antrr	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
168	109	a1i	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to 1 \in ℕ_{0}$
169		dvnadd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (1 \in ℕ_{0} \land k - 1 \in ℕ_{0})) \to (S D^{n} (S D^{n} F) (1)) (k - 1) = (S D^{n} F) (1 + k - 1)$
170	166 167 168 147 169	syl22anc	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (S D^{n} (S D^{n} F) (1)) (k - 1) = (S D^{n} F) (1 + k - 1)$
171	114	ad2antrr	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (S D^{n} F) (1) = S D F$
172	171	oveq2d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to S D^{n} (S D^{n} F) (1) = S D^{n} F_{S}^{'}$
173	172	fveq1d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (S D^{n} (S D^{n} F) (1)) (k - 1) = (S D^{n} F_{S}^{'}) (k - 1)$
174	152 143	pncan3d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to 1 + k - 1 = k$
175	174	fveq2d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (S D^{n} F) (1 + k - 1) = (S D^{n} F) (k)$
176	170 173 175	3eqtr3rd	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (S D^{n} F) (k) = (S D^{n} F_{S}^{'}) (k - 1)$
177	176	fveq1d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (S D^{n} F) (k) (B) = (S D^{n} F_{S}^{'}) (k - 1) (B)$
178	177	oveq1d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B)}{(k - 1)!} = \frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}$
179	165 178	eqtrd	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B) k}{(k - 1)! k} = \frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}$
180	157 160 179	3eqtr3d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) k = \frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}$
181	180	oveq1d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) k {(x - B)}^{k - 1} = (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1}$
182	137 149 181	3eqtr2d	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1}$
183	182	sumeq2dv	$⊢ (φ \land x \in ℂ) \to \sum_{k = 1}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = \sum_{k = 1}^{N + 1} (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1}$
184		0p1e1	$⊢ 0 + 1 = 1$
185	184	oveq1i	$⊢ (0 + 1 \dots N + 1) = (1 \dots N + 1)$
186	185	sumeq1i	$⊢ \sum_{k = 0 + 1}^{N + 1} (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1} = \sum_{k = 1}^{N + 1} (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1}$
187	183 186	eqtr4di	$⊢ (φ \land x \in ℂ) \to \sum_{k = 1}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = \sum_{k = 0 + 1}^{N + 1} (\frac{(S D^{n} F_{S}^{'}) (k - 1) (B)}{(k - 1)!}) {(x - B)}^{k - 1}$
188	139	a1i	$⊢ (φ \land x \in ℂ) \to (1 \dots N + 1) \subseteq (0 \dots N + 1)$
189	69	an32s	$⊢ ((φ \land x \in ℂ) \land k \in (0 \dots N + 1)) \to if (k = 0, 0, k {(x - B)}^{k - 1}) \in ℂ$
190	140 189	sylan2	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to if (k = 0, 0, k {(x - B)}^{k - 1}) \in ℂ$
191	142 190	mulcld	$⊢ ((φ \land x \in ℂ) \land k \in (1 \dots N + 1)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) \in ℂ$
192		eldif	$⊢ k \in ((0 \dots N + 1) ∖ (1 \dots N + 1)) \leftrightarrow (k \in (0 \dots N + 1) \land \neg k \in (1 \dots N + 1))$
193	59	biimpri	$⊢ (k \in ℕ_{0} \land k \neq 0) \to k \in ℕ$
194	18 193	sylan	$⊢ (k \in (0 \dots N + 1) \land k \neq 0) \to k \in ℕ$
195		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
196	194 195	eleqtrdi	$⊢ (k \in (0 \dots N + 1) \land k \neq 0) \to k \in ℤ_{\geq 1}$
197		elfzuz3	$⊢ k \in (0 \dots N + 1) \to N + 1 \in ℤ_{\geq k}$
198	197	adantr	$⊢ (k \in (0 \dots N + 1) \land k \neq 0) \to N + 1 \in ℤ_{\geq k}$
199		elfzuzb	$⊢ k \in (1 \dots N + 1) \leftrightarrow (k \in ℤ_{\geq 1} \land N + 1 \in ℤ_{\geq k})$
200	196 198 199	sylanbrc	$⊢ (k \in (0 \dots N + 1) \land k \neq 0) \to k \in (1 \dots N + 1)$
201	200	ex	$⊢ k \in (0 \dots N + 1) \to (k \neq 0 \to k \in (1 \dots N + 1))$
202	201	adantl	$⊢ ((φ \land x \in ℂ) \land k \in (0 \dots N + 1)) \to (k \neq 0 \to k \in (1 \dots N + 1))$
203	202	necon1bd	$⊢ ((φ \land x \in ℂ) \land k \in (0 \dots N + 1)) \to (\neg k \in (1 \dots N + 1) \to k = 0)$
204	203	impr	$⊢ ((φ \land x \in ℂ) \land (k \in (0 \dots N + 1) \land \neg k \in (1 \dots N + 1))) \to k = 0$
205	192 204	sylan2b	$⊢ ((φ \land x \in ℂ) \land k \in ((0 \dots N + 1) ∖ (1 \dots N + 1))) \to k = 0$
206	205	iftrued	$⊢ ((φ \land x \in ℂ) \land k \in ((0 \dots N + 1) ∖ (1 \dots N + 1))) \to if (k = 0, 0, k {(x - B)}^{k - 1}) = 0$
207	206	oveq2d	$⊢ ((φ \land x \in ℂ) \land k \in ((0 \dots N + 1) ∖ (1 \dots N + 1))) \to (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = (\frac{(S D^{n} F) (k) (B)}{k!}) \cdot 0$
208		eldifi	$⊢ k \in ((0 \dots N + 1) ∖ (1 \dots N + 1)) \to k \in (0 \dots N + 1)$
209	36	adantlr	$⊢ ((φ \land x \in ℂ) \land k \in (0 \dots N + 1)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
210	208 209	sylan2	$⊢ ((φ \land x \in ℂ) \land k \in ((0 \dots N + 1) ∖ (1 \dots N + 1))) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
211	210	mul01d	$⊢ ((φ \land x \in ℂ) \land k \in ((0 \dots N + 1) ∖ (1 \dots N + 1))) \to (\frac{(S D^{n} F) (k) (B)}{k!}) \cdot 0 = 0$
212	207 211	eqtrd	$⊢ ((φ \land x \in ℂ) \land k \in ((0 \dots N + 1) ∖ (1 \dots N + 1))) \to (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = 0$
213		fzfid	$⊢ (φ \land x \in ℂ) \to (0 \dots N + 1) \in Fin$
214	188 191 212 213	fsumss	$⊢ (φ \land x \in ℂ) \to \sum_{k = 1}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1})$
215	131 187 214	3eqtr2rd	$⊢ (φ \land x \in ℂ) \to \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1}) = \sum_{j = 0}^{N} (\frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!}) {(x - B)}^{j}$
216	215	mpteq2dva	$⊢ φ \to (x \in ℂ ⟼ \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) if (k = 0, 0, k {(x - B)}^{k - 1})) = (x \in ℂ ⟼ \sum_{j = 0}^{N} (\frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!}) {(x - B)}^{j})$
217	100 216	eqtrd	$⊢ φ \to \frac{d (x \in ℂ⟼ \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})}{d_{ℂ} x} = (x \in ℂ ⟼ \sum_{j = 0}^{N} (\frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!}) {(x - B)}^{j})$
218		eqid	$⊢ (N + 1) (S Tayl F) B = (N + 1) (S Tayl F) B$
219	1 2 3 23 5 218	taylpfval	$⊢ φ \to (N + 1) (S Tayl F) B = (x \in ℂ ⟼ \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$
220	219	oveq2d	$⊢ φ \to ℂ D ((N + 1) (S Tayl F) B) = \frac{d (x \in ℂ⟼ \sum_{k = 0}^{N + 1} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})}{d_{ℂ} x}$
221		eqid	$⊢ N (S Tayl F_{S}^{'}) B = N (S Tayl F_{S}^{'}) B$
222	1 106 108 4 123 221	taylpfval	$⊢ φ \to N (S Tayl F_{S}^{'}) B = (x \in ℂ ⟼ \sum_{j = 0}^{N} (\frac{(S D^{n} F_{S}^{'}) (j) (B)}{j!}) {(x - B)}^{j})$
223	217 220 222	3eqtr4d	$⊢ φ \to ℂ D ((N + 1) (S Tayl F) B) = N (S Tayl F_{S}^{'}) B$

Metamath Proof Explorer

Theorem dvtaylp

Proof