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

Theorem fourierdlem62 32154
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 2461 . . . . . 6  |-  ( y  =  s  ->  (
y  =  0  <->  s  =  0 ) )
3 id 22 . . . . . . 7  |-  ( y  =  s  ->  y  =  s )
4 oveq1 6303 . . . . . . . . 9  |-  ( y  =  s  ->  (
y  /  2 )  =  ( s  / 
2 ) )
54fveq2d 5876 . . . . . . . 8  |-  ( y  =  s  ->  ( sin `  ( y  / 
2 ) )  =  ( sin `  (
s  /  2 ) ) )
65oveq2d 6312 . . . . . . 7  |-  ( y  =  s  ->  (
2  x.  ( sin `  ( y  /  2
) ) )  =  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )
73, 6oveq12d 6314 . . . . . 6  |-  ( y  =  s  ->  (
y  /  ( 2  x.  ( sin `  (
y  /  2 ) ) ) )  =  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
82, 7ifbieq2d 3969 . . . . 5  |-  ( y  =  s  ->  if ( y  =  0 ,  1 ,  ( y  /  ( 2  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
98cbvmptv 4548 . . . 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 ) ) ) ) ) )
101, 9eqtri 2486 . . 3  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
1110fourierdlem43 32135 . 2  |-  K :
( -u pi [,] pi )
--> RR
12 ax-resscn 9566 . . 3  |-  RR  C_  CC
13 fss 5745 . . . . . 6  |-  ( ( K : ( -u pi [,] pi ) --> RR 
/\  RR  C_  CC )  ->  K : (
-u pi [,] pi )
--> CC )
1411, 12, 13mp2an 672 . . . . 5  |-  K :
( -u pi [,] pi )
--> CC
1514a1i 11 . . . . . . . . 9  |-  ( s  =  0  ->  K : ( -u pi [,] pi ) --> CC )
16 difss 3627 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  ( -u pi (,) pi )
17 elioore 11584 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( -u pi (,) pi )  ->  s  e.  RR )
1817ssriv 3503 . . . . . . . . . . . . . . . . 17  |-  ( -u pi (,) pi )  C_  RR
1916, 18sstri 3508 . . . . . . . . . . . . . . . 16  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  RR
2019a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  C_  RR )
21 eqid 2457 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x )
2219sseli 3495 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  x  e.  RR )
2321, 22fmpti 6055 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) : ( ( -u pi (,) pi )  \  { 0 } ) --> RR
2423a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  x ) : ( ( -u pi (,) pi )  \  { 0 } ) --> RR )
25 eqid 2457 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) )
26 2re 10626 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  RR
2726a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR )
2822rehalfcld 10806 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( x  / 
2 )  e.  RR )
2928resincld 13890 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
x  /  2 ) )  e.  RR )
3027, 29remulcld 9641 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  x.  ( sin `  (
x  /  2 ) ) )  e.  RR )
3125, 30fmpti 6055 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) : ( (
-u pi (,) pi )  \  { 0 } ) --> RR
3231a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) : ( ( -u pi (,) pi )  \  {
0 } ) --> RR )
33 iooretop 21399 . . . . . . . . . . . . . . . 16  |-  ( -u pi (,) pi )  e.  ( topGen `  ran  (,) )
3433a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( -u pi (,) pi )  e.  ( topGen `
 ran  (,) )
)
35 0re 9613 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
36 negpilt0 31665 . . . . . . . . . . . . . . . . 17  |-  -u pi  <  0
37 pipos 22979 . . . . . . . . . . . . . . . . 17  |-  0  <  pi
38 pire 22977 . . . . . . . . . . . . . . . . . . . 20  |-  pi  e.  RR
3938renegcli 9899 . . . . . . . . . . . . . . . . . . 19  |-  -u pi  e.  RR
4039rexri 9663 . . . . . . . . . . . . . . . . . 18  |-  -u pi  e.  RR*
4138rexri 9663 . . . . . . . . . . . . . . . . . 18  |-  pi  e.  RR*
42 elioo2 11595 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR* )  ->  ( 0  e.  (
-u pi (,) pi ) 
<->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <  pi ) ) )
4340, 41, 42mp2an 672 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  ( -u pi (,) pi )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  < 
pi ) )
4435, 36, 37, 43mpbir3an 1178 . . . . . . . . . . . . . . . 16  |-  0  e.  ( -u pi (,) pi )
4544a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  0  e.  ( -u pi (,) pi ) )
46 eqid 2457 . . . . . . . . . . . . . . 15  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  ( (
-u pi (,) pi )  \  { 0 } )
47 1ex 9608 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  _V
48 eqid 2457 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  1 )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )
4947, 48dmmpti 5716 . . . . . . . . . . . . . . . . . 18  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )  =  ( ( -u pi (,) pi )  \  {
0 } )
50 reelprrecn 9601 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  e.  { RR ,  CC }
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  RR  e.  { RR ,  CC } )
5212sseli 3495 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  x  e.  CC )
5352adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  x  e.  CC )
54 1red 9628 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  1  e.  RR )
5551dvmptid 22486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  x ) )  =  ( x  e.  RR  |->  1 ) )
56 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5756tgioo2 21434 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
58 sncldre 31636 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  e.  RR  ->  { 0 }  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
5935, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { 0 }  e.  ( Clsd `  ( topGen `  ran  (,) )
)
60 retopon 21396 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( topGen ` 
ran  (,) )  e.  (TopOn `  RR )
6160toponunii 19560 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  RR  =  U. ( topGen `  ran  (,) )
6261difopn 19662 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( -u pi (,) pi )  e.  ( topGen `
 ran  (,) )  /\  { 0 }  e.  ( Clsd `  ( topGen ` 
ran  (,) ) ) )  ->  ( ( -u pi (,) pi )  \  { 0 } )  e.  ( topGen `  ran  (,) ) )
6333, 59, 62mp2an 672 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
-u pi (,) pi )  \  { 0 } )  e.  ( topGen ` 
ran  (,) )
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  e.  ( topGen `  ran  (,) )
)
6551, 53, 54, 55, 20, 57, 56, 64dvmptres 22492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  1 ) )
6665trud 1404 . . . . . . . . . . . . . . . . . . . 20  |-  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )
6766eqcomi 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  1 )  =  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) )
6867dmeqi 5214 . . . . . . . . . . . . . . . . . 18  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  1 )  =  dom  ( RR  _D  ( x  e.  (
( -u pi (,) pi )  \  { 0 } )  |->  x ) )
6949, 68eqtr3i 2488 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  dom  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) )
7069eqimssi 3553 . . . . . . . . . . . . . . . 16  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  dom  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) )
7170a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  C_  dom  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x ) ) )
72 fvex 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( cos `  ( x  /  2
) )  e.  _V
73 eqid 2457 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) )
7472, 73dmmpti 5716 . . . . . . . . . . . . . . . . . 18  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) )  =  ( ( -u pi (,) pi )  \  { 0 } )
75 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T.  /\  x  e.  RR )  ->  2  e.  CC )
7653halfcld 10804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( T.  /\  x  e.  RR )  ->  (
x  /  2 )  e.  CC )
7776sincld 13877 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T.  /\  x  e.  RR )  ->  ( sin `  ( x  / 
2 ) )  e.  CC )
7875, 77mulcld 9633 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  e.  CC )
7976coscld 13878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  ( cos `  ( x  / 
2 ) )  e.  CC )
80 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  2  e.  CC )
81 2ne0 10649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  2  =/=  0
8281a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  2  =/=  0 )
8352, 80, 82divrec2d 10345 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  RR  ->  (
x  /  2 )  =  ( ( 1  /  2 )  x.  x ) )
8483fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  RR  ->  ( sin `  ( x  / 
2 ) )  =  ( sin `  (
( 1  /  2
)  x.  x ) ) )
8584oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) )
8685mpteq2ia 4539 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  =  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) )
8786oveq2i 6307 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )  =  ( RR  _D  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) ) )
88 resmpt 5333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR  C_  CC  ->  ( (
x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) )  |`  RR )  =  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) ) )
8912, 88ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) )  |`  RR )  =  ( x  e.  RR  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) )
9089eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) )  =  ( ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) )  |`  RR )
9190oveq2i 6307 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) )  =  ( x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  /  2 )  x.  x ) ) ) )
93 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  CC  ->  2  e.  CC )
94 halfcn 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 1  /  2 )  e.  CC
9594a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  CC  ->  (
1  /  2 )  e.  CC )
96 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  CC  ->  x  e.  CC )
9795, 96mulcld 9633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  CC  ->  (
( 1  /  2
)  x.  x )  e.  CC )
9897sincld 13877 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  CC  ->  ( sin `  ( ( 1  /  2 )  x.  x ) )  e.  CC )
9993, 98mulcld 9633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  CC  ->  (
2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) )  e.  CC )
10092, 99fmpti 6055 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) ) : CC --> CC
101 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 10627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  2  e.  CC
103102, 94mulcli 9618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 2  x.  ( 1  / 
2 ) )  e.  CC
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  CC  ->  (
2  x.  ( 1  /  2 ) )  e.  CC )
10597coscld 13878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  CC  ->  ( cos `  ( ( 1  /  2 )  x.  x ) )  e.  CC )
106104, 105mulcld 9633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  CC  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  e.  CC )
107106adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( T.  /\  x  e.  CC )  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  e.  CC )
108101, 107dmmptd 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( T. 
->  dom  ( x  e.  CC  |->  ( ( 2  x.  ( 1  / 
2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  x ) ) ) )  =  CC )
109108trud 1404 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  (
x  e.  CC  |->  ( ( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) ) )  =  CC
11012, 109sseqtr4i 3532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  RR  C_  dom  ( x  e.  CC  |->  ( ( 2  x.  ( 1  /  2
) )  x.  ( cos `  ( ( 1  /  2 )  x.  x ) ) ) )
111 dvasinbx 31920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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
) ) ) ) )
112102, 94, 111mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) )
113112dmeqi 5214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  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 ) ) ) )
114110, 113sseqtr4i 3532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  RR  C_  dom  ( CC  _D  (
x  e.  CC  |->  ( 2  x.  ( sin `  ( ( 1  / 
2 )  x.  x
) ) ) ) )
115 dvcnre 31914 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
)
116100, 114, 115mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 )
117112reseq1i 5279 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 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 5333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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
) ) ) ) )
11912, 118ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 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
) ) ) )
120102, 81recidi 10296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2  x.  ( 1  / 
2 ) )  =  1
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  (
2  x.  ( 1  /  2 ) )  =  1 )
12283eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  RR  ->  (
( 1  /  2
)  x.  x )  =  ( x  / 
2 ) )
123122fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  ( cos `  ( ( 1  /  2 )  x.  x ) )  =  ( cos `  (
x  /  2 ) ) )
124121, 123oveq12d 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  RR  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  =  ( 1  x.  ( cos `  ( x  / 
2 ) ) ) )
12552halfcld 10804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  RR  ->  (
x  /  2 )  e.  CC )
126125coscld 13878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  RR  ->  ( cos `  ( x  / 
2 ) )  e.  CC )
127126mulid2d 9631 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  RR  ->  (
1  x.  ( cos `  ( x  /  2
) ) )  =  ( cos `  (
x  /  2 ) ) )
128124, 127eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  RR  ->  (
( 2  x.  (
1  /  2 ) )  x.  ( cos `  ( ( 1  / 
2 )  x.  x
) ) )  =  ( cos `  (
x  /  2 ) ) )
129128mpteq2ia 4539 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  |->  ( ( 2  x.  ( 1  /  2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  x ) ) ) )  =  ( x  e.  RR  |->  ( cos `  ( x  /  2 ) ) )
130117, 119, 1293eqtri 2490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( CC  _D  ( x  e.  CC  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) ) )  |`  RR )  =  ( x  e.  RR  |->  ( cos `  ( x  /  2 ) ) )
13191, 116, 1303eqtri 2490 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
( 1  /  2
)  x.  x ) ) ) ) )  =  ( x  e.  RR  |->  ( cos `  (
x  /  2 ) ) )
13287, 131eqtri 2486 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( RR 
_D  ( x  e.  RR  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )  =  ( x  e.  RR  |->  ( cos `  (
x  /  2 ) ) )
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )  =  ( x  e.  RR  |->  ( cos `  ( x  /  2
) ) ) )
13451, 78, 79, 133, 20, 57, 56, 64dvmptres 22492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( cos `  ( x  /  2 ) ) ) )
135134trud 1404 . . . . . . . . . . . . . . . . . . . 20  |-  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )
136135eqcomi 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )  =  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) )
137136dmeqi 5214 . . . . . . . . . . . . . . . . . 18  |-  dom  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) )  =  dom  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )
13874, 137eqtr3i 2488 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  { 0 } )  =  dom  ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )
139138eqimssi 3553 . . . . . . . . . . . . . . . 16  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  dom  ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) )
140139a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( ( -u pi (,) pi )  \  {
0 } )  C_  dom  ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) ) )
14117recnd 9639 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( -u pi (,) pi )  ->  s  e.  CC )
142141ssriv 3503 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -u pi (,) pi )  C_  CC
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( -u pi (,) pi )  C_  CC )
144 ssid 3518 . . . . . . . . . . . . . . . . . . . . . . 23  |-  CC  C_  CC
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  CC  C_  CC )
146143, 145idcncfg 31877 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  x )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
147146trud 1404 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( -u pi (,) pi )  |->  x )  e.  ( ( -u pi (,) pi ) -cn-> CC )
148 cnlimc 22418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
-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 ) ) ) )
149142, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) )
150147, 149mpbi 208 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) )
151150simpri 462 . . . . . . . . . . . . . . . . . 18  |-  A. y  e.  ( -u pi (,) pi ) ( ( x  e.  ( -u pi (,) pi )  |->  x ) `
 y )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  y )
152 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  0  ->  (
( x  e.  (
-u pi (,) pi )  |->  x ) `  y )  =  ( ( x  e.  (
-u pi (,) pi )  |->  x ) ` 
0 ) )
153 oveq2 6304 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  0  ->  (
( x  e.  (
-u pi (,) pi )  |->  x ) lim CC  y )  =  ( ( x  e.  (
-u pi (,) pi )  |->  x ) lim CC  0 ) )
154152, 153eleq12d 2539 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
155154rspccva 3209 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) )
156151, 44, 155mp2an 672 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) `  0 )  e.  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  0 )
157 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  x  =  0 )
158 eqid 2457 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( -u pi (,) pi )  |->  x )  =  ( x  e.  ( -u pi (,) pi )  |->  x )
159 c0ex 9607 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  _V
160157, 158, 159fvmpt 5956 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  ( -u pi (,) pi )  ->  (
( x  e.  (
-u pi (,) pi )  |->  x ) ` 
0 )  =  0 )
16144, 160ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) `  0 )  =  0
162 elioore 11584 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  RR )
163162recnd 9639 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  CC )
164158, 163fmpti 6055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( -u pi (,) pi )  |->  x ) : ( -u pi (,) pi ) --> CC
165164a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  x ) : ( -u pi (,) pi ) --> CC )
166165limcdif 22406 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim
CC  0 )  =  ( ( ( x  e.  ( -u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 ) )
167166trud 1404 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim CC  0 )  =  ( ( ( x  e.  ( -u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) ) lim CC  0 )
168 resmpt 5333 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( -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 ) )
16916, 168ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) )  =  ( x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x )
170169oveq1i 6306 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  (
-u pi (,) pi )  |->  x )  |`  ( ( -u pi (,) pi )  \  {
0 } ) ) lim
CC  0 )  =  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) lim CC  0 )
171167, 170eqtri 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( -u pi (,) pi )  |->  x ) lim CC  0 )  =  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) lim CC  0 )
172156, 161, 1713eltr3i 2557 . . . . . . . . . . . . . . . 16  |-  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x ) lim CC  0 )
173172a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  0  e.  (
( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  x ) lim
CC  0 ) )
174 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  CC  |->  2 )  =  ( x  e.  CC  |->  2 )
175144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2  e.  CC  ->  CC  C_  CC )
176 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2  e.  CC  ->  2  e.  CC )
177175, 176, 175constcncfg 31876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2  e.  CC  ->  (
x  e.  CC  |->  2 )  e.  ( CC
-cn-> CC ) )
178102, 177mp1i 12 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  ( x  e.  CC  |->  2 )  e.  ( CC -cn-> CC ) )
179 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T.  /\  x  e.  ( -u pi (,) pi ) )  ->  2  e.  CC )
180174, 178, 143, 145, 179cncfmptssg 31875 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  2 )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
181 sincn 22965 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  sin  e.  ( CC -cn-> CC )
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  sin  e.  ( CC
-cn-> CC ) )
183 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  CC  |->  ( x  /  2 ) )  =  ( x  e.  CC  |->  ( x  / 
2 ) )
184183divccncf 21536 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 2  e.  CC  /\  2  =/=  0 )  -> 
( x  e.  CC  |->  ( x  /  2
) )  e.  ( CC -cn-> CC ) )
185102, 81, 184mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  CC  |->  ( x  /  2 ) )  e.  ( CC -cn-> CC )
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( T. 
->  ( x  e.  CC  |->  ( x  /  2
) )  e.  ( CC -cn-> CC ) )
187163adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( T.  /\  x  e.  ( -u pi (,) pi ) )  ->  x  e.  CC )
188187halfcld 10804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( T.  /\  x  e.  ( -u pi (,) pi ) )  ->  (
x  /  2 )  e.  CC )
189183, 186, 143, 145, 188cncfmptssg 31875 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( x  / 
2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
190182, 189cncfmpt1f 21543 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( sin `  (
x  /  2 ) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
191180, 190mulcncf 21985 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
192191trud 1404 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  e.  ( ( -u pi (,) pi ) -cn-> CC )
193 cnlimc 22418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
-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 ) ) ) )
194142, 193ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) )
195192, 194mpbi 208 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) )
196195simpri 462 . . . . . . . . . . . . . . . . . 18  |-  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 )
197 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 6304 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) )
199197, 198eleq12d 2539 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
200199rspccva 3209 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) )
201196, 44, 200mp2an 672 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
202 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  0  ->  (
x  /  2 )  =  ( 0  / 
2 ) )
203102, 81div0i 10299 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  /  2 )  =  0
204202, 203syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  0  ->  (
x  /  2 )  =  0 )
205204fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  0  ->  ( sin `  ( x  / 
2 ) )  =  ( sin `  0
) )
206 sin0 13896 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( sin `  0 )  =  0
207205, 206syl6eq 2514 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  0  ->  ( sin `  ( x  / 
2 ) )  =  0 )
208207oveq2d 6312 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  0  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  0 ) )
209 2t0e0 10712 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  x.  0 )  =  0
210208, 209syl6eq 2514 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  0 )
211 eqid 2457 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )  =  ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) )
212210, 211, 159fvmpt 5956 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  ( -u pi (,) pi )  ->  (
( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) ` 
0 )  =  0 )
21344, 212ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) `
 0 )  =  0
214 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( -u pi (,) pi )  ->  2  e.  CC )
215163halfcld 10804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( -u pi (,) pi )  ->  (
x  /  2 )  e.  CC )
216215sincld 13877 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( -u pi (,) pi )  ->  ( sin `  ( x  / 
2 ) )  e.  CC )
217214, 216mulcld 9633 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -u pi (,) pi )  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  e.  CC )
218211, 217fmpti 6055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( -u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) : ( -u pi (,) pi ) --> CC
219218a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( x  e.  (
-u pi (,) pi )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) : ( -u pi (,) pi ) --> CC )
220219limcdif 22406 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
221220trud 1404 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 )
222 resmpt 5333 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( -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
) ) ) ) )
22316, 222ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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
) ) ) )
224223oveq1i 6306 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
225221, 224eqtri 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
226201, 213, 2253eltr3i 2557 . . . . . . . . . . . . . . . 16  |-  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) lim
CC  0 )
227226a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  0  e.  (
( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) lim CC  0 ) )
228 eqidd 2458 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 6303 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
x  /  2 )  =  ( y  / 
2 ) )
230229fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( sin `  ( x  / 
2 ) )  =  ( sin `  (
y  /  2 ) ) )
231230oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  ( sin `  ( y  / 
2 ) ) ) )
232231adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  y )  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  ( sin `  ( y  / 
2 ) ) ) )
233 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  ( ( -u pi (,) pi )  \  { 0 } ) )
23426a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR )
23519sseli 3495 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  RR )
236235rehalfcld 10806 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  e.  RR )
237236resincld 13890 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
y  /  2 ) )  e.  RR )
238234, 237remulcld 9641 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  x.  ( sin `  (
y  /  2 ) ) )  e.  RR )
239228, 232, 233, 238fvmptd 5961 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 10629 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  CC )
241237recnd 9639 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
y  /  2 ) )  e.  CC )
24281a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  =/=  0
)
243 ioossicc 11635 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -u pi (,) pi )  C_  ( -u pi [,] pi )
244 eldifi 3622 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  (
-u pi (,) pi ) )
245243, 244sseldi 3497 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  (
-u pi [,] pi ) )
246 eldifsni 4158 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  =/=  0
)
247 fourierdlem44 32136 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  ( -u pi [,] pi )  /\  y  =/=  0 )  -> 
( sin `  (
y  /  2 ) )  =/=  0 )
248245, 246, 247syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
y  /  2 ) )  =/=  0 )
249240, 241, 242, 248mulne0d 10222 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  x.  ( sin `  (
y  /  2 ) ) )  =/=  0
)
250239, 249eqnetrd 2750 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) `  y )  =/=  0 )
251250neneqd 2659 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) `  y )  =  0 )
252251nrex 2912 . . . . . . . . . . . . . . . . 17  |-  -.  E. y  e.  ( ( -u pi (,) pi ) 
\  { 0 } ) ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) `  y )  =  0
25325fnmpt 5713 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 } ) )
254253, 30mprg 2820 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) )  Fn  ( (
-u pi (,) pi )  \  { 0 } )
255 ssid 3518 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi (,) pi )  \  { 0 } )  C_  ( ( -u pi (,) pi ) 
\  { 0 } )
256 fvelimab 5929 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) )
257254, 255, 256mp2an 672 . . . . . . . . . . . . . . . . 17  |-  ( 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 )
258252, 257mtbir 299 . . . . . . . . . . . . . . . 16  |-  -.  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) )
" ( ( -u pi (,) pi )  \  { 0 } ) )
259258a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  -.  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) "
( ( -u pi (,) pi )  \  {
0 } ) ) )
260 eqidd 2458 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( cos `  ( x  /  2 ) ) )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) )
261229fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( cos `  ( x  / 
2 ) )  =  ( cos `  (
y  /  2 ) ) )
262261adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  y )  ->  ( cos `  ( x  / 
2 ) )  =  ( cos `  (
y  /  2 ) ) )
263235recnd 9639 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  e.  CC )
264263halfcld 10804 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  e.  CC )
265264coscld 13878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
y  /  2 ) )  e.  CC )
266260, 262, 233, 265fvmptd 5961 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  ( cos `  ( y  /  2
) ) )
267236rered 13069 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( y  /  2
) )  =  ( y  /  2 ) )
268 halfpire 22983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( pi 
/  2 )  e.  RR
269268renegcli 9899 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -u (
pi  /  2 )  e.  RR
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR )
271270rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR* )
272268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR )
273272rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR* )
274 picn 22978 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  pi  e.  CC
275 divneg 10260 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( pi  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  -u (
pi  /  2 )  =  ( -u pi  /  2 ) )
276274, 102, 81, 275mp3an 1324 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  -u (
pi  /  2 )  =  ( -u pi  /  2 )
27739a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR )
278 2rp 11250 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  e.  RR+
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR+ )
28040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR* )
28141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR* )
282 ioogtlb 31731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  y  e.  ( -u pi (,) pi ) )  ->  -u pi  <  y )
283280, 281, 244, 282syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  <  y
)
284277, 235, 279, 283ltdiv1dd 11334 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( -u pi  /  2 )  <  (
y  /  2 ) )
285276, 284syl5eqbr 4489 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  <  (
y  /  2 ) )
28638a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR )
287 iooltub 31751 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  y  e.  ( -u pi (,) pi ) )  ->  y  <  pi )
288280, 281, 244, 287syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  y  <  pi )
289235, 286, 279, 288ltdiv1dd 11334 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  <  (
pi  /  2 ) )
290271, 273, 236, 285, 289eliood 31734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( y  / 
2 )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
291267, 290eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( y  /  2
) )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
292 cosne0 23043 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( y  /  2
)  e.  CC  /\  ( Re `  ( y  /  2 ) )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  (
y  /  2 ) )  =/=  0 )
293264, 291, 292syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
y  /  2 ) )  =/=  0 )
294266, 293eqnetrd 2750 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) `  y
)  =/=  0 )
295294neneqd 2659 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  0 )
296295nrex 2912 . . . . . . . . . . . . . . . . . 18  |-  -.  E. y  e.  ( ( -u pi (,) pi ) 
\  { 0 } ) ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) ) `  y
)  =  0
29772, 73fnmpti 5715 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
x  /  2 ) ) )  Fn  (
( -u pi (,) pi )  \  { 0 } )
298 fvelimab 5929 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) )
299297, 255, 298mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  ( 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 )
300296, 299mtbir 299 . . . . . . . . . . . . . . . . 17  |-  -.  0  e.  ( ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( cos `  ( x  /  2 ) ) ) " ( (
-u pi (,) pi )  \  { 0 } ) )
301135imaeq1i 5344 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 } ) )
302301eleq2i 2535 . . . . . . . . . . . . . . . . 17  |-  ( 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 } ) ) )
303300, 302mtbir 299 . . . . . . . . . . . . . . . 16  |-  -.  0  e.  ( ( RR  _D  ( x  e.  (
( -u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )
" ( ( -u pi (,) pi )  \  { 0 } ) )
304303a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  -.  0  e.  ( ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 2  x.  ( sin `  (
x  /  2 ) ) ) ) )
" ( ( -u pi (,) pi )  \  { 0 } ) ) )
305 eqid 2457 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( cos `  (
s  /  2 ) ) )  =  ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( cos `  (
s  /  2 ) ) )
306 eqid 2457 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 1  /  ( cos `  ( s  / 
2 ) ) ) )  =  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 1  /  ( cos `  ( s  / 
2 ) ) ) )
30719sseli 3495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  e.  RR )
308307recnd 9639 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  e.  CC )
309308halfcld 10804 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  e.  CC )
310309coscld 13878 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  e.  CC )
311307rehalfcld 10806 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  e.  RR )
312311rered 13069 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( s  /  2
) )  =  ( s  /  2 ) )
313269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR )
314313rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  e.  RR* )
315268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR )
316315rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( pi  / 
2 )  e.  RR* )
31738a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR )
318317renegcld 10007 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR )
319278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR+ )
32040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  e.  RR* )
32141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  pi  e.  RR* )
322 eldifi 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  e.  (
-u pi (,) pi ) )
323 ioogtlb 31731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  s  e.  ( -u pi (,) pi ) )  ->  -u pi  <  s )
324320, 321, 322, 323syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u pi  <  s
)
325318, 307, 319, 324ltdiv1dd 11334 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( -u pi  /  2 )  <  (
s  /  2 ) )
326276, 325syl5eqbr 4489 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -u ( pi  / 
2 )  <  (
s  /  2 ) )
327 iooltub 31751 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  s  e.  ( -u pi (,) pi ) )  ->  s  <  pi )
328320, 321, 322, 327syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  <  pi )
329307, 317, 319, 328ltdiv1dd 11334 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  <  (
pi  /  2 ) )
330314, 316, 311, 326, 329eliood 31734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( s  / 
2 )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
331312, 330eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( Re `  ( s  /  2
) )  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )
332 cosne0 23043 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  /  2
)  e.  CC  /\  ( Re `  ( s  /  2 ) )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  (
s  /  2 ) )  =/=  0 )
333309, 331, 332syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  =/=  0 )
334333neneqd 2659 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( cos `  ( s  /  2
) )  =  0 )
335311recoscld 13891 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  e.  RR )
336 elsncg 4055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( cos `  ( s  /  2 ) )  e.  RR  ->  (
( cos `  (
s  /  2 ) )  e.  { 0 }  <->  ( cos `  (
s  /  2 ) )  =  0 ) )
337335, 336syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( cos `  ( s  /  2
) )  e.  {
0 }  <->  ( cos `  ( s  /  2
) )  =  0 ) )
338334, 337mtbird 301 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  -.  ( cos `  ( s  /  2
) )  e.  {
0 } )
339310, 338eldifd 3482 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  e.  ( CC 
\  { 0 } ) )
340339adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  s  e.  ( ( -u pi (,) pi )  \  {
0 } ) )  ->  ( cos `  (
s  /  2 ) )  e.  ( CC 
\  { 0 } ) )
341309ad2antrl 727 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  /\  ( s  / 
2 )  =/=  0
) )  ->  (
s  /  2 )  e.  CC )
342 cosf 13872 . . . . . . . . . . . . . . . . . . . 20  |-  cos : CC
--> CC
343342a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  cos : CC --> CC )
344343ffvelrnda 6032 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  CC )  ->  ( cos `  x )  e.  CC )
345 eqid 2457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  CC  |->  ( s  /  2 ) )  =  ( s  e.  CC  |->  ( s  / 
2 ) )
346345divccncf 21536 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  e.  CC  /\  2  =/=  0 )  -> 
( s  e.  CC  |->  ( s  /  2
) )  e.  ( CC -cn-> CC ) )
347102, 81, 346mp2an 672 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  CC  |->  ( s  /  2 ) )  e.  ( CC -cn-> CC )
348347a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( s  e.  CC  |->  ( s  /  2
) )  e.  ( CC -cn-> CC ) )
349141adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  s  e.  ( -u pi (,) pi ) )  ->  s  e.  CC )
350349halfcld 10804 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  s  e.  ( -u pi (,) pi ) )  ->  (
s  /  2 )  e.  CC )
351345, 348, 143, 145, 350cncfmptssg 31875 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) )  e.  ( ( -u pi (,) pi ) -cn-> CC ) )
352 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  0  ->  (
s  /  2 )  =  ( 0  / 
2 ) )
353352, 203syl6eq 2514 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  0  ->  (
s  /  2 )  =  0 )
354351, 45, 353cnmptlimc 22420 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  0  e.  (
( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) ) lim CC  0 ) )
355 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  =  ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )
356141halfcld 10804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( -u pi (,) pi )  ->  (
s  /  2 )  e.  CC )
357355, 356fmpti 6055 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) : ( -u pi (,) pi ) --> CC
358357a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( s  e.  (
-u pi (,) pi )  |->  ( s  / 
2 ) ) : ( -u pi (,) pi ) --> CC )
359358limcdif 22406 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) )
360359trud 1404 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) lim CC  0 )  =  ( ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) ) lim CC  0 )
361 resmpt 5333 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( -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 ) ) )
36216, 361ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) )  |`  ( ( -u pi (,) pi ) 
\  { 0 } ) )  =  ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( s  / 
2 ) )
363362oveq1i 6306 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 )
364360, 363eqtri 2486 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  ( -u pi (,) pi )  |->  ( s  /  2 ) ) lim CC  0 )  =  ( ( s  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( s  /  2
) ) lim CC  0 )
365354, 364syl6eleq 2555 . . . . . . . . . . . . . . . . . 18  |-  ( T. 
->  0  e.  (
( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( s  /  2 ) ) lim
CC  0 ) )
366 ffn 5737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( cos
: CC --> CC  ->  cos 
Fn  CC )
367342, 366ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  cos  Fn  CC
368 dffn5 5918 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( cos 
Fn  CC  <->  cos  =  ( x  e.  CC  |->  ( cos `  x ) ) )
369367, 368mpbi 208 . . . . . . . . . . . . . . . . . . . . 21  |-  cos  =  ( x  e.  CC  |->  ( cos `  x ) )
370 coscn 22966 . . . . . . . . . . . . . . . . . . . . 21  |-  cos  e.  ( CC -cn-> CC )
371369, 370eqeltrri 2542 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  CC  |->  ( cos `  x ) )  e.  ( CC -cn-> CC )
372371a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  ( x  e.  CC  |->  ( cos `  x ) )  e.  ( CC
-cn-> CC ) )
373 0cnd 9606 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  0  e.  CC )
374 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  0  ->  ( cos `  x )  =  ( cos `  0
) )
375 cos0 13897 . . . . . . . . . . . . . . . . . . . 20  |-  ( cos `  0 )  =  1
376374, 375syl6eq 2514 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  ( cos `  x )  =  1 )
377372, 373, 376cnmptlimc 22420 . . . . . . . . . . . . . . . . . 18  |-  ( T. 
->  1  e.  (
( x  e.  CC  |->  ( cos `  x ) ) lim CC  0 ) )
378 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( s  / 
2 )  ->  ( cos `  x )  =  ( cos `  (
s  /  2 ) ) )
379 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  /  2 )  =  0  ->  ( cos `  ( s  / 
2 ) )  =  ( cos `  0
) )
380379, 375syl6eq 2514 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  /  2 )  =  0  ->  ( cos `  ( s  / 
2 ) )  =  1 )
381380ad2antll 728 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  /\  ( s  / 
2 )  =  0 ) )  ->  ( cos `  ( s  / 
2 ) )  =  1 )
382341, 344, 365, 377, 378, 381limcco 22423 . . . . . . . . . . . . . . . . 17  |-  ( T. 
->  1  e.  (
( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  ( cos `  ( s  /  2
) ) ) lim CC  0 ) )
383 ax-1ne0 9578 . . . . . . . . . . . . . . . . . 18  |-  1  =/=  0
384383a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( T. 
->  1  =/=  0
)
385305, 306, 340, 382, 384reclimc 31862 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( 1  /  1
)  e.  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 1  / 
( cos `  (
s  /  2 ) ) ) ) lim CC  0 ) )
386 1div1e1 10258 . . . . . . . . . . . . . . . 16  |-  ( 1  /  1 )  =  1
38766fveq1i 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) ) `  s )  =  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } )  |->  1 ) `
 s )
388 eqidd 2458 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  1 )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  1 ) )
389 eqidd 2458 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  s )  ->  1  =  1 )
390 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  s  e.  ( ( -u pi (,) pi )  \  { 0 } ) )
391 1red 9628 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  1  e.  RR )
392388, 389, 390, 391fvmptd 5961 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  1 ) `  s
)  =  1 )
393387, 392syl5req 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  1  =  ( ( RR  _D  (
x  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  x ) ) `
 s ) )
394135a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 6303 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  s  ->  (
x  /  2 )  =  ( s  / 
2 ) )
396395fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  s  ->  ( cos `  ( x  / 
2 ) )  =  ( cos `  (
s  /  2 ) ) )
397396adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  s )  ->  ( cos `  ( x  / 
2 ) )  =  ( cos `  (
s  /  2 ) ) )
398394, 397, 390, 335fvmptd 5961 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( RR 
_D  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( 2  x.  ( sin `  ( x  /  2
) ) ) ) ) `  s )  =  ( cos `  (
s  /  2 ) ) )
399398eqcomd 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( cos `  (
s  /  2 ) )  =  ( ( RR  _D  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) ) `  s
) )
400393, 399oveq12d 6314 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
401400mpteq2ia 4539 . . . . . . . . . . . . . . . . 17  |-  ( 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
) ) )
402401oveq1i 6306 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  |->  ( 1  / 
( cos `  (
s  /  2 ) ) ) ) lim CC  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 ) ) ) lim CC  0 )
403385, 386, 4023eltr3g 2561 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) lim CC  0 ) )
40420, 24, 32, 34, 45, 46, 71, 140, 173, 227, 259, 304, 403lhop 22543 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) lim CC  0 ) )
405404trud 1404 . . . . . . . . . . . . 13  |-  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 ) ) ) lim CC  0 )
406 eqidd 2458 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( x  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  x )  =  ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) )
407 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  s )  ->  x  =  s )
408406, 407, 390, 307fvmptd 5961 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  x ) `  s
)  =  s )
409 eqidd 2458 . . . . . . . . . . . . . . . . 17  |-  ( 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
) ) ) ) )
410407oveq1d 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  s )  ->  (
x  /  2 )  =  ( s  / 
2 ) )
411410fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  s )  ->  ( sin `  ( x  / 
2 ) )  =  ( sin `  (
s  /  2 ) ) )
412411oveq2d 6312 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( (
-u pi (,) pi )  \  { 0 } )  /\  x  =  s )  ->  (
2  x.  ( sin `  ( x  /  2
) ) )  =  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )
41326a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  2  e.  RR )
414311resincld 13890 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( sin `  (
s  /  2 ) )  e.  RR )
415413, 414remulcld 9641 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  e.  RR )
416409, 412, 390, 415fvmptd 5961 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( -u pi (,) pi )  \  { 0 } )  ->  ( ( x  e.  ( ( -u pi (,) pi )  \  { 0 } ) 
|->  ( 2  x.  ( sin `  ( x  / 
2 ) ) ) ) `  s )  =  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )
417408, 416oveq12d 6314 . . . . . . . . . . . . . . 15  |-  ( 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
) ) ) ) )
418417mpteq2ia 4539 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) )
419418oveq1i 6306 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) lim
CC  0 )  =  ( ( s  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) lim
CC  0 )
420405, 419eleqtri 2543 . . . . . . . . . . . 12  |-  1  e.  ( ( s  e.  ( ( -u pi (,) pi )  \  {
0 } )  |->  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) lim
CC  0 )
42110oveq1i 6306 . . . . . . . . . . . . . 14  |-  ( K lim
CC  0 )  =  ( ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) lim CC  0 )
42210feq1i 5729 . . . . . . . . . . . . . . . . . . 19  |-  ( K : ( -u pi [,] pi ) --> CC  <->  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) : ( -u pi [,] pi ) --> CC )
42314, 422mpbi 208 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =