Metamath Proof Explorer

Theorem abelth

Description: Abel's theorem. If the power series sum_ n e. NN0 A ( n ) ( x ^ n ) is convergent at 1 , then it is equal to the limit from "below", along a Stolz angle S (note that the M = 1 case of a Stolz angle is the real line [ 0 , 1 ] ). (Continuity on S \ { 1 } follows more generally from psercn .) (Contributed by Mario Carneiro, 2-Apr-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses abelth.1 ⊒ ( πœ‘ β†’ 𝐴 : β„•0 ⟢ β„‚ )
abelth.2 ⊒ ( πœ‘ β†’ seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊒ ( πœ‘ β†’ 𝑀 ∈ ℝ )
abelth.4 ⊒ ( πœ‘ β†’ 0 ≀ 𝑀 )
abelth.5 ⊒ 𝑆 = { 𝑧 ∈ β„‚ ∣ ( abs β€˜ ( 1 βˆ’ 𝑧 ) ) ≀ ( 𝑀 Β· ( 1 βˆ’ ( abs β€˜ 𝑧 ) ) ) }
abelth.6 ⊒ 𝐹 = ( π‘₯ ∈ 𝑆 ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) )
Assertion abelth ( πœ‘ β†’ 𝐹 ∈ ( 𝑆 –cnβ†’ β„‚ ) )

Proof

Step Hyp Ref Expression
1 abelth.1 ⊒ ( πœ‘ β†’ 𝐴 : β„•0 ⟢ β„‚ )
2 abelth.2 ⊒ ( πœ‘ β†’ seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ⊒ ( πœ‘ β†’ 𝑀 ∈ ℝ )
4 abelth.4 ⊒ ( πœ‘ β†’ 0 ≀ 𝑀 )
5 abelth.5 ⊒ 𝑆 = { 𝑧 ∈ β„‚ ∣ ( abs β€˜ ( 1 βˆ’ 𝑧 ) ) ≀ ( 𝑀 Β· ( 1 βˆ’ ( abs β€˜ 𝑧 ) ) ) }
6 abelth.6 ⊒ 𝐹 = ( π‘₯ ∈ 𝑆 ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) )
7 1 2 3 4 5 6 abelthlem4 ⊒ ( πœ‘ β†’ 𝐹 : 𝑆 ⟢ β„‚ )
8 1 2 3 4 5 6 abelthlem9 ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑆 ( ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) < 𝑀 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 1 ) βˆ’ ( 𝐹 β€˜ 𝑦 ) ) ) < π‘Ÿ ) )
9 1 2 3 4 5 abelthlem2 ⊒ ( πœ‘ β†’ ( 1 ∈ 𝑆 ∧ ( 𝑆 βˆ– { 1 } ) βŠ† ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) )
10 9 simpld ⊒ ( πœ‘ β†’ 1 ∈ 𝑆 )
11 10 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ 1 ∈ 𝑆 )
12 simpr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ 𝑦 ∈ 𝑆 )
13 11 12 ovresd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) = ( 1 ( abs ∘ βˆ’ ) 𝑦 ) )
14 ax-1cn ⊒ 1 ∈ β„‚
15 5 ssrab3 ⊒ 𝑆 βŠ† β„‚
16 15 12 sselid ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ 𝑦 ∈ β„‚ )
17 eqid ⊒ ( abs ∘ βˆ’ ) = ( abs ∘ βˆ’ )
18 17 cnmetdval ⊒ ( ( 1 ∈ β„‚ ∧ 𝑦 ∈ β„‚ ) β†’ ( 1 ( abs ∘ βˆ’ ) 𝑦 ) = ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) )
19 14 16 18 sylancr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( 1 ( abs ∘ βˆ’ ) 𝑦 ) = ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) )
20 13 19 eqtrd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) = ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) )
21 20 breq1d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 ↔ ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) < 𝑀 ) )
22 7 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ 𝐹 : 𝑆 ⟢ β„‚ )
23 22 11 ffvelcdmd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( 𝐹 β€˜ 1 ) ∈ β„‚ )
24 7 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝐹 : 𝑆 ⟢ β„‚ )
25 24 ffvelcdmda ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( 𝐹 β€˜ 𝑦 ) ∈ β„‚ )
26 17 cnmetdval ⊒ ( ( ( 𝐹 β€˜ 1 ) ∈ β„‚ ∧ ( 𝐹 β€˜ 𝑦 ) ∈ β„‚ ) β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) = ( abs β€˜ ( ( 𝐹 β€˜ 1 ) βˆ’ ( 𝐹 β€˜ 𝑦 ) ) ) )
27 23 25 26 syl2anc ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) = ( abs β€˜ ( ( 𝐹 β€˜ 1 ) βˆ’ ( 𝐹 β€˜ 𝑦 ) ) ) )
28 27 breq1d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ↔ ( abs β€˜ ( ( 𝐹 β€˜ 1 ) βˆ’ ( 𝐹 β€˜ 𝑦 ) ) ) < π‘Ÿ ) )
29 21 28 imbi12d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) β†’ ( ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ) ↔ ( ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) < 𝑀 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 1 ) βˆ’ ( 𝐹 β€˜ 𝑦 ) ) ) < π‘Ÿ ) ) )
30 29 ralbidva ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( βˆ€ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ) ↔ βˆ€ 𝑦 ∈ 𝑆 ( ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) < 𝑀 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 1 ) βˆ’ ( 𝐹 β€˜ 𝑦 ) ) ) < π‘Ÿ ) ) )
31 30 rexbidv ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ) ↔ βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑆 ( ( abs β€˜ ( 1 βˆ’ 𝑦 ) ) < 𝑀 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 1 ) βˆ’ ( 𝐹 β€˜ 𝑦 ) ) ) < π‘Ÿ ) ) )
32 8 31 mpbird ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ) )
33 32 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ π‘Ÿ ∈ ℝ+ βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ) )
34 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
35 xmetres2 ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 𝑆 βŠ† β„‚ ) β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) ∈ ( ∞Met β€˜ 𝑆 ) )
36 34 15 35 mp2an ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) ∈ ( ∞Met β€˜ 𝑆 )
37 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) )
38 eqid ⊒ ( TopOpen β€˜ β„‚fld ) = ( TopOpen β€˜ β„‚fld )
39 38 cnfldtopn ⊒ ( TopOpen β€˜ β„‚fld ) = ( MetOpen β€˜ ( abs ∘ βˆ’ ) )
40 eqid ⊒ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) )
41 37 39 40 metrest ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 𝑆 βŠ† β„‚ ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) ) )
42 34 15 41 mp2an ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) )
43 42 39 metcnp ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) ∈ ( ∞Met β€˜ 𝑆 ) ∧ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 1 ∈ 𝑆 ) β†’ ( 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 1 ) ↔ ( 𝐹 : 𝑆 ⟢ β„‚ ∧ βˆ€ π‘Ÿ ∈ ℝ+ βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ) ) ) )
44 36 34 10 43 mp3an12i ⊒ ( πœ‘ β†’ ( 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 1 ) ↔ ( 𝐹 : 𝑆 ⟢ β„‚ ∧ βˆ€ π‘Ÿ ∈ ℝ+ βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ βˆ’ ) β†Ύ ( 𝑆 Γ— 𝑆 ) ) 𝑦 ) < 𝑀 β†’ ( ( 𝐹 β€˜ 1 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑦 ) ) < π‘Ÿ ) ) ) )
45 7 33 44 mpbir2and ⊒ ( πœ‘ β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 1 ) )
46 45 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 1 ) )
47 simpr ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) β†’ 𝑦 = 1 )
48 47 fveq2d ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) β†’ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) = ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 1 ) )
49 46 48 eleqtrrd ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
50 eldifsn ⊒ ( 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ↔ ( 𝑦 ∈ 𝑆 ∧ 𝑦 β‰  1 ) )
51 9 simprd ⊒ ( πœ‘ β†’ ( 𝑆 βˆ– { 1 } ) βŠ† ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
52 abscl ⊒ ( 𝑀 ∈ β„‚ β†’ ( abs β€˜ 𝑀 ) ∈ ℝ )
53 52 adantl ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( abs β€˜ 𝑀 ) ∈ ℝ )
54 53 a1d ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( abs β€˜ 𝑀 ) < 1 β†’ ( abs β€˜ 𝑀 ) ∈ ℝ ) )
55 absge0 ⊒ ( 𝑀 ∈ β„‚ β†’ 0 ≀ ( abs β€˜ 𝑀 ) )
56 55 adantl ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ 0 ≀ ( abs β€˜ 𝑀 ) )
57 56 a1d ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( abs β€˜ 𝑀 ) < 1 β†’ 0 ≀ ( abs β€˜ 𝑀 ) ) )
58 1 2 abelthlem1 ⊒ ( πœ‘ β†’ 1 ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) )
59 58 adantr ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ 1 ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) )
60 53 rexrd ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( abs β€˜ 𝑀 ) ∈ ℝ* )
61 1re ⊒ 1 ∈ ℝ
62 rexr ⊒ ( 1 ∈ ℝ β†’ 1 ∈ ℝ* )
63 61 62 mp1i ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ 1 ∈ ℝ* )
64 iccssxr ⊒ ( 0 [,] +∞ ) βŠ† ℝ*
65 eqid ⊒ ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) = ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) )
66 eqid ⊒ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < )
67 65 1 66 radcnvcl ⊒ ( πœ‘ β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
68 64 67 sselid ⊒ ( πœ‘ β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
69 68 adantr ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
70 xrltletr ⊒ ( ( ( abs β€˜ 𝑀 ) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* ) β†’ ( ( ( abs β€˜ 𝑀 ) < 1 ∧ 1 ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) β†’ ( abs β€˜ 𝑀 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
71 60 63 69 70 syl3anc ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( ( abs β€˜ 𝑀 ) < 1 ∧ 1 ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) β†’ ( abs β€˜ 𝑀 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
72 59 71 mpan2d ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( abs β€˜ 𝑀 ) < 1 β†’ ( abs β€˜ 𝑀 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
73 54 57 72 3jcad ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( abs β€˜ 𝑀 ) < 1 β†’ ( ( abs β€˜ 𝑀 ) ∈ ℝ ∧ 0 ≀ ( abs β€˜ 𝑀 ) ∧ ( abs β€˜ 𝑀 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
74 0cn ⊒ 0 ∈ β„‚
75 17 cnmetdval ⊒ ( ( 0 ∈ β„‚ ∧ 𝑀 ∈ β„‚ ) β†’ ( 0 ( abs ∘ βˆ’ ) 𝑀 ) = ( abs β€˜ ( 0 βˆ’ 𝑀 ) ) )
76 74 75 mpan ⊒ ( 𝑀 ∈ β„‚ β†’ ( 0 ( abs ∘ βˆ’ ) 𝑀 ) = ( abs β€˜ ( 0 βˆ’ 𝑀 ) ) )
77 abssub ⊒ ( ( 0 ∈ β„‚ ∧ 𝑀 ∈ β„‚ ) β†’ ( abs β€˜ ( 0 βˆ’ 𝑀 ) ) = ( abs β€˜ ( 𝑀 βˆ’ 0 ) ) )
78 74 77 mpan ⊒ ( 𝑀 ∈ β„‚ β†’ ( abs β€˜ ( 0 βˆ’ 𝑀 ) ) = ( abs β€˜ ( 𝑀 βˆ’ 0 ) ) )
79 subid1 ⊒ ( 𝑀 ∈ β„‚ β†’ ( 𝑀 βˆ’ 0 ) = 𝑀 )
80 79 fveq2d ⊒ ( 𝑀 ∈ β„‚ β†’ ( abs β€˜ ( 𝑀 βˆ’ 0 ) ) = ( abs β€˜ 𝑀 ) )
81 76 78 80 3eqtrd ⊒ ( 𝑀 ∈ β„‚ β†’ ( 0 ( abs ∘ βˆ’ ) 𝑀 ) = ( abs β€˜ 𝑀 ) )
82 81 breq1d ⊒ ( 𝑀 ∈ β„‚ β†’ ( ( 0 ( abs ∘ βˆ’ ) 𝑀 ) < 1 ↔ ( abs β€˜ 𝑀 ) < 1 ) )
83 82 adantl ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( 0 ( abs ∘ βˆ’ ) 𝑀 ) < 1 ↔ ( abs β€˜ 𝑀 ) < 1 ) )
84 0re ⊒ 0 ∈ ℝ
85 elico2 ⊒ ( ( 0 ∈ ℝ ∧ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* ) β†’ ( ( abs β€˜ 𝑀 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs β€˜ 𝑀 ) ∈ ℝ ∧ 0 ≀ ( abs β€˜ 𝑀 ) ∧ ( abs β€˜ 𝑀 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
86 84 69 85 sylancr ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( abs β€˜ 𝑀 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs β€˜ 𝑀 ) ∈ ℝ ∧ 0 ≀ ( abs β€˜ 𝑀 ) ∧ ( abs β€˜ 𝑀 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
87 73 83 86 3imtr4d ⊒ ( ( πœ‘ ∧ 𝑀 ∈ β„‚ ) β†’ ( ( 0 ( abs ∘ βˆ’ ) 𝑀 ) < 1 β†’ ( abs β€˜ 𝑀 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
88 87 imdistanda ⊒ ( πœ‘ β†’ ( ( 𝑀 ∈ β„‚ ∧ ( 0 ( abs ∘ βˆ’ ) 𝑀 ) < 1 ) β†’ ( 𝑀 ∈ β„‚ ∧ ( abs β€˜ 𝑀 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
89 1xr ⊒ 1 ∈ ℝ*
90 elbl ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 0 ∈ β„‚ ∧ 1 ∈ ℝ* ) β†’ ( 𝑀 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝑀 ∈ β„‚ ∧ ( 0 ( abs ∘ βˆ’ ) 𝑀 ) < 1 ) ) )
91 34 74 89 90 mp3an ⊒ ( 𝑀 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝑀 ∈ β„‚ ∧ ( 0 ( abs ∘ βˆ’ ) 𝑀 ) < 1 ) )
92 absf ⊒ abs : β„‚ ⟢ ℝ
93 ffn ⊒ ( abs : β„‚ ⟢ ℝ β†’ abs Fn β„‚ )
94 elpreima ⊒ ( abs Fn β„‚ β†’ ( 𝑀 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑀 ∈ β„‚ ∧ ( abs β€˜ 𝑀 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
95 92 93 94 mp2b ⊒ ( 𝑀 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑀 ∈ β„‚ ∧ ( abs β€˜ 𝑀 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
96 88 91 95 3imtr4g ⊒ ( πœ‘ β†’ ( 𝑀 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 𝑀 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
97 96 ssrdv ⊒ ( πœ‘ β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
98 51 97 sstrd ⊒ ( πœ‘ β†’ ( 𝑆 βˆ– { 1 } ) βŠ† ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
99 98 resmptd ⊒ ( πœ‘ β†’ ( ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) β†Ύ ( 𝑆 βˆ– { 1 } ) ) = ( π‘₯ ∈ ( 𝑆 βˆ– { 1 } ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
100 6 reseq1i ⊒ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) = ( ( π‘₯ ∈ 𝑆 ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) β†Ύ ( 𝑆 βˆ– { 1 } ) )
101 difss ⊒ ( 𝑆 βˆ– { 1 } ) βŠ† 𝑆
102 resmpt ⊒ ( ( 𝑆 βˆ– { 1 } ) βŠ† 𝑆 β†’ ( ( π‘₯ ∈ 𝑆 ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) β†Ύ ( 𝑆 βˆ– { 1 } ) ) = ( π‘₯ ∈ ( 𝑆 βˆ– { 1 } ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
103 101 102 ax-mp ⊒ ( ( π‘₯ ∈ 𝑆 ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) β†Ύ ( 𝑆 βˆ– { 1 } ) ) = ( π‘₯ ∈ ( 𝑆 βˆ– { 1 } ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) )
104 100 103 eqtri ⊒ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) = ( π‘₯ ∈ ( 𝑆 βˆ– { 1 } ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) )
105 99 104 eqtr4di ⊒ ( πœ‘ β†’ ( ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) β†Ύ ( 𝑆 βˆ– { 1 } ) ) = ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) )
106 cnvimass ⊒ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) βŠ† dom abs
107 92 fdmi ⊒ dom abs = β„‚
108 106 107 sseqtri ⊒ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) βŠ† β„‚
109 108 sseli ⊒ ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) β†’ π‘₯ ∈ β„‚ )
110 fveq2 ⊒ ( 𝑛 = 𝑗 β†’ ( 𝐴 β€˜ 𝑛 ) = ( 𝐴 β€˜ 𝑗 ) )
111 oveq2 ⊒ ( 𝑛 = 𝑗 β†’ ( π‘₯ ↑ 𝑛 ) = ( π‘₯ ↑ 𝑗 ) )
112 110 111 oveq12d ⊒ ( 𝑛 = 𝑗 β†’ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) = ( ( 𝐴 β€˜ 𝑗 ) Β· ( π‘₯ ↑ 𝑗 ) ) )
113 112 cbvsumv ⊒ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) = Ξ£ 𝑗 ∈ β„•0 ( ( 𝐴 β€˜ 𝑗 ) Β· ( π‘₯ ↑ 𝑗 ) )
114 65 pserval2 ⊒ ( ( π‘₯ ∈ β„‚ ∧ 𝑗 ∈ β„•0 ) β†’ ( ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘₯ ) β€˜ 𝑗 ) = ( ( 𝐴 β€˜ 𝑗 ) Β· ( π‘₯ ↑ 𝑗 ) ) )
115 114 sumeq2dv ⊒ ( π‘₯ ∈ β„‚ β†’ Ξ£ 𝑗 ∈ β„•0 ( ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘₯ ) β€˜ 𝑗 ) = Ξ£ 𝑗 ∈ β„•0 ( ( 𝐴 β€˜ 𝑗 ) Β· ( π‘₯ ↑ 𝑗 ) ) )
116 113 115 eqtr4id ⊒ ( π‘₯ ∈ β„‚ β†’ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) = Ξ£ 𝑗 ∈ β„•0 ( ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘₯ ) β€˜ 𝑗 ) )
117 109 116 syl ⊒ ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) β†’ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) = Ξ£ 𝑗 ∈ β„•0 ( ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘₯ ) β€˜ 𝑗 ) )
118 117 mpteq2ia ⊒ ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) = ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑗 ∈ β„•0 ( ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘₯ ) β€˜ 𝑗 ) )
119 eqid ⊒ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) = ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
120 eqid ⊒ if ( sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs β€˜ 𝑣 ) + sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs β€˜ 𝑣 ) + 1 ) ) = if ( sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs β€˜ 𝑣 ) + sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs β€˜ 𝑣 ) + 1 ) )
121 65 118 1 66 119 120 psercn ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) ∈ ( ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cnβ†’ β„‚ ) )
122 rescncf ⊒ ( ( 𝑆 βˆ– { 1 } ) βŠ† ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) β†’ ( ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) ∈ ( ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cnβ†’ β„‚ ) β†’ ( ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( 𝑆 βˆ– { 1 } ) –cnβ†’ β„‚ ) ) )
123 98 121 122 sylc ⊒ ( πœ‘ β†’ ( ( π‘₯ ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( 𝑑 ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( 𝑑 ↑ 𝑛 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( 𝑆 βˆ– { 1 } ) –cnβ†’ β„‚ ) )
124 105 123 eqeltrrd ⊒ ( πœ‘ β†’ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( 𝑆 βˆ– { 1 } ) –cnβ†’ β„‚ ) )
125 124 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( 𝑆 βˆ– { 1 } ) –cnβ†’ β„‚ ) )
126 101 15 sstri ⊒ ( 𝑆 βˆ– { 1 } ) βŠ† β„‚
127 ssid ⊒ β„‚ βŠ† β„‚
128 eqid ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) )
129 38 cnfldtopon ⊒ ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ )
130 129 toponrestid ⊒ ( TopOpen β€˜ β„‚fld ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt β„‚ )
131 38 128 130 cncfcn ⊒ ( ( ( 𝑆 βˆ– { 1 } ) βŠ† β„‚ ∧ β„‚ βŠ† β„‚ ) β†’ ( ( 𝑆 βˆ– { 1 } ) –cnβ†’ β„‚ ) = ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) Cn ( TopOpen β€˜ β„‚fld ) ) )
132 126 127 131 mp2an ⊒ ( ( 𝑆 βˆ– { 1 } ) –cnβ†’ β„‚ ) = ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) Cn ( TopOpen β€˜ β„‚fld ) )
133 125 132 eleqtrdi ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) Cn ( TopOpen β€˜ β„‚fld ) ) )
134 simpr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) )
135 resttopon ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ ) ∧ ( 𝑆 βˆ– { 1 } ) βŠ† β„‚ ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) ∈ ( TopOn β€˜ ( 𝑆 βˆ– { 1 } ) ) )
136 129 126 135 mp2an ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) ∈ ( TopOn β€˜ ( 𝑆 βˆ– { 1 } ) )
137 136 toponunii ⊒ ( 𝑆 βˆ– { 1 } ) = βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) )
138 137 cncnpi ⊒ ( ( ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) Cn ( TopOpen β€˜ β„‚fld ) ) ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
139 133 134 138 syl2anc ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
140 38 cnfldtop ⊒ ( TopOpen β€˜ β„‚fld ) ∈ Top
141 cnex ⊒ β„‚ ∈ V
142 141 15 ssexi ⊒ 𝑆 ∈ V
143 restabs ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ Top ∧ ( 𝑆 βˆ– { 1 } ) βŠ† 𝑆 ∧ 𝑆 ∈ V ) β†’ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) )
144 140 101 142 143 mp3an ⊒ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) )
145 144 oveq1i ⊒ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) = ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) )
146 145 fveq1i ⊒ ( ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) = ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 )
147 139 146 eleqtrrdi ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
148 resttop ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ Top ∧ 𝑆 ∈ V ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ Top )
149 140 142 148 mp2an ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ Top
150 149 a1i ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ Top )
151 101 a1i ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( 𝑆 βˆ– { 1 } ) βŠ† 𝑆 )
152 10 snssd ⊒ ( πœ‘ β†’ { 1 } βŠ† 𝑆 )
153 38 cnfldhaus ⊒ ( TopOpen β€˜ β„‚fld ) ∈ Haus
154 unicntop ⊒ β„‚ = βˆͺ ( TopOpen β€˜ β„‚fld )
155 154 sncld ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ Haus ∧ 1 ∈ β„‚ ) β†’ { 1 } ∈ ( Clsd β€˜ ( TopOpen β€˜ β„‚fld ) ) )
156 153 14 155 mp2an ⊒ { 1 } ∈ ( Clsd β€˜ ( TopOpen β€˜ β„‚fld ) )
157 154 restcldi ⊒ ( ( 𝑆 βŠ† β„‚ ∧ { 1 } ∈ ( Clsd β€˜ ( TopOpen β€˜ β„‚fld ) ) ∧ { 1 } βŠ† 𝑆 ) β†’ { 1 } ∈ ( Clsd β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) )
158 15 156 157 mp3an12 ⊒ ( { 1 } βŠ† 𝑆 β†’ { 1 } ∈ ( Clsd β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) )
159 154 restuni ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ Top ∧ 𝑆 βŠ† β„‚ ) β†’ 𝑆 = βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) )
160 140 15 159 mp2an ⊒ 𝑆 = βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 )
161 160 cldopn ⊒ ( { 1 } ∈ ( Clsd β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) β†’ ( 𝑆 βˆ– { 1 } ) ∈ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) )
162 152 158 161 3syl ⊒ ( πœ‘ β†’ ( 𝑆 βˆ– { 1 } ) ∈ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) )
163 160 isopn3 ⊒ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ Top ∧ ( 𝑆 βˆ– { 1 } ) βŠ† 𝑆 ) β†’ ( ( 𝑆 βˆ– { 1 } ) ∈ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ↔ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) β€˜ ( 𝑆 βˆ– { 1 } ) ) = ( 𝑆 βˆ– { 1 } ) ) )
164 149 101 163 mp2an ⊒ ( ( 𝑆 βˆ– { 1 } ) ∈ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ↔ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) β€˜ ( 𝑆 βˆ– { 1 } ) ) = ( 𝑆 βˆ– { 1 } ) )
165 162 164 sylib ⊒ ( πœ‘ β†’ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) β€˜ ( 𝑆 βˆ– { 1 } ) ) = ( 𝑆 βˆ– { 1 } ) )
166 165 eleq2d ⊒ ( πœ‘ β†’ ( 𝑦 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) β€˜ ( 𝑆 βˆ– { 1 } ) ) ↔ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) )
167 166 biimpar ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ 𝑦 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) β€˜ ( 𝑆 βˆ– { 1 } ) ) )
168 7 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ 𝐹 : 𝑆 ⟢ β„‚ )
169 160 154 cnprest ⊒ ( ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ Top ∧ ( 𝑆 βˆ– { 1 } ) βŠ† 𝑆 ) ∧ ( 𝑦 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ) β€˜ ( 𝑆 βˆ– { 1 } ) ) ∧ 𝐹 : 𝑆 ⟢ β„‚ ) ) β†’ ( 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) ↔ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) ) )
170 150 151 167 168 169 syl22anc ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ ( 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) ↔ ( 𝐹 β†Ύ ( 𝑆 βˆ– { 1 } ) ) ∈ ( ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) β†Ύt ( 𝑆 βˆ– { 1 } ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) ) )
171 147 170 mpbird ⊒ ( ( πœ‘ ∧ 𝑦 ∈ ( 𝑆 βˆ– { 1 } ) ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
172 50 171 sylan2br ⊒ ( ( πœ‘ ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑦 β‰  1 ) ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
173 172 anassrs ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 β‰  1 ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
174 49 173 pm2.61dane ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝑆 ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
175 174 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) )
176 resttopon ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ ) ∧ 𝑆 βŠ† β„‚ ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ ( TopOn β€˜ 𝑆 ) )
177 129 15 176 mp2an ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ ( TopOn β€˜ 𝑆 )
178 cncnp ⊒ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) ∈ ( TopOn β€˜ 𝑆 ) ∧ ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ ) ) β†’ ( 𝐹 ∈ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) Cn ( TopOpen β€˜ β„‚fld ) ) ↔ ( 𝐹 : 𝑆 ⟢ β„‚ ∧ βˆ€ 𝑦 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) ) ) )
179 177 129 178 mp2an ⊒ ( 𝐹 ∈ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) Cn ( TopOpen β€˜ β„‚fld ) ) ↔ ( 𝐹 : 𝑆 ⟢ β„‚ ∧ βˆ€ 𝑦 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑦 ) ) )
180 7 175 179 sylanbrc ⊒ ( πœ‘ β†’ 𝐹 ∈ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) Cn ( TopOpen β€˜ β„‚fld ) ) )
181 eqid ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 )
182 38 181 130 cncfcn ⊒ ( ( 𝑆 βŠ† β„‚ ∧ β„‚ βŠ† β„‚ ) β†’ ( 𝑆 –cnβ†’ β„‚ ) = ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) Cn ( TopOpen β€˜ β„‚fld ) ) )
183 15 127 182 mp2an ⊒ ( 𝑆 –cnβ†’ β„‚ ) = ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt 𝑆 ) Cn ( TopOpen β€˜ β„‚fld ) )
184 180 183 eleqtrrdi ⊒ ( πœ‘ β†’ 𝐹 ∈ ( 𝑆 –cnβ†’ β„‚ ) )