etransclem39

Description: G is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Step	Hyp	Ref	Expression
1		etransclem39.p	$⊢ φ \to P \in ℕ$
2		etransclem39.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem39.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
4		etransclem39.g	$⊢ G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x))$
5		fzfid	$⊢ (φ \land x \in ℝ) \to (0 \dots R) \in Fin$
6		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
7	6	a1i	$⊢ (φ \land i \in (0 \dots R)) \to ℝ \in \{ℝ, ℂ\}$
8		reopn	$⊢ ℝ \in topGen (ran (.))$
9		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
10	9	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
11	8 10	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
12	11	a1i	$⊢ (φ \land i \in (0 \dots R)) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
13	1	adantr	$⊢ (φ \land i \in (0 \dots R)) \to P \in ℕ$
14	2	adantr	$⊢ (φ \land i \in (0 \dots R)) \to M \in ℕ_{0}$
15		elfznn0	$⊢ i \in (0 \dots R) \to i \in ℕ_{0}$
16	15	adantl	$⊢ (φ \land i \in (0 \dots R)) \to i \in ℕ_{0}$
17	7 12 13 14 3 16	etransclem33	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
18	17	adantlr	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
19		simplr	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to x \in ℝ$
20	18 19	ffvelrnd	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) (x) \in ℂ$
21	5 20	fsumcl	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x) \in ℂ$
22	21 4	fmptd	$⊢ φ \to G : ℝ ⟶ ℂ$

Metamath Proof Explorer