Metamath Proof Explorer

Theorem psercn2

Description: Since by pserulm the series converges uniformly, it is also continuous by ulmcn . (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses pserf.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
pserf.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
pserf.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
pserf.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
pserulm.h ⊢ 𝐻 = ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
pserulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
pserulm.l ⊢ ( 𝜑 → 𝑀 < 𝑅 )
pserulm.y ⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
Assertion psercn2 ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 pserf.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 pserf.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
3 pserf.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4 pserf.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
5 pserulm.h ⊢ 𝐻 = ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
6 pserulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
7 pserulm.l ⊢ ( 𝜑 → 𝑀 < 𝑅 )
8 pserulm.y ⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
9 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
11 cnvimass ⊢ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ dom abs
12 absf ⊢ abs : ℂ ⟶ ℝ
13 12 fdmi ⊢ dom abs = ℂ
14 11 13 sseqtri ⊢ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ ℂ
15 8 14 sstrdi ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑆 ⊆ ℂ )
17 16 resmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ↾ 𝑆 ) = ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
18 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑦 ∈ ℂ )
19 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑖 ) → 𝑘 ∈ ℕ0 )
20 19 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑘 ∈ ℕ0 )
21 1 pserval2 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) )
22 18 20 21 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
24 23 9 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
26 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐴 : ℕ0 ⟶ ℂ )
27 26 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
28 27 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
29 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑘 ) ∈ ℂ )
30 29 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑘 ) ∈ ℂ )
31 28 30 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ∈ ℂ )
32 19 31 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ∈ ℂ )
33 22 25 32 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) )
34 33 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
35 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
36 35 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
37 36 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
38 fzfid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 0 ... 𝑖 ) ∈ Fin )
39 36 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
40 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
41 26 19 40 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
42 39 39 41 cnmptc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑦 ∈ ℂ ↦ ( 𝐴 ‘ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
43 19 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑘 ∈ ℕ0 )
44 35 expcn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
45 43 44 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
46 35 mulcn ⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
47 46 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
48 39 42 45 47 cnmpt12f ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
49 35 37 38 48 fsumcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
50 35 cncfcn1 ⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
51 49 50 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
52 34 51 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( ℂ –cn→ ℂ ) )
53 rescncf ⊢ ( 𝑆 ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ↾ 𝑆 ) ∈ ( 𝑆 –cn→ ℂ ) ) )
54 16 52 53 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ↾ 𝑆 ) ∈ ( 𝑆 –cn→ ℂ ) )
55 17 54 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( 𝑆 –cn→ ℂ ) )
56 55 5 fmptd ⊢ ( 𝜑 → 𝐻 : ℕ0 ⟶ ( 𝑆 –cn→ ℂ ) )
57 1 2 3 4 5 6 7 8 pserulm ⊢ ( 𝜑 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )
58 9 10 56 57 ulmcn ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )