etransclem43

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

	Ref	Expression
Hypotheses	etransclem43.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	etransclem43.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
	etransclem43.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem43.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
	etransclem43.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
	etransclem43.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
Assertion	etransclem43	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		etransclem43.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		etransclem43.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
3		etransclem43.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4		etransclem43.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
5		etransclem43.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
6		etransclem43.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
7	1 2	dvdmsscn	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
8		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑅 ) ∈ Fin )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑆 ∈ { ℝ , ℂ } )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
11	3	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑃 ∈ ℕ )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑀 ∈ ℕ₀ )
13		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... 𝑅 ) → 𝑖 ∈ ℕ₀ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑖 ∈ ℕ₀ )
15	9 10 11 12 5 14	etransclem33	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) : 𝑋 ⟶ ℂ )
16	15	feqmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
17	9 10 11 12 5 14	etransclem40	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) ∈ ( 𝑋 –cn→ ℂ ) )
18	16 17	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
19	7 8 18	fsumcncf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
20	6 19	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )

Metamath Proof Explorer

Theorem etransclem43

Proof