Theorem taylply

Description: The Taylor polynomial is a polynomial of degree (at most) N . (Contributed by Mario Carneiro, 31-Dec-2016)

	Ref	Expression
Hypotheses	taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
	taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion	taylply	⊢ ( 𝜑 → ( 𝑇 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑇 ) ≤ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
6		taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7		cnring	⊢ ℂfld ∈ Ring
8		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
9	8	subrgid	⊢ ( ℂfld ∈ Ring → ℂ ∈ ( SubRing ‘ ℂfld ) )
10	7 9	mp1i	⊢ ( 𝜑 → ℂ ∈ ( SubRing ‘ ℂfld ) )
11		cnex	⊢ ℂ ∈ V
12	11	a1i	⊢ ( 𝜑 → ℂ ∈ V )
13		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
14	12 1 2 3 13	syl22anc	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
15		dvnbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )
16	1 14 4 15	syl3anc	⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )
17	2 16	fssdmd	⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ 𝐴 )
18		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
19	1 18	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
20	3 19	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
21	17 20	sstrd	⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ ℂ )
22	21 5	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
23	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
24	14	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
25		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
26	25	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
27		dvnf	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
28	23 24 26 27	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
29		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
30		dvn2bss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
31	23 24 29 30	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
32	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
33	31 32	sseldd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
34	28 33	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℂ )
35	26	faccld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
36	35	nncnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
37	35	nnne0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
38	34 36 37	divcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
39	1 2 3 4 5 6 10 22 38	taylply2	⊢ ( 𝜑 → ( 𝑇 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑇 ) ≤ 𝑁 ) )