dvntaylp

Description: The M -th derivative of the Taylor polynomial is the Taylor polynomial of the M -th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dvntaylp.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvntaylp.f	$⊢ φ \to F : A ⟶ ℂ$
3		dvntaylp.a	$⊢ φ \to A \subseteq S$
4		dvntaylp.m	$⊢ φ \to M \in ℕ_{0}$
5		dvntaylp.n	$⊢ φ \to N \in ℕ_{0}$
6		dvntaylp.b	$⊢ φ \to B \in dom (S D^{n} F) (N + M)$
7		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
8	4 7	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
9		eluzfz2b	$⊢ M \in ℤ_{\geq 0} \leftrightarrow M \in (0 \dots M)$
10	8 9	sylib	$⊢ φ \to M \in (0 \dots M)$
11		fveq2	$⊢ m = 0 \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (ℂ D^{n} ((N + M) (S Tayl F) B)) (0)$
12		fveq2	$⊢ m = 0 \to (S D^{n} F) (m) = (S D^{n} F) (0)$
13	12	oveq2d	$⊢ m = 0 \to S Tayl (S D^{n} F) (m) = S Tayl (S D^{n} F) (0)$
14		oveq2	$⊢ m = 0 \to M - m = M - 0$
15	14	oveq2d	$⊢ m = 0 \to N + M - m = N + M - 0$
16		eqidd	$⊢ m = 0 \to B = B$
17	13 15 16	oveq123d	$⊢ m = 0 \to (N + M - m) (S Tayl (S D^{n} F) (m)) B = (N + M - 0) (S Tayl (S D^{n} F) (0)) B$
18	11 17	eqeq12d	$⊢ m = 0 \to ((ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B \leftrightarrow (ℂ D^{n} ((N + M) (S Tayl F) B)) (0) = (N + M - 0) (S Tayl (S D^{n} F) (0)) B)$
19	18	imbi2d	$⊢ m = 0 \to ((φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B) \leftrightarrow (φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (0) = (N + M - 0) (S Tayl (S D^{n} F) (0)) B))$
20		fveq2	$⊢ m = n \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (ℂ D^{n} ((N + M) (S Tayl F) B)) (n)$
21		fveq2	$⊢ m = n \to (S D^{n} F) (m) = (S D^{n} F) (n)$
22	21	oveq2d	$⊢ m = n \to S Tayl (S D^{n} F) (m) = S Tayl (S D^{n} F) (n)$
23		oveq2	$⊢ m = n \to M - m = M - n$
24	23	oveq2d	$⊢ m = n \to N + M - m = N + M - n$
25		eqidd	$⊢ m = n \to B = B$
26	22 24 25	oveq123d	$⊢ m = n \to (N + M - m) (S Tayl (S D^{n} F) (m)) B = (N + M - n) (S Tayl (S D^{n} F) (n)) B$
27	20 26	eqeq12d	$⊢ m = n \to ((ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B \leftrightarrow (ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = (N + M - n) (S Tayl (S D^{n} F) (n)) B)$
28	27	imbi2d	$⊢ m = n \to ((φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B) \leftrightarrow (φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = (N + M - n) (S Tayl (S D^{n} F) (n)) B))$
29		fveq2	$⊢ m = n + 1 \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1)$
30		fveq2	$⊢ m = n + 1 \to (S D^{n} F) (m) = (S D^{n} F) (n + 1)$
31	30	oveq2d	$⊢ m = n + 1 \to S Tayl (S D^{n} F) (m) = S Tayl (S D^{n} F) (n + 1)$
32		oveq2	$⊢ m = n + 1 \to M - m = M - (n + 1)$
33	32	oveq2d	$⊢ m = n + 1 \to N + M - m = N + M - (n + 1)$
34		eqidd	$⊢ m = n + 1 \to B = B$
35	31 33 34	oveq123d	$⊢ m = n + 1 \to (N + M - m) (S Tayl (S D^{n} F) (m)) B = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B$
36	29 35	eqeq12d	$⊢ m = n + 1 \to ((ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B \leftrightarrow (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B)$
37	36	imbi2d	$⊢ m = n + 1 \to ((φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B) \leftrightarrow (φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B))$
38		fveq2	$⊢ m = M \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (ℂ D^{n} ((N + M) (S Tayl F) B)) (M)$
39		fveq2	$⊢ m = M \to (S D^{n} F) (m) = (S D^{n} F) (M)$
40	39	oveq2d	$⊢ m = M \to S Tayl (S D^{n} F) (m) = S Tayl (S D^{n} F) (M)$
41		oveq2	$⊢ m = M \to M - m = M - M$
42	41	oveq2d	$⊢ m = M \to N + M - m = N + M - M$
43		eqidd	$⊢ m = M \to B = B$
44	40 42 43	oveq123d	$⊢ m = M \to (N + M - m) (S Tayl (S D^{n} F) (m)) B = (N + M - M) (S Tayl (S D^{n} F) (M)) B$
45	38 44	eqeq12d	$⊢ m = M \to ((ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B \leftrightarrow (ℂ D^{n} ((N + M) (S Tayl F) B)) (M) = (N + M - M) (S Tayl (S D^{n} F) (M)) B)$
46	45	imbi2d	$⊢ m = M \to ((φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (m) = (N + M - m) (S Tayl (S D^{n} F) (m)) B) \leftrightarrow (φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (M) = (N + M - M) (S Tayl (S D^{n} F) (M)) B))$
47		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
48		mapsspm	$⊢ ℂ^{ℂ} \subseteq ℂ ↑_{𝑝𝑚} ℂ$
49	5 4	nn0addcld	$⊢ φ \to N + M \in ℕ_{0}$
50		eqid	$⊢ (N + M) (S Tayl F) B = (N + M) (S Tayl F) B$
51	1 2 3 49 6 50	taylpf	$⊢ φ \to ((N + M) (S Tayl F) B) : ℂ ⟶ ℂ$
52		cnex	$⊢ ℂ \in V$
53	52 52	elmap	$⊢ (N + M) (S Tayl F) B \in (ℂ^{ℂ}) \leftrightarrow ((N + M) (S Tayl F) B) : ℂ ⟶ ℂ$
54	51 53	sylibr	$⊢ φ \to (N + M) (S Tayl F) B \in (ℂ^{ℂ})$
55	48 54	sselid	$⊢ φ \to (N + M) (S Tayl F) B \in (ℂ ↑_{𝑝𝑚} ℂ)$
56		dvn0	$⊢ (ℂ \subseteq ℂ \land (N + M) (S Tayl F) B \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (0) = (N + M) (S Tayl F) B$
57	47 55 56	syl2anc	$⊢ φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (0) = (N + M) (S Tayl F) B$
58		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
59	1 58	syl	$⊢ φ \to S \subseteq ℂ$
60	52	a1i	$⊢ φ \to ℂ \in V$
61		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
62	60 1 2 3 61	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
63		dvn0	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$
64	59 62 63	syl2anc	$⊢ φ \to (S D^{n} F) (0) = F$
65	64	oveq2d	$⊢ φ \to S Tayl (S D^{n} F) (0) = S Tayl F$
66	4	nn0cnd	$⊢ φ \to M \in ℂ$
67	66	subid1d	$⊢ φ \to M - 0 = M$
68	67	oveq2d	$⊢ φ \to N + M - 0 = N + M$
69		eqidd	$⊢ φ \to B = B$
70	65 68 69	oveq123d	$⊢ φ \to (N + M - 0) (S Tayl (S D^{n} F) (0)) B = (N + M) (S Tayl F) B$
71	57 70	eqtr4d	$⊢ φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (0) = (N + M - 0) (S Tayl (S D^{n} F) (0)) B$
72	71	a1i	$⊢ M \in ℤ_{\geq 0} \to (φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (0) = (N + M - 0) (S Tayl (S D^{n} F) (0)) B)$
73		oveq2	$⊢ (ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = (N + M - n) (S Tayl (S D^{n} F) (n)) B \to ℂ D (ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = ℂ D ((N + M - n) (S Tayl (S D^{n} F) (n)) B)$
74		ssidd	$⊢ (φ \land n \in (0 ..^M)) \to ℂ \subseteq ℂ$
75	55	adantr	$⊢ (φ \land n \in (0 ..^M)) \to (N + M) (S Tayl F) B \in (ℂ ↑_{𝑝𝑚} ℂ)$
76		elfzouz	$⊢ n \in (0 ..^M) \to n \in ℤ_{\geq 0}$
77	76	adantl	$⊢ (φ \land n \in (0 ..^M)) \to n \in ℤ_{\geq 0}$
78	77 7	eleqtrrdi	$⊢ (φ \land n \in (0 ..^M)) \to n \in ℕ_{0}$
79		dvnp1	$⊢ (ℂ \subseteq ℂ \land (N + M) (S Tayl F) B \in (ℂ ↑_{𝑝𝑚} ℂ) \land n \in ℕ_{0}) \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = ℂ D (ℂ D^{n} ((N + M) (S Tayl F) B)) (n)$
80	74 75 78 79	syl3anc	$⊢ (φ \land n \in (0 ..^M)) \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = ℂ D (ℂ D^{n} ((N + M) (S Tayl F) B)) (n)$
81	1	adantr	$⊢ (φ \land n \in (0 ..^M)) \to S \in \{ℝ, ℂ\}$
82	62	adantr	$⊢ (φ \land n \in (0 ..^M)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
83		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land n \in ℕ_{0}) \to (S D^{n} F) (n) : dom (S D^{n} F) (n) ⟶ ℂ$
84	81 82 78 83	syl3anc	$⊢ (φ \land n \in (0 ..^M)) \to (S D^{n} F) (n) : dom (S D^{n} F) (n) ⟶ ℂ$
85		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land n \in ℕ_{0}) \to dom (S D^{n} F) (n) \subseteq dom F$
86	81 82 78 85	syl3anc	$⊢ (φ \land n \in (0 ..^M)) \to dom (S D^{n} F) (n) \subseteq dom F$
87	2	fdmd	$⊢ φ \to dom F = A$
88	87	adantr	$⊢ (φ \land n \in (0 ..^M)) \to dom F = A$
89	86 88	sseqtrd	$⊢ (φ \land n \in (0 ..^M)) \to dom (S D^{n} F) (n) \subseteq A$
90	3	adantr	$⊢ (φ \land n \in (0 ..^M)) \to A \subseteq S$
91	89 90	sstrd	$⊢ (φ \land n \in (0 ..^M)) \to dom (S D^{n} F) (n) \subseteq S$
92	5	adantr	$⊢ (φ \land n \in (0 ..^M)) \to N \in ℕ_{0}$
93		fzofzp1	$⊢ n \in (0 ..^M) \to n + 1 \in (0 \dots M)$
94	93	adantl	$⊢ (φ \land n \in (0 ..^M)) \to n + 1 \in (0 \dots M)$
95		fznn0sub	$⊢ n + 1 \in (0 \dots M) \to M - (n + 1) \in ℕ_{0}$
96	94 95	syl	$⊢ (φ \land n \in (0 ..^M)) \to M - (n + 1) \in ℕ_{0}$
97	92 96	nn0addcld	$⊢ (φ \land n \in (0 ..^M)) \to N + M - (n + 1) \in ℕ_{0}$
98	6	adantr	$⊢ (φ \land n \in (0 ..^M)) \to B \in dom (S D^{n} F) (N + M)$
99		elfzofz	$⊢ n \in (0 ..^M) \to n \in (0 \dots M)$
100	99	adantl	$⊢ (φ \land n \in (0 ..^M)) \to n \in (0 \dots M)$
101		fznn0sub	$⊢ n \in (0 \dots M) \to M - n \in ℕ_{0}$
102	100 101	syl	$⊢ (φ \land n \in (0 ..^M)) \to M - n \in ℕ_{0}$
103	92 102	nn0addcld	$⊢ (φ \land n \in (0 ..^M)) \to N + M - n \in ℕ_{0}$
104		dvnadd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (n \in ℕ_{0} \land N + M - n \in ℕ_{0})) \to (S D^{n} (S D^{n} F) (n)) (N + M - n) = (S D^{n} F) (n + N + (M - n))$
105	81 82 78 103 104	syl22anc	$⊢ (φ \land n \in (0 ..^M)) \to (S D^{n} (S D^{n} F) (n)) (N + M - n) = (S D^{n} F) (n + N + (M - n))$
106	5	nn0cnd	$⊢ φ \to N \in ℂ$
107	106	adantr	$⊢ (φ \land n \in (0 ..^M)) \to N \in ℂ$
108	96	nn0cnd	$⊢ (φ \land n \in (0 ..^M)) \to M - (n + 1) \in ℂ$
109		1cnd	$⊢ (φ \land n \in (0 ..^M)) \to 1 \in ℂ$
110	107 108 109	addassd	$⊢ (φ \land n \in (0 ..^M)) \to N + (M - (n + 1)) + 1 = N + (M - (n + 1)) + 1$
111	66	adantr	$⊢ (φ \land n \in (0 ..^M)) \to M \in ℂ$
112	78	nn0cnd	$⊢ (φ \land n \in (0 ..^M)) \to n \in ℂ$
113	111 112 109	nppcan2d	$⊢ (φ \land n \in (0 ..^M)) \to M - (n + 1) + 1 = M - n$
114	113	oveq2d	$⊢ (φ \land n \in (0 ..^M)) \to N + (M - (n + 1)) + 1 = N + M - n$
115	110 114	eqtrd	$⊢ (φ \land n \in (0 ..^M)) \to N + (M - (n + 1)) + 1 = N + M - n$
116	115	fveq2d	$⊢ (φ \land n \in (0 ..^M)) \to (S D^{n} (S D^{n} F) (n)) (N + (M - (n + 1)) + 1) = (S D^{n} (S D^{n} F) (n)) (N + M - n)$
117	112 111	pncan3d	$⊢ (φ \land n \in (0 ..^M)) \to n + M - n = M$
118	117	oveq2d	$⊢ (φ \land n \in (0 ..^M)) \to N + n + (M - n) = N + M$
119	111 112	subcld	$⊢ (φ \land n \in (0 ..^M)) \to M - n \in ℂ$
120	107 112 119	add12d	$⊢ (φ \land n \in (0 ..^M)) \to N + n + (M - n) = n + N + (M - n)$
121	118 120	eqtr3d	$⊢ (φ \land n \in (0 ..^M)) \to N + M = n + N + (M - n)$
122	121	fveq2d	$⊢ (φ \land n \in (0 ..^M)) \to (S D^{n} F) (N + M) = (S D^{n} F) (n + N + (M - n))$
123	105 116 122	3eqtr4d	$⊢ (φ \land n \in (0 ..^M)) \to (S D^{n} (S D^{n} F) (n)) (N + (M - (n + 1)) + 1) = (S D^{n} F) (N + M)$
124	123	dmeqd	$⊢ (φ \land n \in (0 ..^M)) \to dom (S D^{n} (S D^{n} F) (n)) (N + (M - (n + 1)) + 1) = dom (S D^{n} F) (N + M)$
125	98 124	eleqtrrd	$⊢ (φ \land n \in (0 ..^M)) \to B \in dom (S D^{n} (S D^{n} F) (n)) (N + (M - (n + 1)) + 1)$
126	81 84 91 97 125	dvtaylp	$⊢ (φ \land n \in (0 ..^M)) \to ℂ D ((N + (M - (n + 1)) + 1) (S Tayl (S D^{n} F) (n)) B) = (N + M - (n + 1)) (S Tayl {(S D^{n} F) (n)}_{S}^{'}) B$
127	115	oveq1d	$⊢ (φ \land n \in (0 ..^M)) \to (N + (M - (n + 1)) + 1) (S Tayl (S D^{n} F) (n)) B = (N + M - n) (S Tayl (S D^{n} F) (n)) B$
128	127	oveq2d	$⊢ (φ \land n \in (0 ..^M)) \to ℂ D ((N + (M - (n + 1)) + 1) (S Tayl (S D^{n} F) (n)) B) = ℂ D ((N + M - n) (S Tayl (S D^{n} F) (n)) B)$
129	59	adantr	$⊢ (φ \land n \in (0 ..^M)) \to S \subseteq ℂ$
130		dvnp1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land n \in ℕ_{0}) \to (S D^{n} F) (n + 1) = S D (S D^{n} F) (n)$
131	129 82 78 130	syl3anc	$⊢ (φ \land n \in (0 ..^M)) \to (S D^{n} F) (n + 1) = S D (S D^{n} F) (n)$
132	131	oveq2d	$⊢ (φ \land n \in (0 ..^M)) \to S Tayl (S D^{n} F) (n + 1) = S Tayl {(S D^{n} F) (n)}_{S}^{'}$
133	132	eqcomd	$⊢ (φ \land n \in (0 ..^M)) \to S Tayl {(S D^{n} F) (n)}_{S}^{'} = S Tayl (S D^{n} F) (n + 1)$
134	133	oveqd	$⊢ (φ \land n \in (0 ..^M)) \to (N + M - (n + 1)) (S Tayl {(S D^{n} F) (n)}_{S}^{'}) B = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B$
135	126 128 134	3eqtr3rd	$⊢ (φ \land n \in (0 ..^M)) \to (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B = ℂ D ((N + M - n) (S Tayl (S D^{n} F) (n)) B)$
136	80 135	eqeq12d	$⊢ (φ \land n \in (0 ..^M)) \to ((ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B \leftrightarrow ℂ D (ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = ℂ D ((N + M - n) (S Tayl (S D^{n} F) (n)) B))$
137	73 136	imbitrrid	$⊢ (φ \land n \in (0 ..^M)) \to ((ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = (N + M - n) (S Tayl (S D^{n} F) (n)) B \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B)$
138	137	expcom	$⊢ n \in (0 ..^M) \to (φ \to ((ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = (N + M - n) (S Tayl (S D^{n} F) (n)) B \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B))$
139	138	a2d	$⊢ n \in (0 ..^M) \to ((φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n) = (N + M - n) (S Tayl (S D^{n} F) (n)) B) \to (φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (n + 1) = (N + M - (n + 1)) (S Tayl (S D^{n} F) (n + 1)) B))$
140	19 28 37 46 72 139	fzind2	$⊢ M \in (0 \dots M) \to (φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (M) = (N + M - M) (S Tayl (S D^{n} F) (M)) B)$
141	10 140	mpcom	$⊢ φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (M) = (N + M - M) (S Tayl (S D^{n} F) (M)) B$
142	66	subidd	$⊢ φ \to M - M = 0$
143	142	oveq2d	$⊢ φ \to N + M - M = N + 0$
144	106	addridd	$⊢ φ \to N + 0 = N$
145	143 144	eqtrd	$⊢ φ \to N + M - M = N$
146	145	oveq1d	$⊢ φ \to (N + M - M) (S Tayl (S D^{n} F) (M)) B = N (S Tayl (S D^{n} F) (M)) B$
147	141 146	eqtrd	$⊢ φ \to (ℂ D^{n} ((N + M) (S Tayl F) B)) (M) = N (S Tayl (S D^{n} F) (M)) B$

Metamath Proof Explorer

Theorem dvntaylp

Proof