Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem62 Structured version   Unicode version

Theorem fourierdlem62 31792
Description: The function  K is continuous (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
fourierdlem62.k  |-  K  =  ( y  e.  (
-u pi [,] pi )  |->  if ( y  =  0 ,  1 ,  ( y  / 
( 2  x.  ( sin `  ( y  / 
2 ) ) ) ) ) )
Assertion
Ref Expression
fourierdlem62  |-  K  e.  ( ( -u pi [,] pi ) -cn-> RR )

Proof of Theorem fourierdlem62
Dummy variables  s  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem62.k . . . 4  |-  K  =  ( y  e.  (
-u pi [,] pi )  |->  if ( y  =  0 ,  1 ,  ( y  / 
( 2  x.  ( sin `  ( y  / 
2 ) ) ) ) ) )
2 eqeq1 2471 . . . . . 6  |-  ( y  =  s  ->  (
y  =  0  <->  s  =  0 ) )
3 eqidd 2468 . . . . . 6  |-  ( y  =  s  ->  1  =  1 )
4 id 22 . . . . . . 7  |-  ( y  =  s  ->  y  =  s )
5 oveq1 6302 . . . . . . . . 9  |-  ( y  =  s  ->  (
y  /  2 )  =  ( s  / 
2 ) )
65fveq2d 5876 . . . . . . . 8  |-  ( y  =  s  ->  ( sin `  ( y  / 
2 ) )  =  ( sin `  (
s  /  2 ) ) )
76oveq2d 6311 . . . . . . 7  |-  ( y  =  s  ->  (
2  x.  ( sin `  ( y  /  2
) ) )  =  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )
84, 7oveq12d 6313 . . . . . 6  |-  ( y  =  s  ->  (
y  /  ( 2  x.  ( sin `  (
y  /  2 ) ) ) )  =  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
92, 3, 8ifeq123d 31337 . . . . 5  |-  ( y  =  s  ->  if ( y  =  0 ,  1 ,  ( y  /  ( 2  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
109cbvmptv 4544 . . . 4  |-  ( 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 ) ) ) ) ) )
111, 10eqtri 2496 . . 3  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
1211fourierdlem43 31773 . 2  |-  K :
( -u pi [,] pi )
--> RR
13 ax-resscn 9561 . . 3  |-  RR  C_  CC
14 fss 5745 . . . . . 6  |-  ( ( K : ( -u pi [,] pi ) --> RR 
/\  RR  C_  CC )  ->  K : (
-u pi [,] pi )
--> CC )
1512, 13, 14mp2an 672 . . . . 5  |-  K :
( -u pi [,] pi )
--> CC
1615a1i 11 . . . . . . . . . 10  |-  ( s  =  0  ->  K : ( -u pi [,] pi ) --> CC )
17 difss 3636 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  ( -u pi (,) pi )
18 elioore 11571 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( -u pi (,) pi )  ->  s  e.  RR )
1918ssriv 3513 . . . . . . . . . . . . . . . . . 18  |-  ( -u pi (,) pi )  C_  RR
2017, 19sstri 3518 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  RR
2120a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  C_  RR )
22 eqid 2467 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x )
2320sseli 3505 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  x  e.  RR )
2422, 23fmpti 6055 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) : ( ( -u pi (,) pi )  \  { 0 } ) --> RR
2524a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  x ) : ( ( -u pi (,) pi )  \  { 0 } ) --> RR )
26 eqid 2467 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) )
27 2re 10617 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
2827a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR )
29 rehalfcl 10777 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  /  2 )  e.  RR )
3023, 29syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( x  / 
2 )  e.  RR )
31 resincl 13753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  /  2 )  e.  RR  ->  ( sin `  ( x  / 
2 ) )  e.  RR )
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
x  /  2 ) )  e.  RR )
3328, 32jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  e.  RR  /\  ( sin `  ( x  /  2
) )  e.  RR ) )
34 remulcl 9589 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  e.  RR  /\  ( sin `  ( x  /  2 ) )  e.  RR )  -> 
( 2  x.  ( sin `  ( x  / 
2 ) ) )  e.  RR )
3533, 34syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  x.  ( sin `  (
x  /  2 ) ) )  e.  RR )
3626, 35fmpti 6055 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) : ( (
-u pi (,) pi )  \  { 0 } ) --> RR
3736a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) : ( ( -u pi (,) pi )  \  {
0 } ) --> RR )
38 iooretop 21141 . . . . . . . . . . . . . . . . 17  |-  ( -u pi (,) pi )  e.  ( topGen `  ran  (,) )
3938a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( -u pi (,) pi )  e.  ( topGen `
 ran  (,) )
)
40 0re 9608 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
41 negpilt0 31362 . . . . . . . . . . . . . . . . . . 19  |-  -u pi  <  0
42 pipos 22720 . . . . . . . . . . . . . . . . . . 19  |-  0  <  pi
4340, 41, 423pm3.2i 1174 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  /\  -u pi  <  0  /\  0  < 
pi )
44 pire 22718 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  e.  RR
4544renegcli 9892 . . . . . . . . . . . . . . . . . . . 20  |-  -u pi  e.  RR
4645rexri 9658 . . . . . . . . . . . . . . . . . . 19  |-  -u pi  e.  RR*
4744rexri 9658 . . . . . . . . . . . . . . . . . . 19  |-  pi  e.  RR*
48 elioo2 11582 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR* )  ->  ( 0  e.  (
-u pi (,) pi ) 
<->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <  pi ) ) )
4946, 47, 48mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  ( -u pi (,) pi )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  < 
pi ) )
5043, 49mpbir 209 . . . . . . . . . . . . . . . . 17  |-  0  e.  ( -u pi (,) pi )
5150a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  0  e.  ( -u pi (,) pi ) )
52 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  ( (
-u pi (,) pi )  \  { 0 } )
53 1ex 9603 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  _V
54 eqid 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  1 )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )
5553, 54dmmpti 5716 . . . . . . . . . . . . . . . . . . . 20  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )  =  ( ( -u pi (,) pi )  \  {
0 } )
5655eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )
57 reex 9595 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  RR  e.  _V
5857prid1 4141 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  RR  e.  { RR ,  CC }
5958a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  RR  e.  { RR ,  CC } )
6013sseli 3505 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  x  e.  CC )
6160adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T.  /\  x  e.  RR )  ->  x  e.  CC )
62 1re 9607 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  RR
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T.  /\  x  e.  RR )  ->  1  e.  RR )
6459dvmptid 22228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  x ) )  =  ( x  e.  RR  |->  1 ) )
65 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6665tgioo2 21176 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
67 sncldre 31338 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0  e.  RR  ->  { 0 }  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
6840, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { 0 }  e.  ( Clsd `  ( topGen `  ran  (,) )
)
69 retopon 21138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( topGen ` 
ran  (,) )  e.  (TopOn `  RR )
7069toponunii 19302 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  RR  =  U. ( topGen `  ran  (,) )
7170difopn 19403 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( -u pi (,) pi )  e.  ( topGen `
 ran  (,) )  /\  { 0 }  e.  ( Clsd `  ( topGen ` 
ran  (,) ) ) )  ->  ( ( -u pi (,) pi )  \  { 0 } )  e.  ( topGen `  ran  (,) ) )
7238, 68, 71mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
-u pi (,) pi )  \  { 0 } )  e.  ( topGen ` 
ran  (,) )
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  e.  ( topGen `  ran  (,) )
)
7459, 61, 63, 64, 21, 66, 65, 73dvmptres 22234 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  1 ) )
7574trud 1388 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )
7675eqcomi 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  1 )  =  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) )
7776dmeqi 5210 . . . . . . . . . . . . . . . . . . 19  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )  =  dom  ( RR  _D  ( x  e.  (
( -u pi (,) pi )  \  { 0 } )  |->  x ) )
7856, 77eqtri 2496 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  dom  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) )
7978eqimssi 3563 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  dom  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) )
8079a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  C_  dom  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x ) ) )
81 fvex 5882 . . . . . . . . . . . . . . . . . . . . 21  |-  ( cos `  ( x  /  2
) )  e.  _V
82 eqid 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) )
8381, 82dmmpti 5716 . . . . . . . . . . . . . . . . . . . 20  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) )  =  ( ( -u pi (,) pi )  \  { 0 } )
8483eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) )
85 2cn 10618 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  2  e.  CC
8685a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( T.  /\  x  e.  RR )  ->  2  e.  CC )
87 halfcl 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  CC  ->  (
x  /  2 )  e.  CC )
8861, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T.  /\  x  e.  RR )  ->  (
x  /  2 )  e.  CC )
89 sincl 13739 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  /  2 )  e.  CC  ->  ( sin `  ( x  / 
2 ) )  e.  CC )
9088, 89syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( T.  /\  x  e.  RR )  ->  ( sin `  ( x  / 
2 ) )  e.  CC )
9186, 90jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( T.  /\  x  e.  RR )  ->  (
2  e.  CC  /\  ( sin `  ( x  /  2 ) )  e.  CC ) )
92 mulcl 9588 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2  e.  CC  /\  ( sin `  ( x  /  2 ) )  e.  CC )  -> 
( 2  x.  ( sin `  ( x  / 
2 ) ) )  e.  CC )
9391, 92syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T.  /\  x  e.  RR )  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  e.  CC )
94 coscl 13740 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  /  2 )  e.  CC  ->  ( cos `  ( x  / 
2 ) )  e.  CC )
9588, 94syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T.  /\  x  e.  RR )  ->  ( cos `  ( x  / 
2 ) )  e.  CC )
9685a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  RR  ->  2  e.  CC )
97 2ne0 10640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  2  =/=  0
9897a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  RR  ->  2  =/=  0 )
9960, 96, 98divrec2d 10336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  (
x  /  2 )  =  ( ( 1  /  2 )  x.  x ) )
10099fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  RR  ->  ( sin `  ( x  / 
2 ) )  =  ( sin `  (
( 1  /  2
)  x.  x ) ) )
101100oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  RR  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) )
102101mpteq2ia 4535 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  =  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) )
103102oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( RR 
_D  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )  =  ( RR  _D  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) ) )
104 resmpt 5329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( RR  C_  CC  ->  ( (
x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) )  |`  RR )  =  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) ) )
10513, 104ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) )  |`  RR )  =  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) )
106105eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) )  =  ( ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) )  |`  RR )
107106oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) )
108 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) )  =  ( x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) )
10985a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  CC  ->  2  e.  CC )
11085, 97reccli 10286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 1  /  2 )  e.  CC
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  CC  ->  (
1  /  2 )  e.  CC )
112 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  CC  ->  x  e.  CC )
113111, 112mulcld 9628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  CC  ->  (
( 1  /  2
)  x.  x )  e.  CC )
114113sincld 13743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  CC  ->  ( sin `  ( ( 1  /  2 )  x.  x ) )  e.  CC )
115109, 114mulcld 9628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  CC  ->  (
2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) )  e.  CC )
116108, 115fmpti 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) ) : CC --> CC
117 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) ) )
11885, 110mulcli 9613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 2  x.  ( 1  / 
2 ) )  e.  CC
119118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  CC  ->  (
2  x.  ( 1  /  2 ) )  e.  CC )
120 coscl 13740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( 1  /  2
)  x.  x )  e.  CC  ->  ( cos `  ( ( 1  /  2 )  x.  x ) )  e.  CC )
121113, 120syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  CC  ->  ( cos `  ( ( 1  /  2 )  x.  x ) )  e.  CC )
122119, 121jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  e.  CC  ->  (
( 2  x.  (
1  /  2 ) )  e.  CC  /\  ( cos `  ( ( 1  /  2 )  x.  x ) )  e.  CC ) )
123 mulcl 9588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( 2  x.  (
1  /  2 ) )  e.  CC  /\  ( cos `  ( ( 1  /  2 )  x.  x ) )  e.  CC )  -> 
( ( 2  x.  ( 1  /  2
) )  x.  ( cos `  ( ( 1  /  2 )  x.  x ) ) )  e.  CC )
124122, 123syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  CC  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  e.  CC )
125124adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( T.  /\  x  e.  CC )  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  e.  CC )
126117, 125dmmptd 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( T. 
->  dom  ( x  e.  CC  |->  ( ( 2  x.  ( 1  / 
2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  x ) ) ) )  =  CC )
127126trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  dom  (
x  e.  CC  |->  ( ( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) ) )  =  CC
12813, 127sseqtr4i 3542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  RR  C_  dom  ( x  e.  CC  |->  ( ( 2  x.  ( 1  /  2
) )  x.  ( cos `  ( ( 1  /  2 )  x.  x ) ) ) )
129 dvasinbx 31573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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
) ) ) ) )
13085, 110, 129mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) )
131130dmeqi 5210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  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 ) ) ) )
132128, 131sseqtr4i 3542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  RR  C_  dom  ( CC  _D  (
x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) ) )
133 dvcnre 31567 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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 )
)
134116, 132, 133mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 )
135130reseq1i 5275 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 )
136 resmpt 5329 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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
) ) ) ) )
13713, 136ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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
) ) ) )
13885, 97recidi 10287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 2  x.  ( 1  / 
2 ) )  =  1
139138a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  RR  ->  (
2  x.  ( 1  /  2 ) )  =  1 )
14099eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  RR  ->  (
( 1  /  2
)  x.  x )  =  ( x  / 
2 ) )
141140fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  RR  ->  ( cos `  ( ( 1  /  2 )  x.  x ) )  =  ( cos `  (
x  /  2 ) ) )
142139, 141oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  =  ( 1  x.  ( cos `  ( x  / 
2 ) ) ) )
14360, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  RR  ->  (
x  /  2 )  e.  CC )
144143, 94syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  RR  ->  ( cos `  ( x  / 
2 ) )  e.  CC )
145144mulid2d 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  (
1  x.  ( cos `  ( x  /  2
) ) )  =  ( cos `  (
x  /  2 ) ) )
146142, 145eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  RR  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  =  ( cos `  (
x  /  2 ) ) )
147146mpteq2ia 4535 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  RR  |->  ( ( 2  x.  ( 1  /  2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  x ) ) ) )  =  ( x  e.  RR  |->  ( cos `  ( x  /  2 ) ) )
148135, 137, 1473eqtri 2500 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( CC  _D  ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) ) )  |`  RR )  =  ( x  e.  RR  |->  ( cos `  ( x  /  2 ) ) )
149107, 134, 1483eqtri 2500 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( RR 
_D  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) ) )  =  ( x  e.  RR  |->  ( cos `  (
x  /  2 ) ) )
150103, 149eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )  =  ( x  e.  RR  |->  ( cos `  (
x  /  2 ) ) )
151150a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )  =  ( x  e.  RR  |->  ( cos `  ( x  /  2
) ) ) )
15259, 93, 95, 151, 21, 66, 65, 73dvmptres 22234 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( cos `  ( x  /  2 ) ) ) )
153152trud 1388 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )
154153eqcomi 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )  =  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) )
155154dmeqi 5210 . . . . . . . . . . . . . . . . . . 19  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) )  =  dom  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )
15684, 155eqtri 2496 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  dom  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )
157156eqimssi 3563 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  dom  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )
158157a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  C_  dom  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) ) )
159 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  0  ->  x  =  0 )
160 eqid 2467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  |->  x )  =  ( x  e.  ( -u pi (,) pi )  |->  x )
16140elexi 3128 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
162159, 160, 161fvmpt 5957 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  ( -u pi (,) pi )  ->  (
( x  e.  (
-u pi (,) pi )  |->  x ) ` 
0 )  =  0 )
16350, 162ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) `  0 )  =  0
164163eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  0  =  ( ( x  e.  ( -u pi (,) pi )  |->  x ) `
 0 )
165 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  CC  |->  x )  =  ( x  e.  CC  |->  x )
166112ssriv 3513 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  CC  C_  CC
167 cncfmptid 21284 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( CC  C_  CC  /\  CC  C_  CC )  ->  (
x  e.  CC  |->  x )  e.  ( CC
-cn-> CC ) )
168166, 166, 167mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  CC  |->  x )  e.  ( CC -cn-> CC )
169168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( T. 
->  ( x  e.  CC  |->  x )  e.  ( CC -cn-> CC ) )
17013, 18sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  e.  ( -u pi (,) pi )  ->  s  e.  CC )
171170ssriv 3513 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -u pi (,) pi )  C_  CC
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( T. 
->  ( -u pi (,) pi )  C_  CC )
173166a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( T. 
->  CC  C_  CC )
17419sseli 3505 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  RR )
175174, 60syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  CC )
176175adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( T.  /\  x  e.  ( -u pi (,) pi ) )  ->  x  e.  CC )
177165, 169, 172, 173, 176cncfmptssg 31531 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  x )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
178177trud 1388 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  |->  x )  e.  ( ( -u pi (,) pi ) -cn-> CC )
179 cnlimc 22160 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
-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 ) lim CC  y ) ) ) )
180171, 179ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 ) lim
CC  y ) ) )
181178, 180mpbi 208 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) lim
CC  y ) )
182181simpri 462 . . . . . . . . . . . . . . . . . . . 20  |-  A. y  e.  ( -u pi (,) pi ) ( ( x  e.  ( -u pi (,) pi )  |->  x ) `
 y )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  y )
183 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  0  ->  (
( x  e.  (
-u pi (,) pi )  |->  x ) `  y )  =  ( ( x  e.  (
-u pi (,) pi )  |->  x ) ` 
0 ) )
184 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  0  ->  (
( x  e.  (
-u pi (,) pi )  |->  x ) lim CC  y )  =  ( ( x  e.  (
-u pi (,) pi )  |->  x ) lim CC  0 ) )
185183, 184eleq12d 2549 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  0  ->  (
( ( x  e.  ( -u pi (,) pi )  |->  x ) `
 y )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  y )  <->  ( (
x  e.  ( -u pi (,) pi )  |->  x ) `  0 )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  0 ) ) )
186185rspccva 3218 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. y  e.  (
-u pi (,) pi ) ( ( x  e.  ( -u pi (,) pi )  |->  x ) `
 y )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  y )  /\  0  e.  ( -u pi (,) pi ) )  -> 
( ( x  e.  ( -u pi (,) pi )  |->  x ) `
 0 )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  0 ) )
187182, 50, 186mp2an 672 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) `  0 )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  0 )
188164, 187eqeltri 2551 . . . . . . . . . . . . . . . . . 18  |-  0  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  0 )
189160, 175fmpti 6055 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  |->  x ) : ( -u pi (,) pi ) --> CC
190189a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  x ) : ( -u pi (,) pi ) --> CC )
191190limcdif 22148 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  0 )  =  ( ( ( x  e.  ( -u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 ) )
192191trud 1388 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim CC  0 )  =  ( ( ( x  e.  ( -u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) ) lim CC  0 )
193 resmpt 5329 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( -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 ) )
19417, 193ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x )
195194oveq1i 6305 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  (
-u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 )  =  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) lim CC  0 )
196192, 195eqtri 2496 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim CC  0 )  =  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) lim CC  0 )
197188, 196eleqtri 2553 . . . . . . . . . . . . . . . . 17  |-  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) lim CC  0 )
198197a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  0  e.  (
( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  x ) lim
CC  0 ) )
199 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  0  ->  (
x  /  2 )  =  ( 0  / 
2 ) )
20085, 97div0i 10290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  /  2 )  =  0
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  0  ->  (
0  /  2 )  =  0 )
202199, 201eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  0  ->  (
x  /  2 )  =  0 )
203202fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  0  ->  ( sin `  ( x  / 
2 ) )  =  ( sin `  0
) )
204 sin0 13762 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( sin `  0 )  =  0
205204a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  0  ->  ( sin `  0 )  =  0 )
206203, 205eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  0  ->  ( sin `  ( x  / 
2 ) )  =  0 )
207206oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  0  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  0 ) )
20885mul01i 9781 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2  x.  0 )  =  0
209208a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  0  ->  (
2  x.  0 )  =  0 )
210207, 209eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  0  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  0 )
211 eqid 2467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  =  ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )
212210, 211, 161fvmpt 5957 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  ( -u pi (,) pi )  ->  (
( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) ` 
0 )  =  0 )
21350, 212ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) `
 0 )  =  0
214213eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  0  =  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) ` 
0 )
215 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  CC  |->  2 )  =  ( x  e.  CC  |->  2 )
216166a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2  e.  CC  ->  CC  C_  CC )
21785a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2  e.  CC  ->  2  e.  CC )
218216, 217, 216constcncfg 31532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 2  e.  CC  ->  (
x  e.  CC  |->  2 )  e.  ( CC
-cn-> CC ) )
21985, 218ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  CC  |->  2 )  e.  ( CC -cn-> CC )
220219a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  ( x  e.  CC  |->  2 )  e.  ( CC -cn-> CC ) )
22185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T.  /\  x  e.  ( -u pi (,) pi ) )  ->  2  e.  CC )
222215, 220, 172, 173, 221cncfmptssg 31531 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  2 )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
223222trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( -u pi (,) pi )  |->  2 )  e.  ( ( -u pi (,) pi ) -cn-> CC )
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  2 )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
225 sincn 22706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  sin  e.  ( CC -cn-> CC )
226225a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  sin  e.  ( CC
-cn-> CC ) )
227 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  CC  |->  ( x  /  2 ) )  =  ( x  e.  CC  |->  ( x  / 
2 ) )
228227divccncf 21278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 2  e.  CC  /\  2  =/=  0 )  -> 
( x  e.  CC  |->  ( x  /  2
) )  e.  ( CC -cn-> CC ) )
22985, 97, 228mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  CC  |->  ( x  /  2 ) )  e.  ( CC -cn-> CC )
230229a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( T. 
->  ( x  e.  CC  |->  ( x  /  2
) )  e.  ( CC -cn-> CC ) )
231176, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( T.  /\  x  e.  ( -u pi (,) pi ) )  ->  (
x  /  2 )  e.  CC )
232227, 230, 172, 173, 231cncfmptssg 31531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( x  / 
2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
233232trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  ( -u pi (,) pi )  |->  ( x  /  2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC )
234233a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( x  / 
2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
235226, 234cncfmpt1f 21285 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( sin `  (
x  /  2 ) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
236235trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( -u pi (,) pi )  |->  ( sin `  ( x  /  2
) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC )
237236a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( sin `  (
x  /  2 ) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
238224, 237mulcncf 21727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
239238trud 1388 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC )
240 cnlimc 22160 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
-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 ) ) ) ) lim CC  y ) ) ) )
241171, 240ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 ) ) ) ) lim CC  y ) ) )
242239, 241mpbi 208 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) ) ) ) lim CC  y ) )
243242simpri 462 . . . . . . . . . . . . . . . . . . . 20  |-  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 ) ) ) ) lim CC  y )
244 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  0  ->  (
( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) `  y )  =  ( ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) ` 
0 ) )
245 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  0  ->  (
( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  y )  =  ( ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  0 ) )
246244, 245eleq12d 2549 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  0  ->  (
( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) `  y )  e.  ( ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  y )  <->  ( (
x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) `
 0 )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  0 ) ) )
247246rspccva 3218 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) ) ) lim CC  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 ) ) ) ) lim CC  0 ) )
248243, 50, 247mp2an 672 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) `
 0 )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  0 )
249214, 248eqeltri 2551 . . . . . . . . . . . . . . . . . 18  |-  0  e.  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  0 )
25085a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( -u pi (,) pi )  ->  2  e.  CC )
251175, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) pi )  ->  (
x  /  2 )  e.  CC )
252251, 89syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( -u pi (,) pi )  ->  ( sin `  ( x  / 
2 ) )  e.  CC )
253250, 252jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( -u pi (,) pi )  ->  (
2  e.  CC  /\  ( sin `  ( x  /  2 ) )  e.  CC ) )
254253, 92syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( -u pi (,) pi )  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  e.  CC )
255211, 254fmpti 6055 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) : ( -u pi (,) pi ) --> CC
256255a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) : ( -u pi (,) pi ) --> CC )
257256limcdif 22148 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  0 )  =  ( ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 ) )
258257trud 1388 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) lim
CC  0 )  =  ( ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 )
259 resmpt 5329 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( -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
) ) ) ) )
26017, 259ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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
) ) ) )
261260oveq1i 6305 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 )  =  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) lim
CC  0 )
262258, 261eqtri 2496 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) lim
CC  0 )  =  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) lim
CC  0 )
263249, 262eleqtri 2553 . . . . . . . . . . . . . . . . 17  |-  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) lim
CC  0 )
264263a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  0  e.  (
( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  0 ) )
265 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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
) ) ) ) )
266 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  y  ->  (
x  /  2 )  =  ( y  / 
2 ) )
267266fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  y  ->  ( sin `  ( x  / 
2 ) )  =  ( sin `  (
y  /  2 ) ) )
268267oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  ( sin `  ( y  / 
2 ) ) ) )
269268adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  y )  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  ( sin `  ( y  / 
2 ) ) ) )
270 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  ( ( -u pi (,) pi )  \  { 0 } ) )
27127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR )
27220sseli 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  RR )
273272rehalfcld 10797 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  e.  RR )
274 resincl 13753 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  /  2 )  e.  RR  ->  ( sin `  ( y  / 
2 ) )  e.  RR )
275273, 274syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
y  /  2 ) )  e.  RR )
276271, 275jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  e.  RR  /\  ( sin `  ( y  /  2
) )  e.  RR ) )
277 remulcl 9589 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2  e.  RR  /\  ( sin `  ( y  /  2 ) )  e.  RR )  -> 
( 2  x.  ( sin `  ( y  / 
2 ) ) )  e.  RR )
278276, 277syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  x.  ( sin `  (
y  /  2 ) ) )  e.  RR )
279265, 269, 270, 278fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) `  y )  =  ( 2  x.  ( sin `  (
y  /  2 ) ) ) )
28085a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  CC )
28113, 275sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
y  /  2 ) )  e.  CC )
28297a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  =/=  0
)
283 ioossicc 11622 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -u pi (,) pi )  C_  ( -u pi [,] pi )
284270eldifad 3493 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  (
-u pi (,) pi ) )
285283, 284sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  (
-u pi [,] pi ) )
286 eldifsni 4159 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  =/=  0
)
287 fourierdlem44 31774 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  ( -u pi [,] pi )  /\  y  =/=  0 )  -> 
( sin `  (
y  /  2 ) )  =/=  0 )
288285, 286, 287syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
y  /  2 ) )  =/=  0 )
289280, 281, 282, 288mulne0d 10213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  x.  ( sin `  (
y  /  2 ) ) )  =/=  0
)
290279, 289eqnetrd 2760 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) `  y )  =/=  0 )
291290neneqd 2669 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) `  y )  =  0 )
292291rgen 2827 . . . . . . . . . . . . . . . . . . 19  |-  A. y  e.  ( ( -u pi (,) pi )  \  {
0 } )  -.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) `
 y )  =  0
293 ralnex 2913 . . . . . . . . . . . . . . . . . . 19  |-  ( A. y  e.  ( ( -u pi (,) pi ) 
\  { 0 } )  -.  ( ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) `  y )  =  0  <->  -.  E. y  e.  ( ( -u pi (,) pi )  \  { 0 } ) ( ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) `  y )  =  0 )
294292, 293mpbi 208 . . . . . . . . . . . . . . . . . 18  |-  -.  E. y  e.  ( ( -u pi (,) pi ) 
\  { 0 } ) ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) `  y )  =  0
29535rgen 2827 . . . . . . . . . . . . . . . . . . . 20  |-  A. x  e.  ( ( -u pi (,) pi )  \  {
0 } ) ( 2  x.  ( sin `  ( x  /  2
) ) )  e.  RR
29626fnmpt 5713 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 } ) )
297295, 296ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) )  Fn  ( (
-u pi (,) pi )  \  { 0 } )
298 ssid 3528 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  ( ( -u pi (,) pi ) 
\  { 0 } )
299 fvelimab 5930 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) )
300297, 298, 299mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  ( 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 )
301294, 300mtbir 299 . . . . . . . . . . . . . . . . 17  |-  -.  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) )
" ( ( -u pi (,) pi )  \  { 0 } ) )
302301a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  -.  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) "
( ( -u pi (,) pi )  \  {
0 } ) ) )
303 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( cos `  ( x  /  2 ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) )
304266fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  y  ->  ( cos `  ( x  / 
2 ) )  =  ( cos `  (
y  /  2 ) ) )
305304adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  y )  ->  ( cos `  ( x  / 
2 ) )  =  ( cos `  (
y  /  2 ) ) )
30613sseli 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  RR  ->  y  e.  CC )
307272, 306syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  CC )
308307, 280, 282divcld 10332 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  e.  CC )
309308coscld 13744 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
y  /  2 ) )  e.  CC )
310303, 305, 270, 309fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  ( cos `  ( y  /  2
) ) )
311273rered 13037 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( y  /  2
) )  =  ( y  /  2 ) )
312 halfpire 22723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( pi 
/  2 )  e.  RR
313312renegcli 9892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  -u (
pi  /  2 )  e.  RR
314313a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR )
315314rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR* )
316312a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR )
317316rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR* )
31813, 44sselii 3506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  pi  e.  CC
319 divneg 10251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( pi  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  -u (
pi  /  2 )  =  ( -u pi  /  2 ) )
320318, 85, 97, 319mp3an 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  -u (
pi  /  2 )  =  ( -u pi  /  2 )
321320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  =  (
-u pi  /  2
) )
32246a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR* )
32347a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR* )
324 ioogtlb 31415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  y  e.  ( -u pi (,) pi ) )  ->  -u pi  <  y )
325322, 323, 284, 324syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  <  y
)
32645a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR )
327 2rp 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  2  e.  RR+
328327a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR+ )
329326, 272, 328ltdiv1d 11309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( -u pi  <  y  <->  ( -u pi  /  2 )  <  (
y  /  2 ) ) )
330325, 329mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( -u pi  /  2 )  <  (
y  /  2 ) )
331321, 330eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  <  (
y  /  2 ) )
332 iooltub 31435 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  y  e.  ( -u pi (,) pi ) )  ->  y  <  pi )
333322, 323, 284, 332syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  <  pi )
33444a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR )
335272, 334, 328ltdiv1d 11309 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  < 
pi 
<->  ( y  /  2
)  <  ( pi  /  2 ) ) )
336333, 335mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  <  (
pi  /  2 ) )
337315, 317, 273, 331, 336eliood 31418 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
338311, 337eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( y  /  2
) )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
339 cosne0 22783 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( y  /  2
)  e.  CC  /\  ( Re `  ( y  /  2 ) )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  (
y  /  2 ) )  =/=  0 )
340308, 338, 339syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
y  /  2 ) )  =/=  0 )
341310, 340eqnetrd 2760 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) `  y
)  =/=  0 )
342341neneqd 2669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  0 )
343342rgen 2827 . . . . . . . . . . . . . . . . . . . 20  |-  A. y  e.  ( ( -u pi (,) pi )  \  {
0 } )  -.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( cos `  ( x  /  2 ) ) ) `  y )  =  0
344 ralnex 2913 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. y  e.  ( ( -u pi (,) pi ) 
\  { 0 } )  -.  ( ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  0  <->  -.  E. y  e.  ( (
-u pi (,) pi )  \  { 0 } ) ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  0 )
345343, 344mpbi 208 . . . . . . . . . . . . . . . . . . 19  |-  -.  E. y  e.  ( ( -u pi (,) pi ) 
\  { 0 } ) ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  0
34681, 82fnmpti 5715 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )  Fn  (
( -u pi (,) pi )  \  { 0 } )
347 fvelimab 5930 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) )
348346, 298, 347mp2an 672 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 )
349345, 348mtbir 299 . . . . . . . . . . . . . . . . . 18  |-  -.  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( cos `  ( x  /  2 ) ) ) " ( (
-u pi (,) pi )  \  { 0 } ) )
350153imaeq1i 5340 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 } ) )
351350eleq2i 2545 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 } ) ) )
352351notbii 296 . . . . . . . . . . . . . . . . . 18  |-  ( -.  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 } ) ) )
353349, 352mpbir 209 . . . . . . . . . . . . . . . . 17  |-  -.  0  e.  ( ( RR  _D  ( x  e.  (
( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )
" ( ( -u pi (,) pi )  \  { 0 } ) )
354353a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  -.  0  e.  ( ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )
" ( ( -u pi (,) pi )  \  { 0 } ) ) )
355 ax-1cn 9562 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
356355div1i 10284 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  1 )  =  1
357356eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  1  =  ( 1  / 
1 )
358 eqid 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
s  /  2 ) ) )  =  ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
s  /  2 ) ) )
359 eqid 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 1  /  ( cos `  ( s  / 
2 ) ) ) )  =  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 1  /  ( cos `  ( s  / 
2 ) ) ) )
36020sseli 3505 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  e.  RR )
36113, 360sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  e.  CC )
362361halfcld 10795 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  e.  CC )
363362coscld 13744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  e.  CC )
36427a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR )
36597a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  =/=  0
)
366360, 364, 365redivcld 10384 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  e.  RR )
367366rered 13037 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( s  /  2
) )  =  ( s  /  2 ) )
368313a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR )
369368rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR* )
370312a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR )
371370rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR* )
372320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  =  (
-u pi  /  2
) )
37344a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR )
374373renegcld 9998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR )
375327a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR+ )
37646a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR* )
37747a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR* )
378 eldif 3491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  <-> 
( s  e.  (
-u pi (,) pi )  /\  -.  s  e. 
{ 0 } ) )
379378simplbi 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  e.  (
-u pi (,) pi ) )
380 ioogtlb 31415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  s  e.  ( -u pi (,) pi ) )  ->  -u pi  <  s )
381376, 377, 379, 380syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  <  s
)
382374, 360, 375, 381ltdiv1dd 11321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( -u pi  /  2 )  <  (
s  /  2 ) )
383372, 382eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  <  (
s  /  2 ) )
384 iooltub 31435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  s  e.  ( -u pi (,) pi ) )  ->  s  <  pi )
385376, 377, 379, 384syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  <  pi )
386360, 373, 375, 385ltdiv1dd 11321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  <  (
pi  /  2 ) )
387369, 371, 366, 383, 386eliood 31418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
388367, 387eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( s  /  2
) )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
389 cosne0 22783 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( s  /  2
)  e.  CC  /\  ( Re `  ( s  /  2 ) )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  (
s  /  2 ) )  =/=  0 )
390362, 388, 389syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  =/=  0 )
391390neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( cos `  ( s  /  2
) )  =  0 )
392366recoscld 13757 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  e.  RR )
393 elsncg 4056 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( cos `  ( s  /  2 ) )  e.  RR  ->  (
( cos `  (
s  /  2 ) )  e.  { 0 }  <->  ( cos `  (
s  /  2 ) )  =  0 ) )
394392, 393syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( cos `  ( s  /  2
) )  e.  {
0 }  <->  ( cos `  ( s  /  2
) )  =  0 ) )
395391, 394mtbird 301 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( cos `  ( s  /  2
) )  e.  {
0 } )
396363, 395eldifd 3492 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  e.  ( CC 
\  { 0 } ) )
397396adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  s  e.  ( ( -u pi (,) pi )  \  {
0 } ) )  ->  ( cos `  (
s  /  2 ) )  e.  ( CC 
\  { 0 } ) )
398362ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  /\  ( s  / 
2 )  =/=  0
) )  ->  (
s  /  2 )  e.  CC )
399 cosf 13738 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  cos : CC
--> CC
400399a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  cos : CC --> CC )
401400ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  CC )  ->  ( cos `  x )  e.  CC )
402 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  CC  |->  ( s  /  2 ) )  =  ( s  e.  CC  |->  ( s  / 
2 ) )
403402divccncf 21278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 2  e.  CC  /\  2  =/=  0 )  -> 
( s  e.  CC  |->  ( s  /  2
) )  e.  ( CC -cn-> CC ) )
40485, 97, 403mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  CC  |->  ( s  /  2 ) )  e.  ( CC -cn-> CC )
405404a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( T. 
->  ( s  e.  CC  |->  ( s  /  2
) )  e.  ( CC -cn-> CC ) )
406170adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( T.  /\  s  e.  ( -u pi (,) pi ) )  ->  s  e.  CC )
407406halfcld 10795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( T.  /\  s  e.  ( -u pi (,) pi ) )  ->  (
s  /  2 )  e.  CC )
408402, 405, 172, 173, 407cncfmptssg 31531 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( T. 
->  ( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
409408trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC )
410409a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( T. 
->  ( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
411 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  =  0  ->  (
s  /  2 )  =  ( 0  / 
2 ) )
412200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  =  0  ->  (
0  /  2 )  =  0 )
413411, 412eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  =  0  ->  (
s  /  2 )  =  0 )
414410, 51, 413cnmptlimc 22162 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( T. 
->  0  e.  (
( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) ) lim CC  0 ) )
415414trud 1388 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) lim
CC  0 )
416 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  =  ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )
417 halfcl 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  CC  ->  (
s  /  2 )  e.  CC )
418170, 417syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( -u pi (,) pi )  ->  (
s  /  2 )  e.  CC )
419416, 418fmpti 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) : ( -u pi (,) pi ) --> CC
420419a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  ( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) ) : ( -u pi (,) pi ) --> CC )
421420limcdif 22148 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( T. 
->  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) lim
CC  0 )  =  ( ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 ) )
422421trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) lim CC  0 )  =  ( ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) ) lim CC  0 )
423 resmpt 5329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( -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 ) ) )
42417, 423ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) )  =  ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( s  / 
2 ) )
425424oveq1i 6305 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 )  =  ( ( s  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( s  /  2 ) ) lim CC  0 )
426422, 425eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) lim CC  0 )  =  ( ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( s  /  2
) ) lim CC  0 )
427415, 426eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ( ( s  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( s  /  2 ) ) lim CC  0 )
428427a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  0  e.  (
( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( s  /  2 ) ) lim
CC  0 ) )
429 ffn 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( cos
: CC --> CC  ->  cos 
Fn  CC )
430399, 429ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  cos  Fn  CC
431 dffn5 5919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( cos 
Fn  CC  <->  cos  =  ( x  e.  CC  |->  ( cos `  x ) ) )
432430, 431mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  cos  =  ( x  e.  CC  |->  ( cos `  x ) )
433432eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  CC  |->  ( cos `  x ) )  =  cos
434 coscn 22707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  cos  e.  ( CC -cn-> CC )
435433, 434eqeltri 2551 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  CC  |->  ( cos `  x ) )  e.  ( CC -cn-> CC )
436435a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( T. 
->  ( x  e.  CC  |->  ( cos `  x ) )  e.  ( CC
-cn-> CC ) )
437171, 51sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( T. 
->  0  e.  CC )
438 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  0  ->  ( cos `  x )  =  ( cos `  0
) )
439 cos0 13763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( cos `  0 )  =  1
440439a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  0  ->  ( cos `  0 )  =  1 )
441438, 440eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  0  ->  ( cos `  x )  =  1 )
442436, 437, 441cnmptlimc 22162 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( T. 
->  1  e.  (
( x  e.  CC  |->  ( cos `  x ) ) lim CC  0 ) )
443442trud 1388 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  ( ( x  e.  CC  |->  ( cos `  x
) ) lim CC  0 )
444443a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  1  e.  (
( x  e.  CC  |->  ( cos `  x ) ) lim CC  0 ) )
445 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( s  / 
2 )  ->  ( cos `  x )  =  ( cos `  (
s  /  2 ) ) )
446 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  /  2 )  =  0  ->  ( cos `  ( s  / 
2 ) )  =  ( cos `  0
) )
447439a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  /  2 )  =  0  ->  ( cos `  0 )  =  1 )
448446, 447eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  /  2 )  =  0  ->  ( cos `  ( s  / 
2 ) )  =  1 )
449448ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  /\  ( s  / 
2 )  =  0 ) )  ->  ( cos `  ( s  / 
2 ) )  =  1 )
450398, 401, 428, 444, 445, 449limcco 22165 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  1  e.  (
( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( cos `  ( s  /  2
) ) ) lim CC  0 ) )
451 ax-1ne0 9573 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  =/=  0
452451a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  1  =/=  0
)
453358, 359, 397, 450, 452reclimc 31518 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( 1  /  1
)  e.  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 1  / 
( cos `  (
s  /  2 ) ) ) ) lim CC  0 ) )
454453trud 1388 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  /  1 )  e.  ( ( s  e.  ( ( -u pi (,) pi )  \