taylf

Description: The Taylor series defines a function on a subset of the complex numbers. (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	taylf	$⊢ φ \to T : dom T ⟶ ℂ$

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	1 2 3 4 5 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})))$
8		simpr	$⊢ (φ \land x \in ℂ) \to x \in ℂ$
9	8	snssd	$⊢ (φ \land x \in ℂ) \to \{x\} \subseteq ℂ$
10	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 ℂ$
11		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 ℂ$
12	9 10 11	syl2anc	$⊢ (φ \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 ℂ$
13	12	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 ℂ$
14		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 ℂ$
15	13 14	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 ℂ$
16	7 15	eqsstrd	$⊢ φ \to T \subseteq ℂ \times ℂ$
17		relxp	$⊢ Rel (ℂ \times ℂ)$
18		relss	$⊢ T \subseteq ℂ \times ℂ \to (Rel (ℂ \times ℂ) \to Rel T)$
19	16 17 18	mpisyl	$⊢ φ \to Rel T$
20	1 2 3 4 5 6	eltayl	$⊢ φ \to (x T y \leftrightarrow (x \in ℂ \land y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))))$
21	20	biimpd	$⊢ φ \to (x T y \to (x \in ℂ \land y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))))$
22	21	alrimiv	$⊢ φ \to \forall y (x T y \to (x \in ℂ \land y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))))$
23		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
24		cnring	$⊢ ℂ_{fld} \in Ring$
25		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
26	24 25	mp1i	$⊢ (φ \land x \in ℂ) \to ℂ_{fld} \in CMnd$
27		cnfldtps	$⊢ ℂ_{fld} \in TopSp$
28	27	a1i	$⊢ (φ \land x \in ℂ) \to ℂ_{fld} \in TopSp$
29		ovex	$⊢ [0, N] \in V$
30	29	inex1	$⊢ [0, N] \cap ℤ \in V$
31	30	a1i	$⊢ (φ \land x \in ℂ) \to [0, N] \cap ℤ \in V$
32	1 2 3 4 5	taylfvallem1	$⊢ ((φ \land x \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} \in ℂ$
33	32	fmpttd	$⊢ (φ \land x \in ℂ) \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) : [0, N] \cap ℤ ⟶ ℂ$
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	23 26 28 31 33 34 36	haustsms	$⊢ (φ \land x \in ℂ) \to \exists^{*} y y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))$
38	37	ex	$⊢ φ \to (x \in ℂ \to \exists^{*} y y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))$
39		moanimv	$⊢ \exists^{} y (x \in ℂ \land y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \leftrightarrow (x \in ℂ \to \exists^{} y y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))$
40	38 39	sylibr	$⊢ φ \to \exists^{*} y (x \in ℂ \land y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))$
41		moim	$⊢ \forall y (x T y \to (x \in ℂ \land y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})))) \to (\exists^{} y (x \in ℂ \land y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \to \exists^{} y x T y)$
42	22 40 41	sylc	$⊢ φ \to \exists^{*} y x T y$
43	42	alrimiv	$⊢ φ \to \forall x \exists^{*} y x T y$
44		dffun6	$⊢ Fun T \leftrightarrow (Rel T \land \forall x \exists^{*} y x T y)$
45	19 43 44	sylanbrc	$⊢ φ \to Fun T$
46	45	funfnd	$⊢ φ \to T Fn dom T$
47		rnss	$⊢ T \subseteq ℂ \times ℂ \to ran T \subseteq ran (ℂ \times ℂ)$
48	16 47	syl	$⊢ φ \to ran T \subseteq ran (ℂ \times ℂ)$
49		rnxpss	$⊢ ran (ℂ \times ℂ) \subseteq ℂ$
50	48 49	sstrdi	$⊢ φ \to ran T \subseteq ℂ$
51		df-f	$⊢ T : dom T ⟶ ℂ \leftrightarrow (T Fn dom T \land ran T \subseteq ℂ)$
52	46 50 51	sylanbrc	$⊢ φ \to T : dom T ⟶ ℂ$

Metamath Proof Explorer

Theorem taylf

Proof