taylplem2

Description: Lemma for taylpfval and similar theorems. (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)$
Assertion	taylplem2	$⊢ ((φ \land X \in ℂ) \land k \in (0 \dots N)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k} \in ℂ$

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		0z	$⊢ 0 \in ℤ$
7	4	nn0zd	$⊢ φ \to N \in ℤ$
8		fzval2	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 \dots N) = [0, N] \cap ℤ$
9	6 7 8	sylancr	$⊢ φ \to (0 \dots N) = [0, N] \cap ℤ$
10	9	eleq2d	$⊢ φ \to (k \in (0 \dots N) \leftrightarrow k \in ([0, N] \cap ℤ))$
11	10	adantr	$⊢ (φ \land X \in ℂ) \to (k \in (0 \dots N) \leftrightarrow k \in ([0, N] \cap ℤ))$
12	11	biimpa	$⊢ ((φ \land X \in ℂ) \land k \in (0 \dots N)) \to k \in ([0, N] \cap ℤ)$
13	4	orcd	$⊢ φ \to (N \in ℕ_{0} \lor N = +∞)$
14	1 2 3 4 5	taylplem1	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
15	1 2 3 13 14	taylfvallem1	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k} \in ℂ$
16	12 15	syldan	$⊢ ((φ \land X \in ℂ) \land k \in (0 \dots N)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k} \in ℂ$

Metamath Proof Explorer