taylpfval

Description: Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: S is the base set with respect to evaluate the derivatives (generally RR or CC ), F is the function we are approximating, at point B , to order N . The result is a polynomial function of x . (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	taylpfval	$⊢ φ \to T = (x \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$

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	4	orcd	$⊢ φ \to (N \in ℕ_{0} \lor N = +∞)$
8	1 2 3 4 5	taylplem1	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
9	1 2 3 7 8 6	taylfval	$⊢ φ \to T = ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))$
10		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
11		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
12		cnring	$⊢ ℂ_{fld} \in Ring$
13		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
14	12 13	mp1i	$⊢ (φ \land x \in ℂ) \to ℂ_{fld} \in CMnd$
15		cnfldtps	$⊢ ℂ_{fld} \in TopSp$
16	15	a1i	$⊢ (φ \land x \in ℂ) \to ℂ_{fld} \in TopSp$
17		ovex	$⊢ [0, N] \in V$
18	17	inex1	$⊢ [0, N] \cap ℤ \in V$
19	18	a1i	$⊢ (φ \land x \in ℂ) \to [0, N] \cap ℤ \in V$
20	1 2 3 7 8	taylfvallem1	$⊢ ((φ \land x \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} \in ℂ$
21	20	fmpttd	$⊢ (φ \land x \in ℂ) \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) : [0, N] \cap ℤ ⟶ ℂ$
22		eqid	$⊢ (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) = (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$
23		0z	$⊢ 0 \in ℤ$
24	4	nn0zd	$⊢ φ \to N \in ℤ$
25		fzval2	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 \dots N) = [0, N] \cap ℤ$
26	23 24 25	sylancr	$⊢ φ \to (0 \dots N) = [0, N] \cap ℤ$
27	26	adantr	$⊢ (φ \land x \in ℂ) \to (0 \dots N) = [0, N] \cap ℤ$
28		fzfid	$⊢ (φ \land x \in ℂ) \to (0 \dots N) \in Fin$
29	27 28	eqeltrrd	$⊢ (φ \land x \in ℂ) \to [0, N] \cap ℤ \in Fin$
30		ovexd	$⊢ ((φ \land x \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} \in V$
31		c0ex	$⊢ 0 \in V$
32	31	a1i	$⊢ (φ \land x \in ℂ) \to 0 \in V$
33	22 29 30 32	fsuppmptdm	$⊢ (φ \land x \in ℂ) \to {finSupp}_{0} ((k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))$
34		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
35	34	cnfldhaus	$⊢ TopOpen (ℂ_{fld}) \in Haus$
36	35	a1i	$⊢ (φ \land x \in ℂ) \to TopOpen (ℂ_{fld}) \in Haus$
37	10 11 14 16 19 21 33 34 36	haustsmsid	$⊢ (φ \land x \in ℂ) \to ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) = \{\underset{k \in [0, N] \cap ℤ}{\sum_{ℂ_{fld}}} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\}$
38	29 20	gsumfsum	$⊢ (φ \land x \in ℂ) \to \underset{k \in [0, N] \cap ℤ}{\sum_{ℂ_{fld}}} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} = \sum_{k \in [0, N] \cap ℤ} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}$
39	27	sumeq1d	$⊢ (φ \land x \in ℂ) \to \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} = \sum_{k \in [0, N] \cap ℤ} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}$
40	38 39	eqtr4d	$⊢ (φ \land x \in ℂ) \to \underset{k \in [0, N] \cap ℤ}{\sum_{ℂ_{fld}}} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} = \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}$
41	40	sneqd	$⊢ (φ \land x \in ℂ) \to \{\underset{k \in [0, N] \cap ℤ}{\sum_{ℂ_{fld}}} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\} = \{\sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\}$
42	37 41	eqtrd	$⊢ (φ \land x \in ℂ) \to ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) = \{\sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\}$
43	42	xpeq2d	$⊢ (φ \land x \in ℂ) \to \{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})) = \{x\} \times \{\sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\}$
44	43	iuneq2dv	$⊢ φ \to ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) = ⋃_{x \in ℂ} (\{x\} \times \{\sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\})$
45	9 44	eqtrd	$⊢ φ \to T = ⋃_{x \in ℂ} (\{x\} \times \{\sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\})$
46		dfmpt3	$⊢ (x \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) = ⋃_{x \in ℂ} (\{x\} \times \{\sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}\})$
47	45 46	eqtr4di	$⊢ φ \to T = (x \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$

Metamath Proof Explorer

Theorem taylpfval

Proof