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 sselid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑅 ∈ ℝ* )
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 eqtrid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝐹 β†Ύ ( 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 eqtrid ⊒ ( 𝑠 = 𝑖 β†’ ( π‘˜ ∈ ( 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 ffvelcdmd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( 𝐹 β†Ύ ( 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β†’ β„‚ ) )