Metamath Proof Explorer


Theorem fourierdlem62

Description: The function K is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem62.k
|- K = ( y e. ( -u _pi [,] _pi ) |-> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) )
Assertion fourierdlem62
|- K e. ( ( -u _pi [,] _pi ) -cn-> RR )

Proof

Step Hyp Ref Expression
1 fourierdlem62.k
 |-  K = ( y e. ( -u _pi [,] _pi ) |-> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) )
2 eqeq1
 |-  ( y = s -> ( y = 0 <-> s = 0 ) )
3 id
 |-  ( y = s -> y = s )
4 oveq1
 |-  ( y = s -> ( y / 2 ) = ( s / 2 ) )
5 4 fveq2d
 |-  ( y = s -> ( sin ` ( y / 2 ) ) = ( sin ` ( s / 2 ) ) )
6 5 oveq2d
 |-  ( y = s -> ( 2 x. ( sin ` ( y / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
7 3 6 oveq12d
 |-  ( y = s -> ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
8 2 7 ifbieq2d
 |-  ( y = s -> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
9 8 cbvmptv
 |-  ( y e. ( -u _pi [,] _pi ) |-> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
10 1 9 eqtri
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
11 10 fourierdlem43
 |-  K : ( -u _pi [,] _pi ) --> RR
12 ax-resscn
 |-  RR C_ CC
13 fss
 |-  ( ( K : ( -u _pi [,] _pi ) --> RR /\ RR C_ CC ) -> K : ( -u _pi [,] _pi ) --> CC )
14 11 12 13 mp2an
 |-  K : ( -u _pi [,] _pi ) --> CC
15 14 a1i
 |-  ( s = 0 -> K : ( -u _pi [,] _pi ) --> CC )
16 difss
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi )
17 elioore
 |-  ( s e. ( -u _pi (,) _pi ) -> s e. RR )
18 17 ssriv
 |-  ( -u _pi (,) _pi ) C_ RR
19 16 18 sstri
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) C_ RR
20 19 a1i
 |-  ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) C_ RR )
21 eqid
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x )
22 19 sseli
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> x e. RR )
23 21 22 fmpti
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR
24 23 a1i
 |-  ( T. -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR )
25 eqid
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) )
26 2re
 |-  2 e. RR
27 26 a1i
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR )
28 22 rehalfcld
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x / 2 ) e. RR )
29 28 resincld
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( x / 2 ) ) e. RR )
30 27 29 remulcld
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. RR )
31 25 30 fmpti
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR
32 31 a1i
 |-  ( T. -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR )
33 iooretop
 |-  ( -u _pi (,) _pi ) e. ( topGen ` ran (,) )
34 33 a1i
 |-  ( T. -> ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) )
35 0re
 |-  0 e. RR
36 negpilt0
 |-  -u _pi < 0
37 pipos
 |-  0 < _pi
38 pire
 |-  _pi e. RR
39 38 renegcli
 |-  -u _pi e. RR
40 39 rexri
 |-  -u _pi e. RR*
41 38 rexri
 |-  _pi e. RR*
42 elioo2
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* ) -> ( 0 e. ( -u _pi (,) _pi ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 < _pi ) ) )
43 40 41 42 mp2an
 |-  ( 0 e. ( -u _pi (,) _pi ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 < _pi ) )
44 35 36 37 43 mpbir3an
 |-  0 e. ( -u _pi (,) _pi )
45 44 a1i
 |-  ( T. -> 0 e. ( -u _pi (,) _pi ) )
46 eqid
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) = ( ( -u _pi (,) _pi ) \ { 0 } )
47 1ex
 |-  1 e. _V
48 eqid
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 )
49 47 48 dmmpti
 |-  dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( ( -u _pi (,) _pi ) \ { 0 } )
50 reelprrecn
 |-  RR e. { RR , CC }
51 50 a1i
 |-  ( T. -> RR e. { RR , CC } )
52 12 sseli
 |-  ( x e. RR -> x e. CC )
53 52 adantl
 |-  ( ( T. /\ x e. RR ) -> x e. CC )
54 1red
 |-  ( ( T. /\ x e. RR ) -> 1 e. RR )
55 51 dvmptid
 |-  ( T. -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
56 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
57 56 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
58 sncldre
 |-  ( 0 e. RR -> { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) )
59 35 58 ax-mp
 |-  { 0 } e. ( Clsd ` ( topGen ` ran (,) ) )
60 retopon
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
61 60 toponunii
 |-  RR = U. ( topGen ` ran (,) )
62 61 difopn
 |-  ( ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) /\ { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( -u _pi (,) _pi ) \ { 0 } ) e. ( topGen ` ran (,) ) )
63 33 59 62 mp2an
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) e. ( topGen ` ran (,) )
64 63 a1i
 |-  ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) e. ( topGen ` ran (,) ) )
65 51 53 54 55 20 57 56 64 dvmptres
 |-  ( T. -> ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) )
66 65 mptru
 |-  ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 )
67 66 eqcomi
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
68 67 dmeqi
 |-  dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
69 49 68 eqtr3i
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
70 69 eqimssi
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
71 70 a1i
 |-  ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) )
72 fvex
 |-  ( cos ` ( x / 2 ) ) e. _V
73 eqid
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) )
74 72 73 dmmpti
 |-  dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( ( -u _pi (,) _pi ) \ { 0 } )
75 2cnd
 |-  ( ( T. /\ x e. RR ) -> 2 e. CC )
76 53 halfcld
 |-  ( ( T. /\ x e. RR ) -> ( x / 2 ) e. CC )
77 76 sincld
 |-  ( ( T. /\ x e. RR ) -> ( sin ` ( x / 2 ) ) e. CC )
78 75 77 mulcld
 |-  ( ( T. /\ x e. RR ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
79 76 coscld
 |-  ( ( T. /\ x e. RR ) -> ( cos ` ( x / 2 ) ) e. CC )
80 2cnd
 |-  ( x e. RR -> 2 e. CC )
81 2ne0
 |-  2 =/= 0
82 81 a1i
 |-  ( x e. RR -> 2 =/= 0 )
83 52 80 82 divrec2d
 |-  ( x e. RR -> ( x / 2 ) = ( ( 1 / 2 ) x. x ) )
84 83 fveq2d
 |-  ( x e. RR -> ( sin ` ( x / 2 ) ) = ( sin ` ( ( 1 / 2 ) x. x ) ) )
85 84 oveq2d
 |-  ( x e. RR -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
86 85 mpteq2ia
 |-  ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
87 86 oveq2i
 |-  ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
88 resmpt
 |-  ( RR C_ CC -> ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
89 12 88 ax-mp
 |-  ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
90 89 eqcomi
 |-  ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) = ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR )
91 90 oveq2i
 |-  ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( RR _D ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) )
92 eqid
 |-  ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
93 2cnd
 |-  ( x e. CC -> 2 e. CC )
94 halfcn
 |-  ( 1 / 2 ) e. CC
95 94 a1i
 |-  ( x e. CC -> ( 1 / 2 ) e. CC )
96 id
 |-  ( x e. CC -> x e. CC )
97 95 96 mulcld
 |-  ( x e. CC -> ( ( 1 / 2 ) x. x ) e. CC )
98 97 sincld
 |-  ( x e. CC -> ( sin ` ( ( 1 / 2 ) x. x ) ) e. CC )
99 93 98 mulcld
 |-  ( x e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
100 92 99 fmpti
 |-  ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) : CC --> CC
101 eqid
 |-  ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
102 2cn
 |-  2 e. CC
103 102 94 mulcli
 |-  ( 2 x. ( 1 / 2 ) ) e. CC
104 103 a1i
 |-  ( x e. CC -> ( 2 x. ( 1 / 2 ) ) e. CC )
105 97 coscld
 |-  ( x e. CC -> ( cos ` ( ( 1 / 2 ) x. x ) ) e. CC )
106 104 105 mulcld
 |-  ( x e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
107 106 adantl
 |-  ( ( T. /\ x e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
108 101 107 dmmptd
 |-  ( T. -> dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC )
109 108 mptru
 |-  dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC
110 12 109 sseqtrri
 |-  RR C_ dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
111 dvasinbx
 |-  ( ( 2 e. CC /\ ( 1 / 2 ) e. CC ) -> ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) )
112 102 94 111 mp2an
 |-  ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
113 112 dmeqi
 |-  dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
114 110 113 sseqtrri
 |-  RR C_ dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
115 dvcnre
 |-  ( ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) : CC --> CC /\ RR C_ dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) ) -> ( RR _D ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) ) = ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR ) )
116 100 114 115 mp2an
 |-  ( RR _D ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) ) = ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR )
117 112 reseq1i
 |-  ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR ) = ( ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR )
118 resmpt
 |-  ( RR C_ CC -> ( ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) )
119 12 118 ax-mp
 |-  ( ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
120 102 81 recidi
 |-  ( 2 x. ( 1 / 2 ) ) = 1
121 120 a1i
 |-  ( x e. RR -> ( 2 x. ( 1 / 2 ) ) = 1 )
122 83 eqcomd
 |-  ( x e. RR -> ( ( 1 / 2 ) x. x ) = ( x / 2 ) )
123 122 fveq2d
 |-  ( x e. RR -> ( cos ` ( ( 1 / 2 ) x. x ) ) = ( cos ` ( x / 2 ) ) )
124 121 123 oveq12d
 |-  ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( 1 x. ( cos ` ( x / 2 ) ) ) )
125 52 halfcld
 |-  ( x e. RR -> ( x / 2 ) e. CC )
126 125 coscld
 |-  ( x e. RR -> ( cos ` ( x / 2 ) ) e. CC )
127 126 mulid2d
 |-  ( x e. RR -> ( 1 x. ( cos ` ( x / 2 ) ) ) = ( cos ` ( x / 2 ) ) )
128 124 127 eqtrd
 |-  ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( cos ` ( x / 2 ) ) )
129 128 mpteq2ia
 |-  ( x e. RR |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
130 117 119 129 3eqtri
 |-  ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
131 91 116 130 3eqtri
 |-  ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
132 87 131 eqtri
 |-  ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
133 132 a1i
 |-  ( T. -> ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) ) )
134 51 78 79 133 20 57 56 64 dvmptres
 |-  ( T. -> ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) )
135 134 mptru
 |-  ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) )
136 135 eqcomi
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
137 136 dmeqi
 |-  dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
138 74 137 eqtr3i
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
139 138 eqimssi
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
140 139 a1i
 |-  ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) )
141 17 recnd
 |-  ( s e. ( -u _pi (,) _pi ) -> s e. CC )
142 141 ssriv
 |-  ( -u _pi (,) _pi ) C_ CC
143 142 a1i
 |-  ( T. -> ( -u _pi (,) _pi ) C_ CC )
144 ssid
 |-  CC C_ CC
145 144 a1i
 |-  ( T. -> CC C_ CC )
146 143 145 idcncfg
 |-  ( T. -> ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
147 146 mptru
 |-  ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC )
148 cnlimc
 |-  ( ( -u _pi (,) _pi ) C_ CC -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) ) ) )
149 142 148 ax-mp
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) ) )
150 147 149 mpbi
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) )
151 150 simpri
 |-  A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y )
152 fveq2
 |-  ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) = ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) )
153 oveq2
 |-  ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) = ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) )
154 152 153 eleq12d
 |-  ( y = 0 -> ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) ) )
155 154 rspccva
 |-  ( ( A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) /\ 0 e. ( -u _pi (,) _pi ) ) -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) )
156 151 44 155 mp2an
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 )
157 id
 |-  ( x = 0 -> x = 0 )
158 eqid
 |-  ( x e. ( -u _pi (,) _pi ) |-> x ) = ( x e. ( -u _pi (,) _pi ) |-> x )
159 c0ex
 |-  0 e. _V
160 157 158 159 fvmpt
 |-  ( 0 e. ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) = 0 )
161 44 160 ax-mp
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) = 0
162 elioore
 |-  ( x e. ( -u _pi (,) _pi ) -> x e. RR )
163 162 recnd
 |-  ( x e. ( -u _pi (,) _pi ) -> x e. CC )
164 158 163 fmpti
 |-  ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC
165 164 a1i
 |-  ( T. -> ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC )
166 165 limcdif
 |-  ( T. -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
167 166 mptru
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
168 resmpt
 |-  ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
169 16 168 ax-mp
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x )
170 169 oveq1i
 |-  ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 )
171 167 170 eqtri
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 )
172 156 161 171 3eltr3i
 |-  0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 )
173 172 a1i
 |-  ( T. -> 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 ) )
174 eqid
 |-  ( x e. CC |-> 2 ) = ( x e. CC |-> 2 )
175 144 a1i
 |-  ( 2 e. CC -> CC C_ CC )
176 2cnd
 |-  ( 2 e. CC -> 2 e. CC )
177 175 176 175 constcncfg
 |-  ( 2 e. CC -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
178 102 177 mp1i
 |-  ( T. -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
179 2cnd
 |-  ( ( T. /\ x e. ( -u _pi (,) _pi ) ) -> 2 e. CC )
180 174 178 143 145 179 cncfmptssg
 |-  ( T. -> ( x e. ( -u _pi (,) _pi ) |-> 2 ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
181 sincn
 |-  sin e. ( CC -cn-> CC )
182 181 a1i
 |-  ( T. -> sin e. ( CC -cn-> CC ) )
183 eqid
 |-  ( x e. CC |-> ( x / 2 ) ) = ( x e. CC |-> ( x / 2 ) )
184 183 divccncf
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC ) )
185 102 81 184 mp2an
 |-  ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC )
186 185 a1i
 |-  ( T. -> ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC ) )
187 163 adantl
 |-  ( ( T. /\ x e. ( -u _pi (,) _pi ) ) -> x e. CC )
188 187 halfcld
 |-  ( ( T. /\ x e. ( -u _pi (,) _pi ) ) -> ( x / 2 ) e. CC )
189 183 186 143 145 188 cncfmptssg
 |-  ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( x / 2 ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
190 182 189 cncfmpt1f
 |-  ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( sin ` ( x / 2 ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
191 180 190 mulcncf
 |-  ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
192 191 mptru
 |-  ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC )
193 cnlimc
 |-  ( ( -u _pi (,) _pi ) C_ CC -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) ) ) )
194 142 193 ax-mp
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) ) )
195 192 194 mpbi
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) )
196 195 simpri
 |-  A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y )
197 fveq2
 |-  ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) )
198 oveq2
 |-  ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) = ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) )
199 197 198 eleq12d
 |-  ( y = 0 -> ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) ) )
200 199 rspccva
 |-  ( ( A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) /\ 0 e. ( -u _pi (,) _pi ) ) -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) )
201 196 44 200 mp2an
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
202 oveq1
 |-  ( x = 0 -> ( x / 2 ) = ( 0 / 2 ) )
203 102 81 div0i
 |-  ( 0 / 2 ) = 0
204 202 203 eqtrdi
 |-  ( x = 0 -> ( x / 2 ) = 0 )
205 204 fveq2d
 |-  ( x = 0 -> ( sin ` ( x / 2 ) ) = ( sin ` 0 ) )
206 sin0
 |-  ( sin ` 0 ) = 0
207 205 206 eqtrdi
 |-  ( x = 0 -> ( sin ` ( x / 2 ) ) = 0 )
208 207 oveq2d
 |-  ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. 0 ) )
209 2t0e0
 |-  ( 2 x. 0 ) = 0
210 208 209 eqtrdi
 |-  ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = 0 )
211 eqid
 |-  ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) )
212 210 211 159 fvmpt
 |-  ( 0 e. ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) = 0 )
213 44 212 ax-mp
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) = 0
214 2cnd
 |-  ( x e. ( -u _pi (,) _pi ) -> 2 e. CC )
215 163 halfcld
 |-  ( x e. ( -u _pi (,) _pi ) -> ( x / 2 ) e. CC )
216 215 sincld
 |-  ( x e. ( -u _pi (,) _pi ) -> ( sin ` ( x / 2 ) ) e. CC )
217 214 216 mulcld
 |-  ( x e. ( -u _pi (,) _pi ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
218 211 217 fmpti
 |-  ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC
219 218 a1i
 |-  ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC )
220 219 limcdif
 |-  ( T. -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
221 220 mptru
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
222 resmpt
 |-  ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
223 16 222 ax-mp
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) )
224 223 oveq1i
 |-  ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
225 221 224 eqtri
 |-  ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
226 201 213 225 3eltr3i
 |-  0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
227 226 a1i
 |-  ( T. -> 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) )
228 eqidd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
229 oveq1
 |-  ( x = y -> ( x / 2 ) = ( y / 2 ) )
230 229 fveq2d
 |-  ( x = y -> ( sin ` ( x / 2 ) ) = ( sin ` ( y / 2 ) ) )
231 230 oveq2d
 |-  ( x = y -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
232 231 adantl
 |-  ( ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = y ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
233 id
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. ( ( -u _pi (,) _pi ) \ { 0 } ) )
234 26 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR )
235 19 sseli
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. RR )
236 235 rehalfcld
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) e. RR )
237 236 resincld
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) e. RR )
238 234 237 remulcld
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) e. RR )
239 228 232 233 238 fvmptd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
240 2cnd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. CC )
241 237 recnd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) e. CC )
242 81 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 =/= 0 )
243 ioossicc
 |-  ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi )
244 eldifi
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. ( -u _pi (,) _pi ) )
245 243 244 sseldi
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. ( -u _pi [,] _pi ) )
246 eldifsni
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y =/= 0 )
247 fourierdlem44
 |-  ( ( y e. ( -u _pi [,] _pi ) /\ y =/= 0 ) -> ( sin ` ( y / 2 ) ) =/= 0 )
248 245 246 247 syl2anc
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) =/= 0 )
249 240 241 242 248 mulne0d
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) =/= 0 )
250 239 249 eqnetrd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) =/= 0 )
251 250 neneqd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 )
252 251 nrex
 |-  -. E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0
253 25 fnmpt
 |-  ( A. x e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( 2 x. ( sin ` ( x / 2 ) ) ) e. RR -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } ) )
254 253 30 mprg
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } )
255 ssid
 |-  ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( ( -u _pi (,) _pi ) \ { 0 } )
256 fvelimab
 |-  ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( ( -u _pi (,) _pi ) \ { 0 } ) ) -> ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 ) )
257 254 255 256 mp2an
 |-  ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 )
258 252 257 mtbir
 |-  -. 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
259 258 a1i
 |-  ( T. -> -. 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) )
260 eqidd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) )
261 229 fveq2d
 |-  ( x = y -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
262 261 adantl
 |-  ( ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = y ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
263 235 recnd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. CC )
264 263 halfcld
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) e. CC )
265 264 coscld
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) e. CC )
266 260 262 233 265 fvmptd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = ( cos ` ( y / 2 ) ) )
267 236 rered
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) = ( y / 2 ) )
268 halfpire
 |-  ( _pi / 2 ) e. RR
269 268 renegcli
 |-  -u ( _pi / 2 ) e. RR
270 269 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR )
271 270 rexrd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR* )
272 268 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR )
273 272 rexrd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR* )
274 picn
 |-  _pi e. CC
275 divneg
 |-  ( ( _pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( _pi / 2 ) = ( -u _pi / 2 ) )
276 274 102 81 275 mp3an
 |-  -u ( _pi / 2 ) = ( -u _pi / 2 )
277 39 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR )
278 2rp
 |-  2 e. RR+
279 278 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR+ )
280 40 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR* )
281 41 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR* )
282 ioogtlb
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ y e. ( -u _pi (,) _pi ) ) -> -u _pi < y )
283 280 281 244 282 syl3anc
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi < y )
284 277 235 279 283 ltdiv1dd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( -u _pi / 2 ) < ( y / 2 ) )
285 276 284 eqbrtrid
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) < ( y / 2 ) )
286 38 a1i
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR )
287 iooltub
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ y e. ( -u _pi (,) _pi ) ) -> y < _pi )
288 280 281 244 287 syl3anc
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y < _pi )
289 235 286 279 288 ltdiv1dd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) < ( _pi / 2 ) )
290 271 273 236 285 289 eliood
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
291 267 290 eqeltrd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
292 cosne0
 |-  ( ( ( y / 2 ) e. CC /\ ( Re ` ( y / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( y / 2 ) ) =/= 0 )
293 264 291 292 syl2anc
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) =/= 0 )
294 266 293 eqnetrd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) =/= 0 )
295 294 neneqd
 |-  ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 )
296 295 nrex
 |-  -. E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0
297 72 73 fnmpti
 |-  ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } )
298 fvelimab
 |-  ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( ( -u _pi (,) _pi ) \ { 0 } ) ) -> ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 ) )
299 297 255 298 mp2an
 |-  ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 )
300 296 299 mtbir
 |-  -. 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
301 135 imaeq1i
 |-  ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
302 301 eleq2i
 |-  ( 0 e. ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) )
303 300 302 mtbir
 |-  -. 0 e. ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
304 303 a1i
 |-  ( T. -> -. 0 e. ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) )
305 eqid
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) )
306 eqid
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) )
307 19 sseli
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. RR )
308 307 recnd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. CC )
309 308 halfcld
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) e. CC )
310 309 coscld
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. CC )
311 307 rehalfcld
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) e. RR )
312 311 rered
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( s / 2 ) ) = ( s / 2 ) )
313 269 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR )
314 313 rexrd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR* )
315 268 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR )
316 315 rexrd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR* )
317 38 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR )
318 317 renegcld
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR )
319 278 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR+ )
320 40 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR* )
321 41 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR* )
322 eldifi
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. ( -u _pi (,) _pi ) )
323 ioogtlb
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ s e. ( -u _pi (,) _pi ) ) -> -u _pi < s )
324 320 321 322 323 syl3anc
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi < s )
325 318 307 319 324 ltdiv1dd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( -u _pi / 2 ) < ( s / 2 ) )
326 276 325 eqbrtrid
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) < ( s / 2 ) )
327 iooltub
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ s e. ( -u _pi (,) _pi ) ) -> s < _pi )
328 320 321 322 327 syl3anc
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s < _pi )
329 307 317 319 328 ltdiv1dd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) < ( _pi / 2 ) )
330 314 316 311 326 329 eliood
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
331 312 330 eqeltrd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( s / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
332 cosne0
 |-  ( ( ( s / 2 ) e. CC /\ ( Re ` ( s / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( s / 2 ) ) =/= 0 )
333 309 331 332 syl2anc
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) =/= 0 )
334 333 neneqd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) = 0 )
335 311 recoscld
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. RR )
336 elsng
 |-  ( ( cos ` ( s / 2 ) ) e. RR -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
337 335 336 syl
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
338 334 337 mtbird
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) e. { 0 } )
339 310 338 eldifd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
340 339 adantl
 |-  ( ( T. /\ s e. ( ( -u _pi (,) _pi ) \ { 0 } ) ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
341 309 ad2antrl
 |-  ( ( T. /\ ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( s / 2 ) =/= 0 ) ) -> ( s / 2 ) e. CC )
342 cosf
 |-  cos : CC --> CC
343 342 a1i
 |-  ( T. -> cos : CC --> CC )
344 343 ffvelrnda
 |-  ( ( T. /\ x e. CC ) -> ( cos ` x ) e. CC )
345 eqid
 |-  ( s e. CC |-> ( s / 2 ) ) = ( s e. CC |-> ( s / 2 ) )
346 345 divccncf
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC ) )
347 102 81 346 mp2an
 |-  ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC )
348 347 a1i
 |-  ( T. -> ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC ) )
349 141 adantl
 |-  ( ( T. /\ s e. ( -u _pi (,) _pi ) ) -> s e. CC )
350 349 halfcld
 |-  ( ( T. /\ s e. ( -u _pi (,) _pi ) ) -> ( s / 2 ) e. CC )
351 345 348 143 145 350 cncfmptssg
 |-  ( T. -> ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
352 oveq1
 |-  ( s = 0 -> ( s / 2 ) = ( 0 / 2 ) )
353 352 203 eqtrdi
 |-  ( s = 0 -> ( s / 2 ) = 0 )
354 351 45 353 cnmptlimc
 |-  ( T. -> 0 e. ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) )
355 eqid
 |-  ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) = ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) )
356 141 halfcld
 |-  ( s e. ( -u _pi (,) _pi ) -> ( s / 2 ) e. CC )
357 355 356 fmpti
 |-  ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) : ( -u _pi (,) _pi ) --> CC
358 357 a1i
 |-  ( T. -> ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) : ( -u _pi (,) _pi ) --> CC )
359 358 limcdif
 |-  ( T. -> ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
360 359 mptru
 |-  ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
361 resmpt
 |-  ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) )
362 16 361 ax-mp
 |-  ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) )
363 362 oveq1i
 |-  ( ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) limCC 0 )
364 360 363 eqtri
 |-  ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) limCC 0 )
365 354 364 eleqtrdi
 |-  ( T. -> 0 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) limCC 0 ) )
366 ffn
 |-  ( cos : CC --> CC -> cos Fn CC )
367 342 366 ax-mp
 |-  cos Fn CC
368 dffn5
 |-  ( cos Fn CC <-> cos = ( x e. CC |-> ( cos ` x ) ) )
369 367 368 mpbi
 |-  cos = ( x e. CC |-> ( cos ` x ) )
370 coscn
 |-  cos e. ( CC -cn-> CC )
371 369 370 eqeltrri
 |-  ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC )
372 371 a1i
 |-  ( T. -> ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC ) )
373 0cnd
 |-  ( T. -> 0 e. CC )
374 fveq2
 |-  ( x = 0 -> ( cos ` x ) = ( cos ` 0 ) )
375 cos0
 |-  ( cos ` 0 ) = 1
376 374 375 eqtrdi
 |-  ( x = 0 -> ( cos ` x ) = 1 )
377 372 373 376 cnmptlimc
 |-  ( T. -> 1 e. ( ( x e. CC |-> ( cos ` x ) ) limCC 0 ) )
378 fveq2
 |-  ( x = ( s / 2 ) -> ( cos ` x ) = ( cos ` ( s / 2 ) ) )
379 fveq2
 |-  ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = ( cos ` 0 ) )
380 379 375 eqtrdi
 |-  ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = 1 )
381 380 ad2antll
 |-  ( ( T. /\ ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( s / 2 ) = 0 ) ) -> ( cos ` ( s / 2 ) ) = 1 )
382 341 344 365 377 378 381 limcco
 |-  ( T. -> 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) limCC 0 ) )
383 ax-1ne0
 |-  1 =/= 0
384 383 a1i
 |-  ( T. -> 1 =/= 0 )
385 305 306 340 382 384 reclimc
 |-  ( T. -> ( 1 / 1 ) e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) limCC 0 ) )
386 1div1e1
 |-  ( 1 / 1 ) = 1
387 66 fveq1i
 |-  ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) ` s )
388 eqidd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) )
389 eqidd
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> 1 = 1 )
390 id
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. ( ( -u _pi (,) _pi ) \ { 0 } ) )
391 1red
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 1 e. RR )
392 388 389 390 391 fvmptd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) ` s ) = 1 )
393 387 392 eqtr2id
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 1 = ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) )
394 135 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) )
395 oveq1
 |-  ( x = s -> ( x / 2 ) = ( s / 2 ) )
396 395 fveq2d
 |-  ( x = s -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
397 396 adantl
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
398 394 397 390 335 fvmptd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) = ( cos ` ( s / 2 ) ) )
399 398 eqcomd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) = ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) )
400 393 399 oveq12d
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 1 / ( cos ` ( s / 2 ) ) ) = ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) )
401 400 mpteq2ia
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) )
402 401 oveq1i
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) ) limCC 0 )
403 385 386 402 3eltr3g
 |-  ( T. -> 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) ) limCC 0 ) )
404 20 24 32 34 45 46 71 140 173 227 259 304 403 lhop
 |-  ( T. -> 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) limCC 0 ) )
405 404 mptru
 |-  1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) limCC 0 )
406 eqidd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
407 simpr
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> x = s )
408 406 407 390 307 fvmptd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) = s )
409 eqidd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
410 407 oveq1d
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( x / 2 ) = ( s / 2 ) )
411 410 fveq2d
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( sin ` ( x / 2 ) ) = ( sin ` ( s / 2 ) ) )
412 411 oveq2d
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
413 26 a1i
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR )
414 311 resincld
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) e. RR )
415 413 414 remulcld
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
416 409 412 390 415 fvmptd
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
417 408 416 oveq12d
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
418 417 mpteq2ia
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
419 418 oveq1i
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 )
420 405 419 eleqtri
 |-  1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 )
421 10 oveq1i
 |-  ( K limCC 0 ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
422 10 feq1i
 |-  ( K : ( -u _pi [,] _pi ) --> CC <-> ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi [,] _pi ) --> CC )
423 14 422 mpbi
 |-  ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi [,] _pi ) --> CC
424 423 a1i
 |-  ( T. -> ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi [,] _pi ) --> CC )
425 243 a1i
 |-  ( T. -> ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) )
426 iccssre
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
427 39 38 426 mp2an
 |-  ( -u _pi [,] _pi ) C_ RR
428 427 a1i
 |-  ( T. -> ( -u _pi [,] _pi ) C_ RR )
429 428 12 sstrdi
 |-  ( T. -> ( -u _pi [,] _pi ) C_ CC )
430 eqid
 |-  ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) )
431 39 35 36 ltleii
 |-  -u _pi <_ 0
432 35 38 37 ltleii
 |-  0 <_ _pi
433 39 38 elicc2i
 |-  ( 0 e. ( -u _pi [,] _pi ) <-> ( 0 e. RR /\ -u _pi <_ 0 /\ 0 <_ _pi ) )
434 35 431 432 433 mpbir3an
 |-  0 e. ( -u _pi [,] _pi )
435 159 snss
 |-  ( 0 e. ( -u _pi [,] _pi ) <-> { 0 } C_ ( -u _pi [,] _pi ) )
436 434 435 mpbi
 |-  { 0 } C_ ( -u _pi [,] _pi )
437 ssequn2
 |-  ( { 0 } C_ ( -u _pi [,] _pi ) <-> ( ( -u _pi [,] _pi ) u. { 0 } ) = ( -u _pi [,] _pi ) )
438 436 437 mpbi
 |-  ( ( -u _pi [,] _pi ) u. { 0 } ) = ( -u _pi [,] _pi )
439 438 oveq2i
 |-  ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) )
440 eqid
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
441 56 440 rerest
 |-  ( ( -u _pi [,] _pi ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) )
442 427 441 ax-mp
 |-  ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
443 439 442 eqtri
 |-  ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
444 443 fveq2i
 |-  ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) = ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) )
445 159 snss
 |-  ( 0 e. ( -u _pi (,) _pi ) <-> { 0 } C_ ( -u _pi (,) _pi ) )
446 44 445 mpbi
 |-  { 0 } C_ ( -u _pi (,) _pi )
447 ssequn2
 |-  ( { 0 } C_ ( -u _pi (,) _pi ) <-> ( ( -u _pi (,) _pi ) u. { 0 } ) = ( -u _pi (,) _pi ) )
448 446 447 mpbi
 |-  ( ( -u _pi (,) _pi ) u. { 0 } ) = ( -u _pi (,) _pi )
449 444 448 fveq12i
 |-  ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) ) = ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( -u _pi (,) _pi ) )
450 resttopon
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( -u _pi [,] _pi ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. ( TopOn ` ( -u _pi [,] _pi ) ) )
451 60 427 450 mp2an
 |-  ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. ( TopOn ` ( -u _pi [,] _pi ) )
452 451 topontopi
 |-  ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top
453 retop
 |-  ( topGen ` ran (,) ) e. Top
454 ovex
 |-  ( -u _pi [,] _pi ) e. _V
455 453 454 pm3.2i
 |-  ( ( topGen ` ran (,) ) e. Top /\ ( -u _pi [,] _pi ) e. _V )
456 ssid
 |-  ( -u _pi (,) _pi ) C_ ( -u _pi (,) _pi )
457 33 243 456 3pm3.2i
 |-  ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi (,) _pi ) )
458 restopnb
 |-  ( ( ( ( topGen ` ran (,) ) e. Top /\ ( -u _pi [,] _pi ) e. _V ) /\ ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi (,) _pi ) ) ) -> ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) <-> ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) )
459 455 457 458 mp2an
 |-  ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) <-> ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) )
460 33 459 mpbi
 |-  ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
461 isopn3i
 |-  ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi ) )
462 452 460 461 mp2an
 |-  ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi )
463 eqid
 |-  ( -u _pi (,) _pi ) = ( -u _pi (,) _pi )
464 449 462 463 3eqtrri
 |-  ( -u _pi (,) _pi ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) )
465 44 464 eleqtri
 |-  0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) )
466 465 a1i
 |-  ( T. -> 0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) ) )
467 424 425 429 56 430 466 limcres
 |-  ( T. -> ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) )
468 467 mptru
 |-  ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
469 468 eqcomi
 |-  ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) = ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 )
470 resmpt
 |-  ( ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) -> ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) = ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
471 243 470 ax-mp
 |-  ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) = ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
472 471 oveq1i
 |-  ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 ) = ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
473 421 469 472 3eqtri
 |-  ( K limCC 0 ) = ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
474 eqid
 |-  ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
475 iftrue
 |-  ( s = 0 -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = 1 )
476 1cnd
 |-  ( s = 0 -> 1 e. CC )
477 475 476 eqeltrd
 |-  ( s = 0 -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
478 477 adantl
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ s = 0 ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
479 iffalse
 |-  ( -. s = 0 -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
480 479 adantl
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
481 141 adantr
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> s e. CC )
482 2cnd
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> 2 e. CC )
483 481 halfcld
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( s / 2 ) e. CC )
484 483 sincld
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( sin ` ( s / 2 ) ) e. CC )
485 482 484 mulcld
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
486 81 a1i
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> 2 =/= 0 )
487 243 sseli
 |-  ( s e. ( -u _pi (,) _pi ) -> s e. ( -u _pi [,] _pi ) )
488 neqne
 |-  ( -. s = 0 -> s =/= 0 )
489 fourierdlem44
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
490 487 488 489 syl2an
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
491 482 484 486 490 mulne0d
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
492 481 485 491 divcld
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. CC )
493 480 492 eqeltrd
 |-  ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
494 478 493 pm2.61dan
 |-  ( s e. ( -u _pi (,) _pi ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
495 474 494 fmpti
 |-  ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi (,) _pi ) --> CC
496 495 a1i
 |-  ( T. -> ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi (,) _pi ) --> CC )
497 496 limcdif
 |-  ( T. -> ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
498 497 mptru
 |-  ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
499 resmpt
 |-  ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
500 16 499 ax-mp
 |-  ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
501 eldifn
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. s e. { 0 } )
502 velsn
 |-  ( s e. { 0 } <-> s = 0 )
503 501 502 sylnib
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. s = 0 )
504 503 479 syl
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
505 504 mpteq2ia
 |-  ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
506 500 505 eqtri
 |-  ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
507 506 oveq1i
 |-  ( ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 )
508 473 498 507 3eqtrri
 |-  ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 ) = ( K limCC 0 )
509 420 508 eleqtri
 |-  1 e. ( K limCC 0 )
510 509 a1i
 |-  ( s = 0 -> 1 e. ( K limCC 0 ) )
511 fveq2
 |-  ( s = 0 -> ( K ` s ) = ( K ` 0 ) )
512 475 10 47 fvmpt
 |-  ( 0 e. ( -u _pi [,] _pi ) -> ( K ` 0 ) = 1 )
513 434 512 ax-mp
 |-  ( K ` 0 ) = 1
514 511 513 eqtrdi
 |-  ( s = 0 -> ( K ` s ) = 1 )
515 oveq2
 |-  ( s = 0 -> ( K limCC s ) = ( K limCC 0 ) )
516 510 514 515 3eltr4d
 |-  ( s = 0 -> ( K ` s ) e. ( K limCC s ) )
517 427 12 sstri
 |-  ( -u _pi [,] _pi ) C_ CC
518 517 a1i
 |-  ( s = 0 -> ( -u _pi [,] _pi ) C_ CC )
519 38 a1i
 |-  ( s = 0 -> _pi e. RR )
520 519 renegcld
 |-  ( s = 0 -> -u _pi e. RR )
521 id
 |-  ( s = 0 -> s = 0 )
522 35 a1i
 |-  ( s = 0 -> 0 e. RR )
523 521 522 eqeltrd
 |-  ( s = 0 -> s e. RR )
524 431 521 breqtrrid
 |-  ( s = 0 -> -u _pi <_ s )
525 521 432 eqbrtrdi
 |-  ( s = 0 -> s <_ _pi )
526 520 519 523 524 525 eliccd
 |-  ( s = 0 -> s e. ( -u _pi [,] _pi ) )
527 57 oveq1i
 |-  ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -u _pi [,] _pi ) )
528 56 cnfldtop
 |-  ( TopOpen ` CCfld ) e. Top
529 reex
 |-  RR e. _V
530 restabs
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( -u _pi [,] _pi ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -u _pi [,] _pi ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) ) )
531 528 427 529 530 mp3an
 |-  ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -u _pi [,] _pi ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) )
532 527 531 eqtri
 |-  ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) )
533 56 532 cnplimc
 |-  ( ( ( -u _pi [,] _pi ) C_ CC /\ s e. ( -u _pi [,] _pi ) ) -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ ( K ` s ) e. ( K limCC s ) ) ) )
534 518 526 533 syl2anc
 |-  ( s = 0 -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ ( K ` s ) e. ( K limCC s ) ) ) )
535 15 516 534 mpbir2and
 |-  ( s = 0 -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
536 535 adantl
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s = 0 ) -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
537 simpl
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( -u _pi [,] _pi ) )
538 502 notbii
 |-  ( -. s e. { 0 } <-> -. s = 0 )
539 538 biimpri
 |-  ( -. s = 0 -> -. s e. { 0 } )
540 539 adantl
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> -. s e. { 0 } )
541 537 540 eldifd
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( -u _pi [,] _pi ) \ { 0 } ) )
542 fveq2
 |-  ( x = s -> ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) = ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
543 542 eleq2d
 |-  ( x = s -> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
544 429 ssdifssd
 |-  ( T. -> ( ( -u _pi [,] _pi ) \ { 0 } ) C_ CC )
545 544 145 idcncfg
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> s ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
546 eqid
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
547 2cnd
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> 2 e. CC )
548 eldifi
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s e. ( -u _pi [,] _pi ) )
549 517 548 sseldi
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s e. CC )
550 549 halfcld
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( s / 2 ) e. CC )
551 550 sincld
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) e. CC )
552 547 551 mulcld
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
553 81 a1i
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> 2 =/= 0 )
554 eldifsni
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s =/= 0 )
555 548 554 489 syl2anc
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) =/= 0 )
556 547 551 553 555 mulne0d
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
557 556 neneqd
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 )
558 elsng
 |-  ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
559 552 558 syl
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
560 557 559 mtbird
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } )
561 552 560 eldifd
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
562 546 561 fmpti
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> ( CC \ { 0 } )
563 difss
 |-  ( CC \ { 0 } ) C_ CC
564 eqid
 |-  ( s e. CC |-> 2 ) = ( s e. CC |-> 2 )
565 175 176 175 constcncfg
 |-  ( 2 e. CC -> ( s e. CC |-> 2 ) e. ( CC -cn-> CC ) )
566 102 565 mp1i
 |-  ( T. -> ( s e. CC |-> 2 ) e. ( CC -cn-> CC ) )
567 2cnd
 |-  ( ( T. /\ s e. ( ( -u _pi [,] _pi ) \ { 0 } ) ) -> 2 e. CC )
568 564 566 544 145 567 cncfmptssg
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> 2 ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
569 549 547 553 divrecd
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( s / 2 ) = ( s x. ( 1 / 2 ) ) )
570 569 mpteq2ia
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / 2 ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s x. ( 1 / 2 ) ) )
571 eqid
 |-  ( s e. CC |-> ( 1 / 2 ) ) = ( s e. CC |-> ( 1 / 2 ) )
572 144 a1i
 |-  ( ( 1 / 2 ) e. CC -> CC C_ CC )
573 id
 |-  ( ( 1 / 2 ) e. CC -> ( 1 / 2 ) e. CC )
574 572 573 572 constcncfg
 |-  ( ( 1 / 2 ) e. CC -> ( s e. CC |-> ( 1 / 2 ) ) e. ( CC -cn-> CC ) )
575 94 574 mp1i
 |-  ( T. -> ( s e. CC |-> ( 1 / 2 ) ) e. ( CC -cn-> CC ) )
576 94 a1i
 |-  ( ( T. /\ s e. ( ( -u _pi [,] _pi ) \ { 0 } ) ) -> ( 1 / 2 ) e. CC )
577 571 575 544 145 576 cncfmptssg
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 1 / 2 ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
578 545 577 mulcncf
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s x. ( 1 / 2 ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
579 570 578 eqeltrid
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / 2 ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
580 182 579 cncfmpt1f
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( sin ` ( s / 2 ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
581 568 580 mulcncf
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
582 581 mptru
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC )
583 cncffvrn
 |-  ( ( ( CC \ { 0 } ) C_ CC /\ ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) ) -> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) ) <-> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> ( CC \ { 0 } ) ) )
584 563 582 583 mp2an
 |-  ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) ) <-> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> ( CC \ { 0 } ) )
585 562 584 mpbir
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) )
586 585 a1i
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) ) )
587 545 586 divcncf
 |-  ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
588 587 mptru
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC )
589 428 ssdifssd
 |-  ( T. -> ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR )
590 589 mptru
 |-  ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR
591 590 12 sstri
 |-  ( ( -u _pi [,] _pi ) \ { 0 } ) C_ CC
592 57 oveq1i
 |-  ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
593 restabs
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
594 528 590 529 593 mp3an
 |-  ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
595 592 594 eqtri
 |-  ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
596 unicntop
 |-  CC = U. ( TopOpen ` CCfld )
597 596 restid
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
598 528 597 ax-mp
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
599 598 eqcomi
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
600 56 595 599 cncfcn
 |-  ( ( ( ( -u _pi [,] _pi ) \ { 0 } ) C_ CC /\ CC C_ CC ) -> ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) )
601 591 144 600 mp2an
 |-  ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) )
602 588 601 eleqtri
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) )
603 resttopon
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( TopOn ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
604 60 590 603 mp2an
 |-  ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( TopOn ` ( ( -u _pi [,] _pi ) \ { 0 } ) )
605 56 cnfldtopon
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
606 cncnp
 |-  ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( TopOn ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> CC /\ A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) ) ) )
607 604 605 606 mp2an
 |-  ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> CC /\ A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) ) )
608 602 607 mpbi
 |-  ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> CC /\ A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) )
609 608 simpri
 |-  A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x )
610 543 609 vtoclri
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
611 541 610 syl
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
612 10 reseq1i
 |-  ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi [,] _pi ) \ { 0 } ) )
613 difss
 |-  ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi )
614 resmpt
 |-  ( ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) -> ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
615 613 614 ax-mp
 |-  ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
616 eldifn
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. s e. { 0 } )
617 616 502 sylnib
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. s = 0 )
618 617 479 syl
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
619 618 mpteq2ia
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
620 612 615 619 3eqtri
 |-  ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
621 restabs
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) /\ ( -u _pi [,] _pi ) e. _V ) -> ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
622 453 613 454 621 mp3an
 |-  ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
623 622 oveq1i
 |-  ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) )
624 623 fveq1i
 |-  ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) = ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s )
625 611 620 624 3eltr4g
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
626 452 613 pm3.2i
 |-  ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) )
627 626 a1i
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) ) )
628 ssdif
 |-  ( ( -u _pi [,] _pi ) C_ RR -> ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( RR \ { 0 } ) )
629 427 628 ax-mp
 |-  ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( RR \ { 0 } )
630 629 541 sseldi
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( RR \ { 0 } ) )
631 sscon
 |-  ( { 0 } C_ ( -u _pi [,] _pi ) -> ( RR \ ( -u _pi [,] _pi ) ) C_ ( RR \ { 0 } ) )
632 436 631 ax-mp
 |-  ( RR \ ( -u _pi [,] _pi ) ) C_ ( RR \ { 0 } )
633 629 632 unssi
 |-  ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) C_ ( RR \ { 0 } )
634 simpr
 |-  ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( -u _pi [,] _pi ) )
635 eldifn
 |-  ( s e. ( RR \ { 0 } ) -> -. s e. { 0 } )
636 635 adantr
 |-  ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> -. s e. { 0 } )
637 634 636 eldifd
 |-  ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( ( -u _pi [,] _pi ) \ { 0 } ) )
638 elun1
 |-  ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
639 637 638 syl
 |-  ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
640 eldifi
 |-  ( s e. ( RR \ { 0 } ) -> s e. RR )
641 640 adantr
 |-  ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> s e. RR )
642 simpr
 |-  ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> -. s e. ( -u _pi [,] _pi ) )
643 641 642 eldifd
 |-  ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> s e. ( RR \ ( -u _pi [,] _pi ) ) )
644 elun2
 |-  ( s e. ( RR \ ( -u _pi [,] _pi ) ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
645 643 644 syl
 |-  ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
646 639 645 pm2.61dan
 |-  ( s e. ( RR \ { 0 } ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
647 646 ssriv
 |-  ( RR \ { 0 } ) C_ ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) )
648 633 647 eqssi
 |-  ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) = ( RR \ { 0 } )
649 648 fveq2i
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( RR \ { 0 } ) )
650 61 cldopn
 |-  ( { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ { 0 } ) e. ( topGen ` ran (,) ) )
651 59 650 ax-mp
 |-  ( RR \ { 0 } ) e. ( topGen ` ran (,) )
652 isopn3i
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( RR \ { 0 } ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( RR \ { 0 } ) ) = ( RR \ { 0 } ) )
653 453 651 652 mp2an
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( RR \ { 0 } ) ) = ( RR \ { 0 } )
654 649 653 eqtri
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) = ( RR \ { 0 } )
655 630 654 eleqtrrdi
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) )
656 655 537 elind
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) i^i ( -u _pi [,] _pi ) ) )
657 eqid
 |-  ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
658 61 657 restntr
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -u _pi [,] _pi ) C_ RR /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) ) -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) i^i ( -u _pi [,] _pi ) ) )
659 453 427 613 658 mp3an
 |-  ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) i^i ( -u _pi [,] _pi ) )
660 656 659 eleqtrrdi
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
661 14 a1i
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> K : ( -u _pi [,] _pi ) --> CC )
662 451 toponunii
 |-  ( -u _pi [,] _pi ) = U. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
663 662 596 cnprest
 |-  ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) ) /\ ( s e. ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) /\ K : ( -u _pi [,] _pi ) --> CC ) ) -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
664 627 660 661 663 syl12anc
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
665 625 664 mpbird
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
666 536 665 pm2.61dan
 |-  ( s e. ( -u _pi [,] _pi ) -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
667 666 rgen
 |-  A. s e. ( -u _pi [,] _pi ) K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s )
668 cncnp
 |-  ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. ( TopOn ` ( -u _pi [,] _pi ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( K e. ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ A. s e. ( -u _pi [,] _pi ) K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) ) )
669 451 605 668 mp2an
 |-  ( K e. ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ A. s e. ( -u _pi [,] _pi ) K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
670 14 667 669 mpbir2an
 |-  K e. ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) )
671 56 532 599 cncfcn
 |-  ( ( ( -u _pi [,] _pi ) C_ CC /\ CC C_ CC ) -> ( ( -u _pi [,] _pi ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) )
672 517 144 671 mp2an
 |-  ( ( -u _pi [,] _pi ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) )
673 672 eqcomi
 |-  ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) = ( ( -u _pi [,] _pi ) -cn-> CC )
674 670 673 eleqtri
 |-  K e. ( ( -u _pi [,] _pi ) -cn-> CC )
675 cncffvrn
 |-  ( ( RR C_ CC /\ K e. ( ( -u _pi [,] _pi ) -cn-> CC ) ) -> ( K e. ( ( -u _pi [,] _pi ) -cn-> RR ) <-> K : ( -u _pi [,] _pi ) --> RR ) )
676 12 674 675 mp2an
 |-  ( K e. ( ( -u _pi [,] _pi ) -cn-> RR ) <-> K : ( -u _pi [,] _pi ) --> RR )
677 11 676 mpbir
 |-  K e. ( ( -u _pi [,] _pi ) -cn-> RR )