Metamath Proof Explorer

Theorem eltayl

Description: Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (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	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}))))$

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	7	eleq2d	$⊢ φ \to (⟨X, Y⟩ \in T \leftrightarrow ⟨X, Y⟩ \in ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))))$
9		df-br	$⊢ X T Y \leftrightarrow ⟨X, Y⟩ \in T$
10	9	bicomi	$⊢ ⟨X, Y⟩ \in T \leftrightarrow X T Y$
11		oveq1	$⊢ x = X \to x - B = X - B$
12	11	oveq1d	$⊢ x = X \to {(x - B)}^{k} = {(X - B)}^{k}$
13	12	oveq2d	$⊢ x = X \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k} = (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k}$
14	13	mpteq2dv	$⊢ x = X \to (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})$
15	14	oveq2d	$⊢ x = X \to ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}) = ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k})$
16	15	opeliunxp2	$⊢ ⟨X, Y⟩ \in ⋃_{x \in ℂ} (\{x\} \times (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}))) \leftrightarrow (X \in ℂ \land Y \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k})))$
17	8 10 16	3bitr3g	$⊢ φ \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}))))$