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		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
10	8 9	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
11	10	a1i	$⊢ (φ \land i \in (0 \dots R)) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
12	1	adantr	$⊢ (φ \land i \in (0 \dots R)) \to P \in ℕ$
13	2	adantr	$⊢ (φ \land i \in (0 \dots R)) \to M \in ℕ_{0}$
14		elfznn0	$⊢ i \in (0 \dots R) \to i \in ℕ_{0}$
15	14	adantl	$⊢ (φ \land i \in (0 \dots R)) \to i \in ℕ_{0}$
16	7 11 12 13 3 15	etransclem33	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
17	16	adantlr	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
18		simplr	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to x \in ℝ$
19	17 18	ffvelcdmd	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) (x) \in ℂ$
20	5 19	fsumcl	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x) \in ℂ$
21	20 4	fmptd	$⊢ φ \to G : ℝ ⟶ ℂ$

Metamath Proof Explorer