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		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
10	9	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
11	8 10	eleqtri	⊢ ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
13	1	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑃 ∈ ℕ )
14	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑀 ∈ ℕ0 )
15		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... 𝑅 ) → 𝑖 ∈ ℕ0 )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑖 ∈ ℕ0 )
17	7 12 13 14 3 16	etransclem33	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
18	17	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
19		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑥 ∈ ℝ )
20	18 19	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℂ )
21	5 20	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℂ )
22	21 4	fmptd	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℂ )