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	$⊢ φ \to S \in \{ℝ, ℂ\}$
	taylpfval.f	$⊢ φ \to F : A ⟶ ℂ$
	taylpfval.a	$⊢ φ \to A \subseteq S$
	taylpfval.n	$⊢ φ \to N \in ℕ_{0}$
	taylpfval.b	$⊢ φ \to B \in dom (S D^{n} F) (N)$
	taylpfval.t	$⊢ T = N (S Tayl F) B$
Assertion	taylply	$⊢ φ \to (T \in Poly (ℂ) \land \deg (T) \leq N)$

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		taylpfval.f	$⊢ φ \to F : A ⟶ ℂ$
3		taylpfval.a	$⊢ φ \to A \subseteq S$
4		taylpfval.n	$⊢ φ \to N \in ℕ_{0}$
5		taylpfval.b	$⊢ φ \to B \in dom (S D^{n} F) (N)$
6		taylpfval.t	$⊢ T = N (S Tayl F) B$
7		cnring	$⊢ ℂ_{fld} \in Ring$
8		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
9	8	subrgid	$⊢ ℂ_{fld} \in Ring \to ℂ \in SubRing (ℂ_{fld})$
10	7 9	mp1i	$⊢ φ \to ℂ \in SubRing (ℂ_{fld})$
11		cnex	$⊢ ℂ \in V$
12	11	a1i	$⊢ φ \to ℂ \in V$
13		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
14	12 1 2 3 13	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
15		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to dom (S D^{n} F) (N) \subseteq dom F$
16	1 14 4 15	syl3anc	$⊢ φ \to dom (S D^{n} F) (N) \subseteq dom F$
17	2 16	fssdmd	$⊢ φ \to dom (S D^{n} F) (N) \subseteq A$
18		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
19	1 18	syl	$⊢ φ \to S \subseteq ℂ$
20	3 19	sstrd	$⊢ φ \to A \subseteq ℂ$
21	17 20	sstrd	$⊢ φ \to dom (S D^{n} F) (N) \subseteq ℂ$
22	21 5	sseldd	$⊢ φ \to B \in ℂ$
23	1	adantr	$⊢ (φ \land k \in (0 \dots N)) \to S \in \{ℝ, ℂ\}$
24	14	adantr	$⊢ (φ \land k \in (0 \dots N)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
25		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
26	25	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
27		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
28	23 24 26 27	syl3anc	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
29		simpr	$⊢ (φ \land k \in (0 \dots N)) \to k \in (0 \dots N)$
30		dvn2bss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
31	23 24 29 30	syl3anc	$⊢ (φ \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
32	5	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (N)$
33	31 32	sseldd	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (k)$
34	28 33	ffvelrnd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) (B) \in ℂ$
35	26	faccld	$⊢ (φ \land k \in (0 \dots N)) \to k! \in ℕ$
36	35	nncnd	$⊢ (φ \land k \in (0 \dots N)) \to k! \in ℂ$
37	35	nnne0d	$⊢ (φ \land k \in (0 \dots N)) \to k! \neq 0$
38	34 36 37	divcld	$⊢ (φ \land k \in (0 \dots N)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
39	1 2 3 4 5 6 10 22 38	taylply2	$⊢ φ \to (T \in Poly (ℂ) \land \deg (T) \leq N)$

Metamath Proof Explorer

Theorem taylply

Proof