Metamath Proof Explorer

Theorem psercn

Description: An infinite series converges to a continuous function on the open disk of radius R , where R is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015)

Ref Expression
Hypotheses pserf.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
pserf.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
pserf.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
pserf.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
psercn.s ⊢ 𝑆 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
psercn.m ⊢ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
Assertion psercn ( 𝜑 → 𝐹 ∈ ( 𝑆 –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 psercn.s ⊢ 𝑆 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
6 psercn.m ⊢ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
7 sumex ⊢ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ∈ V
8 7 rgenw ⊢ ∀ 𝑦 ∈ 𝑆 Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ∈ V
9 2 fnmpt ⊢ ( ∀ 𝑦 ∈ 𝑆 Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ∈ V → 𝐹 Fn 𝑆 )
10 8 9 mp1i ⊢ ( 𝜑 → 𝐹 Fn 𝑆 )
11 cnvimass ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
12 absf ⊢ abs : ℂ ⟶ ℝ
13 12 fdmi ⊢ dom abs = ℂ
14 11 13 sseqtri ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ ℂ
15 5 14 eqsstri ⊢ 𝑆 ⊆ ℂ
16 15 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
17 16 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ℂ )
18 0cn ⊢ 0 ∈ ℂ
19 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
20 19 cnmetdval ⊢ ( ( 0 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 0 ( abs ∘ − ) 𝑎 ) = ( abs ‘ ( 0 − 𝑎 ) ) )
21 18 17 20 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( abs ∘ − ) 𝑎 ) = ( abs ‘ ( 0 − 𝑎 ) ) )
22 abssub ⊢ ( ( 0 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( abs ‘ ( 0 − 𝑎 ) ) = ( abs ‘ ( 𝑎 − 0 ) ) )
23 18 17 22 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ ( 0 − 𝑎 ) ) = ( abs ‘ ( 𝑎 − 0 ) ) )
24 17 subid1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 − 0 ) = 𝑎 )
25 24 fveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ ( 𝑎 − 0 ) ) = ( abs ‘ 𝑎 ) )
26 21 23 25 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( abs ∘ − ) 𝑎 ) = ( abs ‘ 𝑎 ) )
27 breq2 ⊢ ( ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ↔ ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ) )
28 breq2 ⊢ ( ( ( abs ‘ 𝑎 ) + 1 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) ↔ ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ) )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 )
30 29 5 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) )
31 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
32 elpreima ⊢ ( abs Fn ℂ → ( 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) ) )
33 12 31 32 mp2b ⊢ ( 𝑎 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) )
34 30 33 sylib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) )
35 34 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) )
36 0re ⊢ 0 ∈ ℝ
37 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
38 1 3 4 radcnvcl ⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ( 0 [,] +∞ ) )
40 37 39 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ℝ* )
41 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) ) )
42 36 40 41 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) ) )
43 35 42 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) )
44 43 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < 𝑅 )
45 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < 𝑅 )
46 17 abscld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) ∈ ℝ )
47 avglt1 ⊢ ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ) )
48 46 47 sylan ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ) )
49 45 48 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) )
50 46 ltp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ¬ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) )
52 27 28 49 51 ifbothda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) )
53 52 6 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < 𝑀 )
54 26 53 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( abs ∘ − ) 𝑎 ) < 𝑀 )
55 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
56 1 2 3 4 5 6 psercnlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
57 56 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ+ )
58 57 rpxrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ* )
59 elbl ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑀 ∈ ℝ* ) → ( 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↔ ( 𝑎 ∈ ℂ ∧ ( 0 ( abs ∘ − ) 𝑎 ) < 𝑀 ) ) )
60 55 18 58 59 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↔ ( 𝑎 ∈ ℂ ∧ ( 0 ( abs ∘ − ) 𝑎 ) < 𝑀 ) ) )
61 17 54 60 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
62 61 fvresd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
63 2 reseq1i ⊢ ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ) ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
64 1 2 3 4 5 56 psercnlem2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ∧ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ 𝑆 ) )
65 64 simp2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
66 64 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ 𝑆 )
67 65 66 sstrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ 𝑆 )
68 67 resmptd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ) ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ) )
69 63 68 syl5eq ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ) )
70 eqid ⊢ ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
71 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
72 fveq2 ⊢ ( 𝑘 = 𝑦 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑦 ) )
73 72 seqeq3d ⊢ ( 𝑘 = 𝑦 → seq 0 ( + , ( 𝐺 ‘ 𝑘 ) ) = seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) )
74 73 fveq1d ⊢ ( 𝑘 = 𝑦 → ( seq 0 ( + , ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑠 ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑠 ) )
75 74 cbvmptv ⊢ ( 𝑘 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑠 ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑠 ) )
76 fveq2 ⊢ ( 𝑠 = 𝑖 → ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑠 ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) )
77 76 mpteq2dv ⊢ ( 𝑠 = 𝑖 → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑠 ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
78 75 77 syl5eq ⊢ ( 𝑠 = 𝑖 → ( 𝑘 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑠 ) ) = ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
79 78 cbvmptv ⊢ ( 𝑠 ∈ ℕ0 ↦ ( 𝑘 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑠 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
80 57 rpred ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
81 56 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 < 𝑅 )
82 1 70 71 4 79 80 81 65 psercn2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑦 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ) ∈ ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) –cn→ ℂ ) )
83 69 82 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) –cn→ ℂ ) )
84 cncff ⊢ ( ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) –cn→ ℂ ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) : ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⟶ ℂ )
85 83 84 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) : ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⟶ ℂ )
86 85 61 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ‘ 𝑎 ) ∈ ℂ )
87 62 86 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
88 87 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
89 ffnfv ⊢ ( 𝐹 : 𝑆 ⟶ ℂ ↔ ( 𝐹 Fn 𝑆 ∧ ∀ 𝑎 ∈ 𝑆 ( 𝐹 ‘ 𝑎 ) ∈ ℂ ) )
90 10 88 89 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
91 67 15 sstrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ℂ )
92 ssid ⊢ ℂ ⊆ ℂ
93 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
94 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
95 93 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
96 95 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
97 93 94 96 cncfcn ⊢ ( ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
98 91 92 97 sylancl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
99 83 98 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
100 93 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
101 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
102 101 restuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ ℂ ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) )
103 100 91 102 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) )
104 61 103 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) )
105 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
106 105 cncnpi ⊢ ( ( ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ 𝑎 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) )
107 99 104 106 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) )
108 cnex ⊢ ℂ ∈ V
109 108 15 ssexi ⊢ 𝑆 ∈ V
110 109 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑆 ∈ V )
111 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) )
112 100 67 110 111 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) )
113 112 oveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) )
114 113 fveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) )
115 107 114 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) )
116 resttop ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
117 100 109 116 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top
118 117 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
119 df-ss ⊢ ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ 𝑆 ↔ ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∩ 𝑆 ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
120 67 119 sylib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∩ 𝑆 ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
121 93 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
122 121 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑀 ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∈ ( TopOpen ‘ ℂfld ) )
123 55 18 58 122 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∈ ( TopOpen ‘ ℂfld ) )
124 elrestr ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ∈ V ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∈ ( TopOpen ‘ ℂfld ) ) → ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∩ 𝑆 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
125 100 109 123 124 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∩ 𝑆 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
126 120 125 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
127 isopn3i ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
128 117 126 127 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) )
129 61 128 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) )
130 90 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐹 : 𝑆 ⟶ ℂ )
131 101 restuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ⊆ ℂ ) → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
132 100 15 131 mp2an ⊢ 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
133 132 101 cnprest ⊢ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ⊆ 𝑆 ) ∧ ( 𝑎 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∧ 𝐹 : 𝑆 ⟶ ℂ ) ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) ↔ ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) ) )
134 118 67 129 130 133 syl22anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) ↔ ( 𝐹 ↾ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑀 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) ) )
135 115 134 mpbird ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) )
136 135 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) )
137 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
138 95 15 137 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 )
139 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝑆 ⟶ ℂ ∧ ∀ 𝑎 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) ) ) )
140 138 95 139 mp2an ⊢ ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝑆 ⟶ ℂ ∧ ∀ 𝑎 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑎 ) ) )
141 90 136 140 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) )
142 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
143 93 142 96 cncfcn ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑆 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) )
144 15 92 143 mp2an ⊢ ( 𝑆 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) )
145 141 144 eleqtrrdi ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )