Metamath Proof Explorer


Theorem 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 ( 𝜑𝑀 ∈ ℕ0 )
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 ( 𝜑𝑀 ∈ ℕ0 )
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 ... 𝑅 ) ) → 𝑀 ∈ ℕ0 )
13 elfznn0 ( 𝑖 ∈ ( 0 ... 𝑅 ) → 𝑖 ∈ ℕ0 )
14 13 adantl ( ( 𝜑𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑖 ∈ ℕ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→ ℂ ) )