taylplem1

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	taylplem1	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$

Proof

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	biimpar	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k \in (0 \dots N)$
12		cnex	$⊢ ℂ \in V$
13	12	a1i	$⊢ φ \to ℂ \in V$
14		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
15	13 1 2 3 14	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
16	1 15	jca	$⊢ φ \to (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S))$
17		dvn2bss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
18	17	3expa	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
19	16 18	sylan	$⊢ (φ \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
20	5	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (N)$
21	19 20	sseldd	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (k)$
22	11 21	syldan	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$

Metamath Proof Explorer

Theorem taylplem1

Proof