taylfval

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 .

This "extended" version of taylpfval additionally handles the case N = +oo , in which case this is not a polynomial but an infinite series, the Taylor series of the function. (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypotheses	taylfval.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	taylfval.f	$⊢ φ \to F : A ⟶ ℂ$
	taylfval.a	$⊢ φ \to A \subseteq S$
	taylfval.n	$⊢ φ \to (N \in ℕ_{0} \lor N = +∞)$
	taylfval.b	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
	taylfval.t	$⊢ T = N (S Tayl F) B$
Assertion	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})))$

Proof

Step	Hyp	Ref	Expression
1		taylfval.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		taylfval.f	$⊢ φ \to F : A ⟶ ℂ$
3		taylfval.a	$⊢ φ \to A \subseteq S$
4		taylfval.n	$⊢ φ \to (N \in ℕ_{0} \lor N = +∞)$
5		taylfval.b	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
6		taylfval.t	$⊢ T = N (S Tayl F) B$
7		df-tayl	$⊢ Tayl = (s \in \{ℝ, ℂ\}, f \in (ℂ ↑_{𝑝𝑚} s) ⟼ (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (s D^{n} f) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k})))))$
8	7	a1i	$⊢ φ \to Tayl = (s \in \{ℝ, ℂ\}, f \in (ℂ ↑_{𝑝𝑚} s) ⟼ (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (s D^{n} f) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k})))))$
9		eqidd	$⊢ (φ \land (s = S \land f = F)) \to ℕ_{0} \cup \{+∞\} = ℕ_{0} \cup \{+∞\}$
10		oveq12	$⊢ (s = S \land f = F) \to s D^{n} f = S D^{n} F$
11	10	ad2antlr	$⊢ ((φ \land (s = S \land f = F)) \land k \in ([0, n] \cap ℤ)) \to s D^{n} f = S D^{n} F$
12	11	fveq1d	$⊢ ((φ \land (s = S \land f = F)) \land k \in ([0, n] \cap ℤ)) \to (s D^{n} f) (k) = (S D^{n} F) (k)$
13	12	dmeqd	$⊢ ((φ \land (s = S \land f = F)) \land k \in ([0, n] \cap ℤ)) \to dom (s D^{n} f) (k) = dom (S D^{n} F) (k)$
14	13	iineq2dv	$⊢ (φ \land (s = S \land f = F)) \to ⋂_{k \in [0, n] \cap ℤ} dom (s D^{n} f) (k) = ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k)$
15	12	fveq1d	$⊢ ((φ \land (s = S \land f = F)) \land k \in ([0, n] \cap ℤ)) \to (s D^{n} f) (k) (a) = (S D^{n} F) (k) (a)$
16	15	oveq1d	$⊢ ((φ \land (s = S \land f = F)) \land k \in ([0, n] \cap ℤ)) \to \frac{(s D^{n} f) (k) (a)}{k!} = \frac{(S D^{n} F) (k) (a)}{k!}$
17	16	oveq1d	$⊢ ((φ \land (s = S \land f = F)) \land k \in ([0, n] \cap ℤ)) \to (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k} = (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}$
18	17	mpteq2dva	$⊢ (φ \land (s = S \land f = F)) \to (k \in ([0, n] \cap ℤ) ⟼ (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k}) = (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})$
19	18	oveq2d	$⊢ (φ \land (s = S \land f = F)) \to ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k}) = ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})$
20	19	xpeq2d	$⊢ (φ \land (s = S \land f = F)) \to \{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k})) = \{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}))$
21	20	iuneq2d	$⊢ (φ \land (s = S \land f = F)) \to ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k}))) = ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})))$
22	9 14 21	mpoeq123dv	$⊢ (φ \land (s = S \land f = F)) \to (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (s D^{n} f) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(s D^{n} f) (k) (a)}{k!}) {(x - a)}^{k})))) = (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}))))$
23		simpr	$⊢ (φ \land s = S) \to s = S$
24	23	oveq2d	$⊢ (φ \land s = S) \to ℂ ↑_{𝑝𝑚} s = ℂ ↑_{𝑝𝑚} S$
25		cnex	$⊢ ℂ \in V$
26	25	a1i	$⊢ φ \to ℂ \in V$
27		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
28	26 1 2 3 27	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
29		nn0ex	$⊢ ℕ_{0} \in V$
30		snex	$⊢ \{+∞\} \in V$
31	29 30	unex	$⊢ ℕ_{0} \cup \{+∞\} \in V$
32		0xr	$⊢ 0 \in ℝ^{*}$
33		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
34		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
35	33 34	sstri	$⊢ ℕ_{0} \subseteq ℝ^{*}$
36		pnfxr	$⊢ +∞ \in ℝ^{*}$
37		snssi	$⊢ +∞ \in ℝ^{} \to \{+∞\} \subseteq ℝ^{}$
38	36 37	ax-mp	$⊢ \{+∞\} \subseteq ℝ^{*}$
39	35 38	unssi	$⊢ ℕ_{0} \cup \{+∞\} \subseteq ℝ^{*}$
40	39	sseli	$⊢ n \in (ℕ_{0} \cup \{+∞\}) \to n \in ℝ^{*}$
41		elun	$⊢ n \in (ℕ_{0} \cup \{+∞\}) \leftrightarrow (n \in ℕ_{0} \lor n \in \{+∞\})$
42		nn0ge0	$⊢ n \in ℕ_{0} \to 0 \leq n$
43		0lepnf	$⊢ 0 \leq +∞$
44		elsni	$⊢ n \in \{+∞\} \to n = +∞$
45	43 44	breqtrrid	$⊢ n \in \{+∞\} \to 0 \leq n$
46	42 45	jaoi	$⊢ (n \in ℕ_{0} \lor n \in \{+∞\}) \to 0 \leq n$
47	41 46	sylbi	$⊢ n \in (ℕ_{0} \cup \{+∞\}) \to 0 \leq n$
48		lbicc2	$⊢ (0 \in ℝ^{} \land n \in ℝ^{} \land 0 \leq n) \to 0 \in [0, n]$
49	32 40 47 48	mp3an2i	$⊢ n \in (ℕ_{0} \cup \{+∞\}) \to 0 \in [0, n]$
50		0z	$⊢ 0 \in ℤ$
51		inelcm	$⊢ (0 \in [0, n] \land 0 \in ℤ) \to [0, n] \cap ℤ \neq \emptyset$
52	49 50 51	sylancl	$⊢ n \in (ℕ_{0} \cup \{+∞\}) \to [0, n] \cap ℤ \neq \emptyset$
53		fvex	$⊢ (S D^{n} F) (k) \in V$
54	53	dmex	$⊢ dom (S D^{n} F) (k) \in V$
55	54	rgenw	$⊢ \forall k \in ([0, n] \cap ℤ) dom (S D^{n} F) (k) \in V$
56		iinexg	$⊢ ([0, n] \cap ℤ \neq \emptyset \land \forall k \in ([0, n] \cap ℤ) dom (S D^{n} F) (k) \in V) \to ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) \in V$
57	52 55 56	sylancl	$⊢ n \in (ℕ_{0} \cup \{+∞\}) \to ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) \in V$
58	57	rgen	$⊢ \forall n \in (ℕ_{0} \cup \{+∞\}) ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) \in V$
59		eqid	$⊢ (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})))) = (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}))))$
60	59	mpoexxg	$⊢ (ℕ_{0} \cup \{+∞\} \in V \land \forall n \in (ℕ_{0} \cup \{+∞\}) ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) \in V) \to (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})))) \in V$
61	31 58 60	mp2an	$⊢ (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})))) \in V$
62	61	a1i	$⊢ φ \to (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})))) \in V$
63	8 22 24 1 28 62	ovmpodx	$⊢ φ \to S Tayl F = (n \in (ℕ_{0} \cup \{+∞\}), a \in ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) ⟼ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}))))$
64		simprl	$⊢ (φ \land (n = N \land a = B)) \to n = N$
65	64	oveq2d	$⊢ (φ \land (n = N \land a = B)) \to [0, n] = [0, N]$
66	65	ineq1d	$⊢ (φ \land (n = N \land a = B)) \to [0, n] \cap ℤ = [0, N] \cap ℤ$
67		simprr	$⊢ (φ \land (n = N \land a = B)) \to a = B$
68	67	fveq2d	$⊢ (φ \land (n = N \land a = B)) \to (S D^{n} F) (k) (a) = (S D^{n} F) (k) (B)$
69	68	oveq1d	$⊢ (φ \land (n = N \land a = B)) \to \frac{(S D^{n} F) (k) (a)}{k!} = \frac{(S D^{n} F) (k) (B)}{k!}$
70	67	oveq2d	$⊢ (φ \land (n = N \land a = B)) \to x - a = x - B$
71	70	oveq1d	$⊢ (φ \land (n = N \land a = B)) \to {(x - a)}^{k} = {(x - B)}^{k}$
72	69 71	oveq12d	$⊢ (φ \land (n = N \land a = B)) \to (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k} = (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}$
73	66 72	mpteq12dv	$⊢ (φ \land (n = N \land a = B)) \to (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}) = (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$
74	73	oveq2d	$⊢ (φ \land (n = N \land a = B)) \to ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}) = ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$
75	74	xpeq2d	$⊢ (φ \land (n = N \land a = B)) \to \{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k})) = \{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))$
76	75	iuneq2d	$⊢ (φ \land (n = N \land a = B)) \to ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, n] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (a)}{k!}) {(x - a)}^{k}))) = ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))$
77		simpr	$⊢ (φ \land n = N) \to n = N$
78	77	oveq2d	$⊢ (φ \land n = N) \to [0, n] = [0, N]$
79	78	ineq1d	$⊢ (φ \land n = N) \to [0, n] \cap ℤ = [0, N] \cap ℤ$
80		iineq1	$⊢ [0, n] \cap ℤ = [0, N] \cap ℤ \to ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) = ⋂_{k \in [0, N] \cap ℤ} dom (S D^{n} F) (k)$
81	79 80	syl	$⊢ (φ \land n = N) \to ⋂_{k \in [0, n] \cap ℤ} dom (S D^{n} F) (k) = ⋂_{k \in [0, N] \cap ℤ} dom (S D^{n} F) (k)$
82		pnfex	$⊢ +∞ \in V$
83	82	elsn2	$⊢ N \in \{+∞\} \leftrightarrow N = +∞$
84	83	orbi2i	$⊢ (N \in ℕ_{0} \lor N \in \{+∞\}) \leftrightarrow (N \in ℕ_{0} \lor N = +∞)$
85	4 84	sylibr	$⊢ φ \to (N \in ℕ_{0} \lor N \in \{+∞\})$
86		elun	$⊢ N \in (ℕ_{0} \cup \{+∞\}) \leftrightarrow (N \in ℕ_{0} \lor N \in \{+∞\})$
87	85 86	sylibr	$⊢ φ \to N \in (ℕ_{0} \cup \{+∞\})$
88	5	ralrimiva	$⊢ φ \to \forall k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k)$
89		oveq2	$⊢ n = N \to [0, n] = [0, N]$
90	89	ineq1d	$⊢ n = N \to [0, n] \cap ℤ = [0, N] \cap ℤ$
91	90	neeq1d	$⊢ n = N \to ([0, n] \cap ℤ \neq \emptyset \leftrightarrow [0, N] \cap ℤ \neq \emptyset)$
92	91 52	vtoclga	$⊢ N \in (ℕ_{0} \cup \{+∞\}) \to [0, N] \cap ℤ \neq \emptyset$
93	87 92	syl	$⊢ φ \to [0, N] \cap ℤ \neq \emptyset$
94		r19.2z	$⊢ ([0, N] \cap ℤ \neq \emptyset \land \forall k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k)) \to \exists k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k)$
95	93 88 94	syl2anc	$⊢ φ \to \exists k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k)$
96		elex	$⊢ B \in dom (S D^{n} F) (k) \to B \in V$
97	96	rexlimivw	$⊢ \exists k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k) \to B \in V$
98		eliin	$⊢ B \in V \to (B \in ⋂_{k \in [0, N] \cap ℤ} dom (S D^{n} F) (k) \leftrightarrow \forall k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k))$
99	95 97 98	3syl	$⊢ φ \to (B \in ⋂_{k \in [0, N] \cap ℤ} dom (S D^{n} F) (k) \leftrightarrow \forall k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k))$
100	88 99	mpbird	$⊢ φ \to B \in ⋂_{k \in [0, N] \cap ℤ} dom (S D^{n} F) (k)$
101		snssi	$⊢ x \in ℂ \to \{x\} \subseteq ℂ$
102	1 2 3 4 5	taylfvallem	$⊢ (φ \land x \in ℂ) \to ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) \subseteq ℂ$
103		xpss12	$⊢ (\{x\} \subseteq ℂ \land ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) \subseteq ℂ) \to \{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})) \subseteq ℂ \times ℂ$
104	101 102 103	syl2an2	$⊢ (φ \land x \in ℂ) \to \{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})) \subseteq ℂ \times ℂ$
105	104	ralrimiva	$⊢ φ \to \forall x \in ℂ \{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})) \subseteq ℂ \times ℂ$
106		iunss	$⊢ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \subseteq ℂ \times ℂ \leftrightarrow \forall x \in ℂ \{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})) \subseteq ℂ \times ℂ$
107	105 106	sylibr	$⊢ φ \to ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \subseteq ℂ \times ℂ$
108	25 25	xpex	$⊢ ℂ \times ℂ \in V$
109	108	ssex	$⊢ ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \subseteq ℂ \times ℂ \to ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \in V$
110	107 109	syl	$⊢ φ \to ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \in V$
111	63 76 81 87 100 110	ovmpodx	$⊢ φ \to N (S Tayl F) B = ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))$
112	6 111	eqtrid	$⊢ φ \to T = ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))$

Metamath Proof Explorer

Theorem taylfval

Proof