Theorem etransclem39

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

	Ref	Expression
Hypotheses	etransclem39.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem39.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	etransclem39.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
	etransclem39.g	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
Assertion	etransclem39	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		etransclem39.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2		etransclem39.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3		etransclem39.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
4		etransclem39.g	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
5		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 0 ... 𝑅 ) ∈ Fin )
6		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
7	6	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ℝ ∈ { ℝ , ℂ } )
8		reopn	⊢ ℝ ∈ ( topGen ‘ ran (,) )
9		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
10	8 9	eleqtri	⊢ ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
11	10	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
12	1	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑃 ∈ ℕ )
13	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑀 ∈ ℕ0 )
14		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... 𝑅 ) → 𝑖 ∈ ℕ0 )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑖 ∈ ℕ0 )
16	7 11 12 13 3 15	etransclem33	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
17	16	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
18		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑥 ∈ ℝ )
19	17 18	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℂ )
20	5 19	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℂ )
21	20 4	fmptd	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℂ )