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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvntaylp0.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	dvntaylp0.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	dvntaylp0.m	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) )
	dvntaylp0.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
	dvntaylp0.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion	dvntaylp0	⊢ ( 𝜑 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ 𝑀 ) ‘ 𝐵 ) = ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dvntaylp0.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvntaylp0.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		dvntaylp0.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		dvntaylp0.m	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) )
5		dvntaylp0.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
6		dvntaylp0.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7		elfz3nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ₀ )
8	4 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
9	8	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10		elfznn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ₀ )
11	4 10	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
12	11	nn0cnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
13	9 12	npcand	⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 )
14	13	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 ) )
15	14 6	eqtr4di	⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) = 𝑇 )
16	15	oveq2d	⊢ ( 𝜑 → ( ℂ D^𝑛 ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) = ( ℂ D^𝑛 𝑇 ) )
17	16	fveq1d	⊢ ( 𝜑 → ( ( ℂ D^𝑛 ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( ℂ D^𝑛 𝑇 ) ‘ 𝑀 ) )
18		fznn0sub	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ₀ )
19	4 18	syl	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ₀ )
20	13	fveq2d	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
21	20	dmeqd	⊢ ( 𝜑 → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
22	5 21	eleqtrrd	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) )
23	1 2 3 11 19 22	dvntaylp	⊢ ( 𝜑 → ( ( ℂ D^𝑛 ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )
24	17 23	eqtr3d	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ 𝑀 ) = ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )
25	24	fveq1d	⊢ ( 𝜑 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ 𝑀 ) ‘ 𝐵 ) = ( ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ‘ 𝐵 ) )
26		cnex	⊢ ℂ ∈ V
27	26	a1i	⊢ ( 𝜑 → ℂ ∈ V )
28		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
29	27 1 2 3 28	syl22anc	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
30		dvnf	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⟶ ℂ )
31	1 29 11 30	syl3anc	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⟶ ℂ )
32		dvnbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ℕ₀ ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ dom 𝐹 )
33	1 29 11 32	syl3anc	⊢ ( 𝜑 → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ dom 𝐹 )
34	2 33	fssdmd	⊢ ( 𝜑 → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ 𝐴 )
35	34 3	sstrd	⊢ ( 𝜑 → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ 𝑆 )
36	19	orcd	⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) ∈ ℕ₀ ∨ ( 𝑁 − 𝑀 ) = +∞ ) )
37		dvnadd	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑀 ∈ ℕ₀ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ₀ ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
38	1 29 11 19 37	syl22anc	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
39	12 9	pncan3d	⊢ ( 𝜑 → ( 𝑀 + ( 𝑁 − 𝑀 ) ) = 𝑁 )
40	39	fveq2d	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
41	38 40	eqtrd	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
42	41	dmeqd	⊢ ( 𝜑 → dom ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
43	5 42	eleqtrrd	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) )
44	1 31 35 19 43	taylplem1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] ( 𝑁 − 𝑀 ) ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) )
45		eqid	⊢ ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) = ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 )
46	1 31 35 36 44 45	tayl0	⊢ ( 𝜑 → ( 𝐵 ∈ dom ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ∧ ( ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ‘ 𝐵 ) = ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) ) )
47	46	simprd	⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑀 ) ( 𝑆 Tayl ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ‘ 𝐵 ) = ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) )
48	25 47	eqtrd	⊢ ( 𝜑 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ 𝑀 ) ‘ 𝐵 ) = ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem dvntaylp0

Proof