taylfvallem

	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)$
Assertion	taylfvallem	$⊢ (φ \land X \in ℂ) \to ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k}) \subseteq ℂ$

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		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
7		cnring	$⊢ ℂ_{fld} \in Ring$
8		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
9	7 8	mp1i	$⊢ (φ \land X \in ℂ) \to ℂ_{fld} \in CMnd$
10		cnfldtps	$⊢ ℂ_{fld} \in TopSp$
11	10	a1i	$⊢ (φ \land X \in ℂ) \to ℂ_{fld} \in TopSp$
12		ovex	$⊢ [0, N] \in V$
13	12	inex1	$⊢ [0, N] \cap ℤ \in V$
14	13	a1i	$⊢ (φ \land X \in ℂ) \to [0, N] \cap ℤ \in V$
15	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 ℂ$
16	15	fmpttd	$⊢ (φ \land X \in ℂ) \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k}) : [0, N] \cap ℤ ⟶ ℂ$
17	6 9 11 14 16	tsmscl	$⊢ (φ \land X \in ℂ) \to ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k}) \subseteq ℂ$

Metamath Proof Explorer