dvntaylp0

Description: The first N derivatives of the Taylor polynomial at B match the derivatives of the function from which it is derived. (Contributed by Mario Carneiro, 1-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dvntaylp0.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvntaylp0.f	$⊢ φ \to F : A ⟶ ℂ$
3		dvntaylp0.a	$⊢ φ \to A \subseteq S$
4		dvntaylp0.m	$⊢ φ \to M \in (0 \dots N)$
5		dvntaylp0.b	$⊢ φ \to B \in dom (S D^{n} F) (N)$
6		dvntaylp0.t	$⊢ T = N (S Tayl F) B$
7		elfz3nn0	$⊢ M \in (0 \dots N) \to N \in ℕ_{0}$
8	4 7	syl	$⊢ φ \to N \in ℕ_{0}$
9	8	nn0cnd	$⊢ φ \to N \in ℂ$
10		elfznn0	$⊢ M \in (0 \dots N) \to M \in ℕ_{0}$
11	4 10	syl	$⊢ φ \to M \in ℕ_{0}$
12	11	nn0cnd	$⊢ φ \to M \in ℂ$
13	9 12	npcand	$⊢ φ \to N - M + M = N$
14	13	oveq1d	$⊢ φ \to (N - M + M) (S Tayl F) B = N (S Tayl F) B$
15	14 6	eqtr4di	$⊢ φ \to (N - M + M) (S Tayl F) B = T$
16	15	oveq2d	$⊢ φ \to ℂ D^{n} ((N - M + M) (S Tayl F) B) = ℂ D^{n} T$
17	16	fveq1d	$⊢ φ \to (ℂ D^{n} ((N - M + M) (S Tayl F) B)) (M) = (ℂ D^{n} T) (M)$
18		fznn0sub	$⊢ M \in (0 \dots N) \to N - M \in ℕ_{0}$
19	4 18	syl	$⊢ φ \to N - M \in ℕ_{0}$
20	13	fveq2d	$⊢ φ \to (S D^{n} F) (N - M + M) = (S D^{n} F) (N)$
21	20	dmeqd	$⊢ φ \to dom (S D^{n} F) (N - M + M) = dom (S D^{n} F) (N)$
22	5 21	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} F) (N - M + M)$
23	1 2 3 11 19 22	dvntaylp	$⊢ φ \to (ℂ D^{n} ((N - M + M) (S Tayl F) B)) (M) = (N - M) (S Tayl (S D^{n} F) (M)) B$
24	17 23	eqtr3d	$⊢ φ \to (ℂ D^{n} T) (M) = (N - M) (S Tayl (S D^{n} F) (M)) B$
25	24	fveq1d	$⊢ φ \to (ℂ D^{n} T) (M) (B) = ((N - M) (S Tayl (S D^{n} F) (M)) B) (B)$
26		cnex	$⊢ ℂ \in V$
27	26	a1i	$⊢ φ \to ℂ \in V$
28		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
29	27 1 2 3 28	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
30		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in ℕ_{0}) \to (S D^{n} F) (M) : dom (S D^{n} F) (M) ⟶ ℂ$
31	1 29 11 30	syl3anc	$⊢ φ \to (S D^{n} F) (M) : dom (S D^{n} F) (M) ⟶ ℂ$
32		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land M \in ℕ_{0}) \to dom (S D^{n} F) (M) \subseteq dom F$
33	1 29 11 32	syl3anc	$⊢ φ \to dom (S D^{n} F) (M) \subseteq dom F$
34	2 33	fssdmd	$⊢ φ \to dom (S D^{n} F) (M) \subseteq A$
35	34 3	sstrd	$⊢ φ \to dom (S D^{n} F) (M) \subseteq S$
36	19	orcd	$⊢ φ \to (N - M \in ℕ_{0} \lor N - M = +∞)$
37		dvnadd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (M \in ℕ_{0} \land N - M \in ℕ_{0})) \to (S D^{n} (S D^{n} F) (M)) (N - M) = (S D^{n} F) (M + N - M)$
38	1 29 11 19 37	syl22anc	$⊢ φ \to (S D^{n} (S D^{n} F) (M)) (N - M) = (S D^{n} F) (M + N - M)$
39	12 9	pncan3d	$⊢ φ \to M + N - M = N$
40	39	fveq2d	$⊢ φ \to (S D^{n} F) (M + N - M) = (S D^{n} F) (N)$
41	38 40	eqtrd	$⊢ φ \to (S D^{n} (S D^{n} F) (M)) (N - M) = (S D^{n} F) (N)$
42	41	dmeqd	$⊢ φ \to dom (S D^{n} (S D^{n} F) (M)) (N - M) = dom (S D^{n} F) (N)$
43	5 42	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} (S D^{n} F) (M)) (N - M)$
44	1 31 35 19 43	taylplem1	$⊢ (φ \land k \in ([0, N - M] \cap ℤ)) \to B \in dom (S D^{n} (S D^{n} F) (M)) (k)$
45		eqid	$⊢ (N - M) (S Tayl (S D^{n} F) (M)) B = (N - M) (S Tayl (S D^{n} F) (M)) B$
46	1 31 35 36 44 45	tayl0	$⊢ φ \to (B \in dom ((N - M) (S Tayl (S D^{n} F) (M)) B) \land ((N - M) (S Tayl (S D^{n} F) (M)) B) (B) = (S D^{n} F) (M) (B))$
47	46	simprd	$⊢ φ \to ((N - M) (S Tayl (S D^{n} F) (M)) B) (B) = (S D^{n} F) (M) (B)$
48	25 47	eqtrd	$⊢ φ \to (ℂ D^{n} T) (M) (B) = (S D^{n} F) (M) (B)$

Metamath Proof Explorer

Theorem dvntaylp0

Proof