taylfvallem1

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

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	1	ad2antrr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to S \in \{ℝ, ℂ\}$
7		cnex	$⊢ ℂ \in V$
8	7	a1i	$⊢ φ \to ℂ \in V$
9		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
10	8 1 2 3 9	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
11	10	ad2antrr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
12		simpr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to k \in ([0, N] \cap ℤ)$
13	12	elin2d	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to k \in ℤ$
14	12	elin1d	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to k \in [0, N]$
15		0xr	$⊢ 0 \in ℝ^{*}$
16		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
17	16	rexrd	$⊢ N \in ℕ_{0} \to N \in ℝ^{*}$
18		id	$⊢ N = +∞ \to N = +∞$
19		pnfxr	$⊢ +∞ \in ℝ^{*}$
20	18 19	eqeltrdi	$⊢ N = +∞ \to N \in ℝ^{*}$
21	17 20	jaoi	$⊢ (N \in ℕ_{0} \lor N = +∞) \to N \in ℝ^{*}$
22	4 21	syl	$⊢ φ \to N \in ℝ^{*}$
23	22	ad2antrr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to N \in ℝ^{*}$
24		elicc1	$⊢ (0 \in ℝ^{} \land N \in ℝ^{}) \to (k \in [0, N] \leftrightarrow (k \in ℝ^{*} \land 0 \leq k \land k \leq N))$
25	15 23 24	sylancr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (k \in [0, N] \leftrightarrow (k \in ℝ^{*} \land 0 \leq k \land k \leq N))$
26	14 25	mpbid	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (k \in ℝ^{*} \land 0 \leq k \land k \leq N)$
27	26	simp2d	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to 0 \leq k$
28		elnn0z	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℤ \land 0 \leq k)$
29	13 27 28	sylanbrc	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to k \in ℕ_{0}$
30		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
31	6 11 29 30	syl3anc	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
32	5	adantlr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
33	31 32	ffvelcdmd	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (S D^{n} F) (k) (B) \in ℂ$
34	29	faccld	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to k! \in ℕ$
35	34	nncnd	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to k! \in ℂ$
36	34	nnne0d	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to k! \neq 0$
37	33 35 36	divcld	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
38		simplr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to X \in ℂ$
39	2	ad2antrr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to F : A ⟶ ℂ$
40		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to dom (S D^{n} F) (k) \subseteq dom F$
41	6 11 29 40	syl3anc	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to dom (S D^{n} F) (k) \subseteq dom F$
42	39 41	fssdmd	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to dom (S D^{n} F) (k) \subseteq A$
43		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
44	1 43	syl	$⊢ φ \to S \subseteq ℂ$
45	3 44	sstrd	$⊢ φ \to A \subseteq ℂ$
46	45	ad2antrr	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to A \subseteq ℂ$
47	42 46	sstrd	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to dom (S D^{n} F) (k) \subseteq ℂ$
48	47 32	sseldd	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to B \in ℂ$
49	38 48	subcld	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to X - B \in ℂ$
50	49 29	expcld	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to {(X - B)}^{k} \in ℂ$
51	37 50	mulcld	$⊢ ((φ \land X \in ℂ) \land k \in ([0, N] \cap ℤ)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(X - B)}^{k} \in ℂ$

Metamath Proof Explorer

Theorem taylfvallem1

Proof