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

Theorem fouriersw 31855
Description: Fourier series convergence, for the square wave function. Where  F is discontinuous, the series converges to  0, the average value of the left and the right limits. Notice that  F is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fouriersw.t  |-  T  =  ( 2  x.  pi )
fouriersw.f  |-  F  =  ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
fouriersw.x  |-  X  e.  RR
fouriersw.z  |-  S  =  ( n  e.  NN  |->  ( ( sin `  (
( ( 2  x.  n )  -  1 )  x.  X ) )  /  ( ( 2  x.  n )  -  1 ) ) )
fouriersw.y  |-  Y  =  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X
) )
Assertion
Ref Expression
fouriersw  |-  ( ( ( 4  /  pi )  x.  sum_ k  e.  NN  ( ( sin `  ( ( ( 2  x.  k )  - 
1 )  x.  X
) )  /  (
( 2  x.  k
)  -  1 ) ) )  =  Y  /\  seq 1 (  +  ,  S )  ~~>  ( ( pi  / 
4 )  x.  Y
) )
Distinct variable groups:    n, F, x    x, T    n, X, k    x, X    k, Y
Allowed substitution hints:    S( x, k, n)    T( k, n)    F( k)    Y( x, n)

Proof of Theorem fouriersw
Dummy variables  y  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11129 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
2 1zzd 10907 . . . . . . 7  |-  ( T. 
->  1  e.  ZZ )
3 eqidd 2468 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
n  e.  NN  |->  ( ( sin `  (
( ( 2  x.  n )  -  1 )  x.  X ) )  /  ( ( 2  x.  n )  -  1 ) ) )  =  ( n  e.  NN  |->  ( ( sin `  ( ( ( 2  x.  n
)  -  1 )  x.  X ) )  /  ( ( 2  x.  n )  - 
1 ) ) ) )
4 oveq2 6303 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  (
2  x.  n )  =  ( 2  x.  k ) )
54oveq1d 6310 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
( 2  x.  n
)  -  1 )  =  ( ( 2  x.  k )  - 
1 ) )
65oveq1d 6310 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( ( 2  x.  n )  -  1 )  x.  X )  =  ( ( ( 2  x.  k )  -  1 )  x.  X ) )
76fveq2d 5876 . . . . . . . . . . 11  |-  ( n  =  k  ->  ( sin `  ( ( ( 2  x.  n )  -  1 )  x.  X ) )  =  ( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) ) )
87, 5oveq12d 6313 . . . . . . . . . 10  |-  ( n  =  k  ->  (
( sin `  (
( ( 2  x.  n )  -  1 )  x.  X ) )  /  ( ( 2  x.  n )  -  1 ) )  =  ( ( sin `  ( ( ( 2  x.  k )  - 
1 )  x.  X
) )  /  (
( 2  x.  k
)  -  1 ) ) )
98adantl 466 . . . . . . . . 9  |-  ( ( k  e.  NN  /\  n  =  k )  ->  ( ( sin `  (
( ( 2  x.  n )  -  1 )  x.  X ) )  /  ( ( 2  x.  n )  -  1 ) )  =  ( ( sin `  ( ( ( 2  x.  k )  - 
1 )  x.  X
) )  /  (
( 2  x.  k
)  -  1 ) ) )
10 id 22 . . . . . . . . 9  |-  ( k  e.  NN  ->  k  e.  NN )
11 ovex 6320 . . . . . . . . . 10  |-  ( ( sin `  ( ( ( 2  x.  k
)  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  - 
1 ) )  e. 
_V
1211a1i 11 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) )  e.  _V )
133, 9, 10, 12fvmptd 5962 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( sin `  (
( ( 2  x.  n )  -  1 )  x.  X ) )  /  ( ( 2  x.  n )  -  1 ) ) ) `  k )  =  ( ( sin `  ( ( ( 2  x.  k )  - 
1 )  x.  X
) )  /  (
( 2  x.  k
)  -  1 ) ) )
1413adantl 466 . . . . . . 7  |-  ( ( T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( sin `  (
( ( 2  x.  n )  -  1 )  x.  X ) )  /  ( ( 2  x.  n )  -  1 ) ) ) `  k )  =  ( ( sin `  ( ( ( 2  x.  k )  - 
1 )  x.  X
) )  /  (
( 2  x.  k
)  -  1 ) ) )
15 ax-resscn 9561 . . . . . . . . . . . . 13  |-  RR  C_  CC
16 2z 10908 . . . . . . . . . . . . . . . . 17  |-  2  e.  ZZ
1716a1i 11 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  2  e.  ZZ )
18 nnz 10898 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  ZZ )
1917, 18zmulcld 10984 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  ZZ )
20 1zzd 10907 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  1  e.  ZZ )
2119, 20zsubcld 10983 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  ZZ )
2221zred 10978 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  RR )
2315, 22sseldi 3507 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  CC )
24 fouriersw.x . . . . . . . . . . . . . 14  |-  X  e.  RR
2515, 24sselii 3506 . . . . . . . . . . . . 13  |-  X  e.  CC
2625a1i 11 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  X  e.  CC )
2723, 26jca 532 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  -  1 )  e.  CC  /\  X  e.  CC )
)
28 mulcl 9588 . . . . . . . . . . 11  |-  ( ( ( ( 2  x.  k )  -  1 )  e.  CC  /\  X  e.  CC )  ->  ( ( ( 2  x.  k )  - 
1 )  x.  X
)  e.  CC )
2927, 28syl 16 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  -  1 )  x.  X )  e.  CC )
30 sincl 13739 . . . . . . . . . 10  |-  ( ( ( ( 2  x.  k )  -  1 )  x.  X )  e.  CC  ->  ( sin `  ( ( ( 2  x.  k )  -  1 )  x.  X ) )  e.  CC )
3129, 30syl 16 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( sin `  ( ( ( 2  x.  k )  -  1 )  x.  X ) )  e.  CC )
32 0re 9608 . . . . . . . . . . 11  |-  0  e.  RR
3332a1i 11 . . . . . . . . . 10  |-  ( k  e.  NN  ->  0  e.  RR )
34 2re 10617 . . . . . . . . . . . . . 14  |-  2  e.  RR
3534a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  2  e.  RR )
36 1re 9607 . . . . . . . . . . . . . 14  |-  1  e.  RR
3736a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  e.  RR )
3835, 37remulcld 9636 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  1 )  e.  RR )
3938, 37resubcld 9999 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  1 )  -  1 )  e.  RR )
40 0lt1 10087 . . . . . . . . . . . . 13  |-  0  <  1
4115, 34sselii 3506 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
4241mulid1i 9610 . . . . . . . . . . . . . . 15  |-  ( 2  x.  1 )  =  2
4342oveq1i 6305 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
44 2m1e1 10662 . . . . . . . . . . . . . 14  |-  ( 2  -  1 )  =  1
4543, 44eqtr2i 2497 . . . . . . . . . . . . 13  |-  1  =  ( ( 2  x.  1 )  - 
1 )
4640, 45breqtri 4476 . . . . . . . . . . . 12  |-  0  <  ( ( 2  x.  1 )  -  1 )
4746a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  0  <  ( ( 2  x.  1 )  -  1 ) )
4819zred 10978 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  RR )
49 nnre 10555 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  RR )
50 2pos 10639 . . . . . . . . . . . . . . 15  |-  0  <  2
5132, 34, 50ltleii 9719 . . . . . . . . . . . . . 14  |-  0  <_  2
5251a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  0  <_  2 )
53 nnge1 10574 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  <_  k )
5437, 49, 35, 52, 53lemul2ad 10498 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  1 )  <_  ( 2  x.  k ) )
5538, 48, 37, 54lesub1dd 10180 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  1 )  -  1 )  <_  ( ( 2  x.  k )  - 
1 ) )
5633, 39, 22, 47, 55ltletrd 9753 . . . . . . . . . 10  |-  ( k  e.  NN  ->  0  <  ( ( 2  x.  k )  -  1 ) )
5733, 56gtned 9731 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  =/=  0 )
5831, 23, 57divcld 10332 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) )  e.  CC )
5958adantl 466 . . . . . . 7  |-  ( ( T.  /\  k  e.  NN )  ->  (
( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) )  e.  CC )
60 pire 22718 . . . . . . . . . . . . . 14  |-  pi  e.  RR
6115, 60sselii 3506 . . . . . . . . . . . . 13  |-  pi  e.  CC
6261a1i 11 . . . . . . . . . . . 12  |-  ( T. 
->  pi  e.  CC )
63 4cn 10625 . . . . . . . . . . . . 13  |-  4  e.  CC
6463a1i 11 . . . . . . . . . . . 12  |-  ( T. 
->  4  e.  CC )
65 4ne0 10644 . . . . . . . . . . . . 13  |-  4  =/=  0
6665a1i 11 . . . . . . . . . . . 12  |-  ( T. 
->  4  =/=  0
)
6762, 64, 66divcld 10332 . . . . . . . . . . 11  |-  ( T. 
->  ( pi  /  4
)  e.  CC )
6832a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  0  e.  RR )
6915, 68sseldi 3507 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  0  e.  CC )
7063a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  4  e.  CC )
71 nncn 10556 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  n  e.  CC )
72 mulcl 9588 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  CC  /\  pi  e.  CC )  -> 
( n  x.  pi )  e.  CC )
7371, 61, 72sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  (
n  x.  pi )  e.  CC )
7461a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  pi  e.  CC )
75 nnne0 10580 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  n  =/=  0 )
76 pipos 22720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  <  pi
7732, 76gtneii 9708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  pi  =/=  0
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  pi  =/=  0 )
7971, 74, 75, 78mulne0d 10213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  (
n  x.  pi )  =/=  0 )
8070, 73, 79divcld 10332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  (
4  /  ( n  x.  pi ) )  e.  CC )
8125a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  X  e.  CC )
8271, 81mulcld 9628 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  (
n  x.  X )  e.  CC )
8382sincld 13743 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  ( sin `  ( n  x.  X ) )  e.  CC )
8480, 83mulcld 9628 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  (
( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  CC )
8569, 84ifcld 3988 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )  e.  CC )
8685rgen 2827 . . . . . . . . . . . . . . . . . 18  |-  A. n  e.  NN  if ( 2 
||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) )  e.  CC
87 eqid 2467 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )  =  ( n  e.  NN  |->  if ( 2 
||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )
8887fmpt 6053 . . . . . . . . . . . . . . . . . 18  |-  ( A. n  e.  NN  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )  e.  CC  <->  ( n  e.  NN  |->  if ( 2 
||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) ) : NN --> CC )
8986, 88mpbi 208 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) ) : NN --> CC
9089a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) : NN --> CC )
91 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN  ->  (
n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )  =  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) ) )
92 breq2 4457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  k  ->  (
2  ||  n  <->  2  ||  k ) )
93 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  k  ->  0  =  0 )
94 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  k  ->  (
n  x.  pi )  =  ( k  x.  pi ) )
9594oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  k  ->  (
4  /  ( n  x.  pi ) )  =  ( 4  / 
( k  x.  pi ) ) )
96 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  k  ->  (
n  x.  X )  =  ( k  x.  X ) )
9796fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  k  ->  ( sin `  ( n  x.  X ) )  =  ( sin `  (
k  x.  X ) ) )
9895, 97oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  k  ->  (
( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) )  =  ( ( 4  / 
( k  x.  pi ) )  x.  ( sin `  ( k  x.  X ) ) ) )
9992, 93, 98ifeq123d 31337 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )  =  if ( 2 
||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) ) )
10099adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  n  =  k )  ->  if ( 2  ||  n ,  0 , 
( ( 4  / 
( n  x.  pi ) )  x.  ( sin `  ( n  x.  X ) ) ) )  =  if ( 2  ||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) ) )
10132elexi 3128 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
102 ovex 6320 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) )  e.  _V
103101, 102ifex 4014 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 2  ||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) )  e. 
_V
104103a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN  ->  if ( 2  ||  k ,  0 ,  ( ( 4  /  (
k  x.  pi ) )  x.  ( sin `  ( k  x.  X
) ) ) )  e.  _V )
10591, 100, 10, 104fvmptd 5962 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) `  k )  =  if ( 2 
||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) ) )
106105adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) ) `
 k )  =  if ( 2  ||  k ,  0 , 
( ( 4  / 
( k  x.  pi ) )  x.  ( sin `  ( k  x.  X ) ) ) ) )
107 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( k  / 
2 )  e.  NN )
108 simpl 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  k  e.  NN )
109 2nn 10705 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  NN
110109a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  2  e.  NN )
111 nndivdvds 13870 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN  /\  2  e.  NN )  ->  ( 2  ||  k  <->  ( k  /  2 )  e.  NN ) )
112108, 110, 111syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( 2  ||  k 
<->  ( k  /  2
)  e.  NN ) )
113107, 112mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  2  ||  k
)
114113iftrued 3953 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  if ( 2 
||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) )  =  0 )
115106, 114eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) ) `
 k )  =  0 )
1161153adant1 1014 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  k  e.  NN  /\  ( k  /  2 )  e.  NN )  ->  (
( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) `  k )  =  0 )
117 breq2 4457 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  =  n  ->  (
2  ||  m  <->  2  ||  n ) )
118 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  =  0
119118a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  =  n  ->  0  =  0 )
120 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  =  n  ->  (
m  x.  pi )  =  ( n  x.  pi ) )
121120oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  =  n  ->  (
4  /  ( m  x.  pi ) )  =  ( 4  / 
( n  x.  pi ) ) )
122117, 119, 121ifeq123d 31337 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  if ( 2  ||  m ,  0 ,  ( 4  /  ( m  x.  pi ) ) )  =  if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) ) )
123 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  =  n  ->  (
m  x.  X )  =  ( n  x.  X ) )
124123fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  ( sin `  ( m  x.  X ) )  =  ( sin `  (
n  x.  X ) ) )
125122, 124oveq12d 6313 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  ( if ( 2  ||  m ,  0 ,  ( 4  /  ( m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X
) ) )  =  ( if ( 2 
||  n ,  0 ,  ( 4  / 
( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) ) )
126125cbvmptv 4544 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN  |->  ( if ( 2  ||  m ,  0 ,  ( 4  /  ( m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X
) ) ) )  =  ( n  e.  NN  |->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) ) )
127 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  (
m  e.  NN  |->  ( if ( 2  ||  m ,  0 , 
( 4  /  (
m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X ) ) ) )  =  ( m  e.  NN  |->  ( if ( 2  ||  m ,  0 ,  ( 4  /  ( m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X
) ) ) ) )
128125adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN  /\  m  =  n )  ->  ( if ( 2 
||  m ,  0 ,  ( 4  / 
( m  x.  pi ) ) )  x.  ( sin `  (
m  x.  X ) ) )  =  ( if ( 2  ||  n ,  0 , 
( 4  /  (
n  x.  pi ) ) )  x.  ( sin `  ( n  x.  X ) ) ) )
129 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  n  e.  NN )
13069, 80ifcld 3988 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  NN  ->  if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  e.  CC )
131130, 83mulcld 9628 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  CC )
132127, 128, 129, 131fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( if ( 2  ||  m ,  0 , 
( 4  /  (
m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X ) ) ) ) `  n )  =  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) ) )
133 iftrue 3951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2 
||  n  ->  if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  =  0 )
134133oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 2 
||  n  ->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  ( n  x.  X
) ) )  =  ( 0  x.  ( sin `  ( n  x.  X ) ) ) )
135134adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( n  e.  NN  /\  2  ||  n )  -> 
( if ( 2 
||  n ,  0 ,  ( 4  / 
( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) )  =  ( 0  x.  ( sin `  ( n  x.  X
) ) ) )
13683mul02d 9789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  e.  NN  ->  (
0  x.  ( sin `  ( n  x.  X
) ) )  =  0 )
137136adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( n  e.  NN  /\  2  ||  n )  -> 
( 0  x.  ( sin `  ( n  x.  X ) ) )  =  0 )
138135, 137eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( n  e.  NN  /\  2  ||  n )  -> 
( if ( 2 
||  n ,  0 ,  ( 4  / 
( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) )  =  0 )
139 iftrue 3951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 2 
||  n  ->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )  =  0 )
140139eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 2 
||  n  ->  0  =  if ( 2  ||  n ,  0 , 
( ( 4  / 
( n  x.  pi ) )  x.  ( sin `  ( n  x.  X ) ) ) ) )
141140adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( n  e.  NN  /\  2  ||  n )  -> 
0  =  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )
142138, 141eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( n  e.  NN  /\  2  ||  n )  -> 
( if ( 2 
||  n ,  0 ,  ( 4  / 
( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) )  =  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
143 iffalse 3954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  2  ||  n  ->  if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  =  ( 4  /  ( n  x.  pi ) ) )
144143oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  2  ||  n  -> 
( if ( 2 
||  n ,  0 ,  ( 4  / 
( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) )  =  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )
145144adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( n  e.  NN  /\  -.  2  ||  n )  ->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) )  =  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )
146 iffalse 3954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  2  ||  n  ->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )  =  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) )
147146eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  2  ||  n  -> 
( ( 4  / 
( n  x.  pi ) )  x.  ( sin `  ( n  x.  X ) ) )  =  if ( 2 
||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )
148147adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( n  e.  NN  /\  -.  2  ||  n )  ->  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) )  =  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
149145, 148eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( n  e.  NN  /\  -.  2  ||  n )  ->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) )  =  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
150142, 149pm2.61dan 789 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  NN  ->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  ( n  x.  X
) ) )  =  if ( 2  ||  n ,  0 , 
( ( 4  / 
( n  x.  pi ) )  x.  ( sin `  ( n  x.  X ) ) ) ) )
151150adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN  /\  m  =  n )  ->  ( if ( 2 
||  n ,  0 ,  ( 4  / 
( n  x.  pi ) ) )  x.  ( sin `  (
n  x.  X ) ) )  =  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
152128, 151eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN  /\  m  =  n )  ->  ( if ( 2 
||  m ,  0 ,  ( 4  / 
( m  x.  pi ) ) )  x.  ( sin `  (
m  x.  X ) ) )  =  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
153127, 152, 129, 85fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( if ( 2  ||  m ,  0 , 
( 4  /  (
m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X ) ) ) ) `  n )  =  if ( 2 
||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )
154132, 153eqtr3d 2510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  ( n  x.  X
) ) )  =  if ( 2  ||  n ,  0 , 
( ( 4  / 
( n  x.  pi ) )  x.  ( sin `  ( n  x.  X ) ) ) ) )
155154mpteq2ia 4535 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  |->  ( if ( 2  ||  n ,  0 ,  ( 4  /  ( n  x.  pi ) ) )  x.  ( sin `  ( n  x.  X
) ) ) )  =  ( n  e.  NN  |->  if ( 2 
||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )
156126, 155eqtr2i 2497 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )  =  ( m  e.  NN  |->  ( if ( 2  ||  m ,  0 ,  ( 4  /  ( m  x.  pi ) ) )  x.  ( sin `  (
m  x.  X ) ) ) )
157 seqeq3 12092 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )  =  ( m  e.  NN  |->  ( if ( 2  ||  m ,  0 ,  ( 4  /  ( m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X
) ) ) )  ->  seq 1 (  +  ,  ( n  e.  NN  |->  if ( 2 
||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) ) )  =  seq 1
(  +  ,  ( m  e.  NN  |->  ( if ( 2  ||  m ,  0 , 
( 4  /  (
m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X ) ) ) ) ) )
158156, 157ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  seq 1
(  +  ,  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) )  =  seq 1 (  +  , 
( m  e.  NN  |->  ( if ( 2  ||  m ,  0 , 
( 4  /  (
m  x.  pi ) ) )  x.  ( sin `  ( m  x.  X ) ) ) ) )
159 fouriersw.f . . . . . . . . . . . . . . . . . . . . 21  |-  F  =  ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
16036renegcli 9892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u 1  e.  RR
161 ifcl 3987 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR  /\  -u 1  e.  RR )  ->  if ( ( x  mod  T )  <  pi ,  1 ,  -u 1 )  e.  RR )
16236, 160, 161mp2an 672 . . . . . . . . . . . . . . . . . . . . . 22  |-  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
)  e.  RR
163162a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  e.  RR )
164159, 163fmpti 6055 . . . . . . . . . . . . . . . . . . . 20  |-  F : RR
--> RR
165 fouriersw.t . . . . . . . . . . . . . . . . . . . 20  |-  T  =  ( 2  x.  pi )
166 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  y  ->  (
x  mod  T )  =  ( y  mod 
T ) )
167166breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  y  ->  (
( x  mod  T
)  <  pi  <->  ( y  mod  T )  <  pi ) )
168 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  y  ->  1  =  1 )
169 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  y  ->  -u 1  =  -u 1 )
170167, 168, 169ifeq123d 31337 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  y  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  if ( ( y  mod  T
)  <  pi , 
1 ,  -u 1
) )
171170cbvmptv 4544 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( y  e.  RR  |->  if ( ( y  mod 
T )  <  pi ,  1 ,  -u
1 ) )
172159, 171eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F  =  ( y  e.  RR  |->  if ( ( y  mod 
T )  <  pi ,  1 ,  -u
1 ) )
173172a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  F  =  ( y  e.  RR  |->  if ( ( y  mod  T )  <  pi ,  1 ,  -u 1 ) ) )
174 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  ( x  +  T )  ->  (
y  mod  T )  =  ( ( x  +  T )  mod 
T ) )
17534, 60remulcli 9622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 2  x.  pi )  e.  RR
176165, 175eqeltri 2551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  T  e.  RR
177176recni 9620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  T  e.  CC
178177mulid2i 9611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 1  x.  T )  =  T
179178eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  T  =  ( 1  x.  T
)
180179oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  +  T )  =  ( x  +  ( 1  x.  T ) )
181180oveq1i 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  +  T )  mod  T )  =  ( ( x  +  ( 1  x.  T
) )  mod  T
)
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  ( x  +  T )  ->  (
( x  +  T
)  mod  T )  =  ( ( x  +  ( 1  x.  T ) )  mod 
T ) )
183174, 182eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( x  +  T )  ->  (
y  mod  T )  =  ( ( x  +  ( 1  x.  T ) )  mod 
T ) )
184183adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( y  mod  T
)  =  ( ( x  +  ( 1  x.  T ) )  mod  T ) )
185 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  x  e.  RR )
18634, 60mulgt0i 9728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0  <  2  /\  0  <  pi )  ->  0  <  (
2  x.  pi ) )
18750, 76, 186mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  0  <  ( 2  x.  pi )
188165eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 2  x.  pi )  =  T
189187, 188breqtri 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  <  T
190 elrp 11234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( T  e.  RR+  <->  ( T  e.  RR  /\  0  < 
T ) )
191176, 189, 190mpbir2an 918 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  T  e.  RR+
192191a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  T  e.  RR+ )
193 1zzd 10907 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
1  e.  ZZ )
194 modcyc 12011 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  RR  /\  T  e.  RR+  /\  1  e.  ZZ )  ->  (
( x  +  ( 1  x.  T ) )  mod  T )  =  ( x  mod  T ) )
195185, 192, 193, 194syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( ( x  +  ( 1  x.  T
) )  mod  T
)  =  ( x  mod  T ) )
196184, 195eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( y  mod  T
)  =  ( x  mod  T ) )
197196breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( ( y  mod 
T )  <  pi  <->  ( x  mod  T )  <  pi ) )
198 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
1  =  1 )
199 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  -u 1  =  -u 1
)
200197, 198, 199ifeq123d 31337 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  if ( ( y  mod 
T )  <  pi ,  1 ,  -u
1 )  =  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
201 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  x  e.  RR )
202176a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  T  e.  RR )
203201, 202readdcld 9635 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  +  T )  e.  RR )
204173, 200, 203, 163fvmptd 5962 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  ( F `  ( x  +  T ) )  =  if ( ( x  mod  T )  < 
pi ,  1 , 
-u 1 ) )
205159fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  e.  RR )  ->  ( F `  x )  =  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
206201, 163, 205syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  ( F `  x )  =  if ( ( x  mod  T )  < 
pi ,  1 , 
-u 1 ) )
207206eqcomd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  ( F `
 x ) )
208 eqidd 2468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  ( F `  x )  =  ( F `  x ) )
209204, 207, 2083eqtrd 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
210 eqid 2467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  =  ( ( RR  _D  F
)  |`  ( -u pi (,) pi ) )
211 snfi 7608 . . . . . . . . . . . . . . . . . . . . 21  |-  { 0 }  e.  Fin
212 eldifi 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  e.  ( -u pi (,) pi ) )
213212adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  /\  -.  x  =  0
)  ->  x  e.  ( -u pi (,) pi ) )
214 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  /\  -.  x  =  0
)  ->  -.  x  =  0 )
215 0xr 9652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  0  e.  RR*
216215a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  -> 
0  e.  RR* )
21760rexri 9658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  pi  e.  RR*
218217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  pi  e.  RR* )
219 elioore 11571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  RR )
220219adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  RR )
221 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  -> 
0  <  x )
22260renegcli 9892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -u pi  e.  RR
223222rexri 9658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  -u pi  e.  RR*
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  ( -u pi (,) pi )  ->  -u pi  e.  RR* )
225217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  ( -u pi (,) pi )  ->  pi  e.  RR* )
226 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  ( -u pi (,) pi ) )
227 iooltub 31435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( -u pi (,) pi ) )  ->  x  <  pi )
228224, 225, 226, 227syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( -u pi (,) pi )  ->  x  <  pi )
229228adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  <  pi )
230216, 218, 220, 221, 229eliood 31418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  ( 0 (,) pi ) )
231 negpilt0 31362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -u pi  <  0
232222, 32, 231ltleii 9719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  -u pi  <_  0
233 iooss1 11576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
-u pi  e.  RR*  /\  -u pi  <_  0 )  ->  ( 0 (,) pi )  C_  ( -u pi (,) pi ) )
234223, 232, 233mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 0 (,) pi )  C_  ( -u pi (,) pi )
235 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( 0 (,) pi ) )
236234, 235sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( -u pi (,) pi ) )
237 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( 0 (,) pi )  |->  0 )  =  ( x  e.  ( 0 (,) pi )  |->  0 )
238101, 237dmmpti 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  dom  (
x  e.  ( 0 (,) pi )  |->  0 )  =  ( 0 (,) pi )
239238eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0 (,) pi )  =  dom  ( x  e.  ( 0 (,) pi )  |->  0 )
240 reelprrecn 9596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  RR  e.  { RR ,  CC }
241240a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( T. 
->  RR  e.  { RR ,  CC } )
242 iooretop 21141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 0 (,) pi )  e.  ( topGen `  ran  (,) )
243 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
244243tgioo2 21176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
245242, 244eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( 0 (,) pi )  e.  ( ( TopOpen ` fld )t  RR )
246245a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( T. 
->  ( 0 (,) pi )  e.  ( ( TopOpen
` fld
)t 
RR ) )
247 1cnd 9624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( T. 
->  1  e.  CC )
248241, 246, 247dvmptconst 31566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  ( RR  _D  (
x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( x  e.  ( 0 (,) pi )  |->  0 ) )
249248trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( RR 
_D  ( x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( x  e.  ( 0 (,) pi )  |->  0 )
250249eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( 0 (,) pi )  |->  0 )  =  ( RR  _D  ( x  e.  (
0 (,) pi ) 
|->  1 ) )
251159reseq1i 5275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( F  |`  ( 0 (,) pi ) )  =  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )  |`  (
0 (,) pi ) )
252 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( 0 (,) pi )  C_  RR
253 resmpt 5329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( 0 (,) pi ) 
C_  RR  ->  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )  |`  (
0 (,) pi ) )  =  ( x  e.  ( 0 (,) pi )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) ) )
254252, 253ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )  |`  (
0 (,) pi ) )  =  ( x  e.  ( 0 (,) pi )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )
255236, 219syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  RR )
256191a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( 0 (,) pi )  ->  T  e.  RR+ )
25732a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( 0 (,) pi )  ->  0  e.  RR )
258215a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( 0 (,) pi )  ->  0  e.  RR* )
259217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( 0 (,) pi )  ->  pi  e.  RR* )
260 ioogtlb 31415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( 0 (,) pi ) )  ->  0  <  x )
261258, 259, 235, 260syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( 0 (,) pi )  ->  0  <  x )
262257, 255, 261ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( 0 (,) pi )  ->  0  <_  x )
26360a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( 0 (,) pi )  ->  pi  e.  RR )
264176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( 0 (,) pi )  ->  T  e.  RR )
265236, 228syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( 0 (,) pi )  ->  x  <  pi )
26660, 76elrpii 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  pi  e.  RR+
267 2timesgt 31375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( pi  e.  RR+  ->  pi  <  ( 2  x.  pi ) )
268266, 267ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  pi  <  ( 2  x.  pi )
269268, 188breqtri 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  pi  <  T
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( 0 (,) pi )  ->  pi  <  T )
271255, 263, 264, 265, 270lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( 0 (,) pi )  ->  x  <  T )
272 modid 12000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( x  e.  RR  /\  T  e.  RR+ )  /\  ( 0  <_  x  /\  x  <  T ) )  ->  ( x  mod  T )  =  x )
273255, 256, 262, 271, 272syl22anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( 0 (,) pi )  ->  (
x  mod  T )  =  x )
274273, 265eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( 0 (,) pi )  ->  (
x  mod  T )  <  pi )
275274iftrued 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( 0 (,) pi )  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  1 )
276275mpteq2ia 4535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( x  e.  ( 0 (,) pi )  |->  1 )
277251, 254, 2763eqtri 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( F  |`  ( 0 (,) pi ) )  =  ( x  e.  ( 0 (,) pi )  |->  1 )
278277eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( 0 (,) pi )  |->  1 )  =  ( F  |`  ( 0 (,) pi ) )
279278oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( RR 
_D  ( x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( RR  _D  ( F  |`  ( 0 (,) pi ) ) )
280201ssriv 3513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  RR  C_  RR
281 fss 5745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( F : RR --> RR  /\  RR  C_  CC )  ->  F : RR --> CC )
282164, 15, 281mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  F : RR
--> CC
283 dvresioo 31574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( RR  C_  RR  /\  F : RR --> CC )  -> 
( RR  _D  ( F  |`  ( 0 (,) pi ) ) )  =  ( ( RR 
_D  F )  |`  ( 0 (,) pi ) ) )
284280, 282, 283mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( RR 
_D  ( F  |`  ( 0 (,) pi ) ) )  =  ( ( RR  _D  F )  |`  (
0 (,) pi ) )
285250, 279, 2843eqtri 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( 0 (,) pi )  |->  0 )  =  ( ( RR 
_D  F )  |`  ( 0 (,) pi ) )
286285dmeqi 5210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  dom  (
x  e.  ( 0 (,) pi )  |->  0 )  =  dom  (
( RR  _D  F
)  |`  ( 0 (,) pi ) )
287239, 286eqtr2i 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  dom  (
( RR  _D  F
)  |`  ( 0 (,) pi ) )  =  ( 0 (,) pi )
288 ssdmres 5301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 0 (,) pi ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( 0 (,) pi ) )  =  ( 0 (,) pi ) )
289287, 288mpbir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 0 (,) pi )  C_  dom  ( RR  _D  F
)
290289, 235sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  dom  ( RR  _D  F ) )
291236, 290elind 3693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) ) )
292 dmres 5300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  =  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) )
293292eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
-u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  =  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )
294293a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( 0 (,) pi )  ->  (
( -u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  =  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
295291, 294eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
296230, 295syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
297296adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  0  <  x )  ->  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
298223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -u pi  e.  RR* )
299215a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  -> 
0  e.  RR* )
300219ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  RR )
301 ioogtlb 31415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( -u pi (,) pi ) )  ->  -u pi  <  x )
302224, 225, 226, 301syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( -u pi (,) pi )  ->  -u pi  <  x )
303302ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -u pi  <  x )
30432a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  -> 
0  e.  RR )
305 neqne 31339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -.  x  =  0  ->  x  =/=  0 )
306305ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  =/=  0 )
307 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -.  0  <  x )
308300, 304, 306, 307lttri5d 31399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  <  0 )
309298, 299, 300, 303, 308eliood 31418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  ( -u pi (,) 0 ) )
31032, 60, 76ltleii 9719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  0  <_  pi
311 iooss2 11577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( pi  e.  RR*  /\  0  <_  pi )  ->  ( -u pi (,) 0 ) 
C_  ( -u pi (,) pi ) )
312217, 310, 311mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -u pi (,) 0 )  C_  ( -u pi (,) pi )
313 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( -u pi (,) 0 ) )
314312, 313sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( -u pi (,) pi ) )
315 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( x  e.  ( -u pi (,) 0 )  |->  0 )
316101, 315dmmpti 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  dom  (
x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( -u pi (,) 0 )
317316eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -u pi (,) 0 )  =  dom  ( x  e.  ( -u pi (,) 0 )  |->  0 )
318 iooretop 21141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( -u pi (,) 0 )  e.  ( topGen `  ran  (,) )
319318, 244eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( -u pi (,) 0 )  e.  ( ( TopOpen ` fld )t  RR )
320319a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  ( -u pi (,) 0 )  e.  ( ( TopOpen ` fld )t  RR ) )
321247negcld 9929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  -u 1  e.  CC )
322241, 320, 321dvmptconst 31566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( T. 
->  ( RR  _D  (
x  e.  ( -u pi (,) 0 )  |->  -u
1 ) )  =  ( x  e.  (
-u pi (,) 0
)  |->  0 ) )
323322trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( RR 
_D  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
) )  =  ( x  e.  ( -u pi (,) 0 )  |->  0 )
324323eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( RR  _D  ( x  e.  ( -u pi (,) 0 ) 
|->  -u 1 ) )
325159reseq1i 5275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( F  |`  ( -u pi (,) 0 ) )  =  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi ,  1 ,  -u 1 ) )  |`  ( -u pi (,) 0 ) )
326 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( -u pi (,) 0 )  C_  RR
327 resmpt 5329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
-u pi (,) 0
)  C_  RR  ->  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )  |`  ( -u pi (,) 0 ) )  =  ( x  e.  ( -u pi (,) 0 )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) ) )
328326, 327ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )  |`  ( -u pi (,) 0 ) )  =  ( x  e.  ( -u pi (,) 0 )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )
32960a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  e.  RR )
330314, 219syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  RR )
331330, 203syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  e.  RR )
332 2times 10666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( pi  e.  CC  ->  (
2  x.  pi )  =  ( pi  +  pi ) )
33361, 332ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( 2  x.  pi )  =  ( pi  +  pi )
334165, 333eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  T  =  ( pi  +  pi )
335334oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( -u pi  +  T )  =  ( -u pi  +  ( pi  +  pi ) )
33615, 222sselii 3506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  -u pi  e.  CC
337336, 61, 61addassi 9616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
-u pi  +  pi )  +  pi )  =  ( -u pi  +  ( pi  +  pi ) )
338337eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( -u pi  +  ( pi  +  pi ) )  =  ( ( -u pi  +  pi )  +  pi )
339336, 61addcomi 9782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( -u pi  +  pi )  =  ( pi  +  -u pi )
34061negidi 9900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( pi  +  -u pi )  =  0
341339, 340eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( -u pi  +  pi )  =  0
342341oveq1i 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
-u pi  +  pi )  +  pi )  =  ( 0  +  pi )
34361addid2i 9779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( 0  +  pi )  =  pi
344342, 343eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
-u pi  +  pi )  +  pi )  =  pi
345335, 338, 3443eqtrri 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  pi  =  ( -u pi  +  T
)
346345a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  =  ( -u pi  +  T ) )
347222a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( -u pi (,) 0 )  ->  -u pi  e.  RR )
348176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  RR )
349314, 302syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( -u pi (,) 0 )  ->  -u pi  <  x )
350347, 330, 348, 349ltadd1dd 10175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( -u pi  +  T )  <  ( x  +  T ) )
351346, 350eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <  ( x  +  T
) )
352329, 331, 351ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <_  ( x  +  T
) )
353 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( x  +  T ) )
35432a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  e.  RR )
355222, 176readdcli 9621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( -u pi  +  T )  e.  RR
356355a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( -u pi  +  T )  e.  RR )
35776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  pi )
358357, 346breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  ( -u pi  +  T ) )
359354, 356, 331, 358, 350lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  ( x  +  T
) )
360354, 331, 359ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <_  ( x  +  T
) )
36115, 330sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  CC )
362177a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  CC )
363361, 362addcomd 9793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( T  +  x ) )
364223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( x  e.  ( -u pi (,) 0 )  ->  -u pi  e.  RR* )
365215a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  e.  RR* )
366 iooltub 31435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  x  e.  ( -u pi (,) 0 ) )  ->  x  <  0 )
367364, 365, 313, 366syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  <  0 )
368 ltaddneg 31384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( x  e.  RR  /\  T  e.  RR )  ->  ( x  <  0  <->  ( T  +  x )  <  T ) )
369330, 348, 368syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  <  0  <->  ( T  +  x )  <  T
) )
370367, 369mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( T  +  x )  <  T )
371363, 370eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  <  T )
372360, 371jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
0  <_  ( x  +  T )  /\  (
x  +  T )  <  T ) )
373191a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  RR+ )
374 modid2 12003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( ( x  +  T
)  e.  RR  /\  T  e.  RR+ )  -> 
( ( ( x  +  T )  mod 
T )  =  ( x  +  T )  <-> 
( 0  <_  (
x  +  T )  /\  ( x  +  T )  <  T
) ) )
375331, 373, 374syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( ( x  +  T )  mod  T
)  =  ( x  +  T )  <->  ( 0  <_  ( x  +  T )  /\  (
x  +  T )  <  T ) ) )
376372, 375mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( x  +  T
)  mod  T )  =  ( x  +  T ) )
377376eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( ( x  +  T )  mod 
T ) )
378181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  RR  ->  (
( x  +  T
)  mod  T )  =  ( ( x  +  ( 1  x.  T ) )  mod 
T ) )
379191a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  RR  ->  T  e.  RR+ )
380 1zzd 10907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  RR  ->  1  e.  ZZ )
381201, 379, 380, 194syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  RR  ->  (
( x  +  ( 1  x.  T ) )  mod  T )  =  ( x  mod  T ) )
382378, 381eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  RR  ->  (
( x  +  T
)  mod  T )  =  ( x  mod  T ) )
383330, 382syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( x  +  T
)  mod  T )  =  ( x  mod  T ) )
384353, 377, 3833eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( x  mod  T ) )
385352, 384breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <_  ( x  mod  T
) )
386384, 331eqeltrrd 2556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  mod  T )  e.  RR )
387329, 386lenltd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
pi  <_  ( x  mod  T )  <->  -.  ( x  mod  T )  <  pi ) )
388385, 387mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  -.  ( x  mod  T )  <  pi )
389388iffalsed 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  -u 1
)
390389mpteq2ia 4535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( -u pi (,) 0 )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( x  e.  ( -u pi (,) 0 )  |->  -u
1 )
391325, 328, 3903eqtri 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( F  |`  ( -u pi (,) 0 ) )  =  ( x  e.  (
-u pi (,) 0
)  |->  -u 1 )
392391eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( F  |`  ( -u pi (,) 0 ) )
393392oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( RR 
_D  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
) )  =  ( RR  _D  ( F  |`  ( -u pi (,) 0 ) ) )
394 dvresioo 31574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( RR  C_  RR  /\  F : RR --> CC )  -> 
( RR  _D  ( F  |`  ( -u pi (,) 0 ) ) )  =  ( ( RR 
_D  F )  |`  ( -u pi (,) 0
) ) )
395280, 282, 394mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( RR 
_D  ( F  |`  ( -u pi (,) 0
) ) )  =  ( ( RR  _D  F )  |`  ( -u pi (,) 0 ) )
396324, 393, 3953eqtri 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( ( RR 
_D  F )  |`  ( -u pi (,) 0
) )
397396dmeqi 5210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  dom  (
x  e.  ( -u pi (,) 0 )  |->  0 )  =  dom  (
( RR  _D  F
)  |`  ( -u pi (,) 0 ) )
398317, 397eqtr2i 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 )
399 ssdmres 5301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
-u pi (,) 0
)  C_  dom  ( RR 
_D  F )  <->  dom  ( ( RR  _D  F )  |`  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 ) )
400398, 399mpbir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -u pi (,) 0 )  C_  dom  ( RR  _D  F
)
401400, 313sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  dom  ( RR  _D  F ) )
402314, 401elind 3693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) ) )
403293a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( -u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  =  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
404402, 403eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
405309, 404syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
406297, 405pm2.61dan 789 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  -.  x  =  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
407213, 214, 406syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  /\  -.  x  =  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
408 eldifn 3632 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  -.  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
409408adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  /\  -.  x  =  0
)  ->  -.  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
410407, 409condan 792 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  =  0 )
411 elsn 4047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  { 0 }  <-> 
x  =  0 )
412410, 411sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  e.  { 0 } )
413412rgen 2827 . . . . . . . . . . . . . . . . . . . . . 22  |-  A. x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) x  e. 
{ 0 }
414 dfss3 3499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( -u pi (,) pi )  \  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) ) ) 
C_  { 0 }  <->  A. x  e.  (
( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) x  e.  { 0 } )
415413, 414mpbir 209 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  C_  { 0 }
416 ssfi 7752 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { 0 }  e.  Fin  /\  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  C_  { 0 } )  ->  (
( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  e. 
Fin )
417211, 415, 416mp2an 672 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  e. 
Fin
418 inss1 3723 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
-u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  C_  ( -u pi (,) pi )
419292, 418eqsstri 3539 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  ( -u pi (,) pi )
420 ioosscn 31414 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -u pi (,) pi )  C_  CC
421419, 420sstri 3518 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  CC
422421a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  C_  CC )
423 dvf 22179 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
424 fresin 5760 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( RR  _D  F ) : dom  ( RR 
_D  F ) --> CC 
->  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : ( dom  ( RR  _D  F
)  i^i  ( -u pi (,) pi ) ) --> CC )
425423, 424ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : ( dom  ( RR  _D  F )  i^i  ( -u pi (,) pi ) ) --> CC
426 ffdm 5751 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( RR  _D  F
)  |`  ( -u pi (,) pi ) ) : ( dom  ( RR 
_D  F )  i^i  ( -u pi (,) pi ) ) --> CC  ->  ( ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) ) --> CC 
/\  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  C_  ( dom  ( RR  _D  F
)  i^i  ( -u pi (,) pi ) ) ) )
427425, 426ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( RR  _D  F
)  |`  ( -u pi (,) pi ) ) : dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) --> CC  /\  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  C_  ( dom  ( RR  _D  F
)  i^i  ( -u pi (,) pi ) ) )
428427simpli 458 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) --> CC
429428a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) ) --> CC )
430223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  -u pi  e.  RR* )
431215a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  -> 
0  e.  RR* )
432219ssriv 3513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -u pi (,) pi )  C_  RR
433419sseli 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  ( -u pi (,) pi ) )
434432, 433sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  RR )
435434adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  e.  RR )
436433, 302syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  -u pi  <  x )
437436adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  -u pi  <  x )
438 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  <  0 )
439430, 431, 435, 437, 438eliood 31418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  e.  ( -u pi (,) 0 ) )
440 elun1 3676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( ( -u pi (,) 0 )  u.  (
0 (,) pi ) ) )
441439, 440syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  e.  ( ( -u pi (,) 0 )  u.  ( 0 (,) pi ) ) )
442 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
44332a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  0  e.  RR )
444442, 434syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  RR )
445 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  -.  x  <  0 )
446443, 444lenltd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  ( 0  <_  x  <->  -.  x  <  0 ) )
447445, 446mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  0  <_  x )
448 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  0  ->  x  =  0 )
44915a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  RR  C_  CC )
450282a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  F : RR --> CC )
451280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  RR  C_  RR )
452 inss2 3724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
-u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  C_  dom  ( RR  _D  F
)
453292, 452eqsstri 3539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  dom  ( RR  _D  F
)
454 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  0  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
455453, 454sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  0  e.  dom  ( RR  _D  F ) )
456244, 243dvcnp2 22191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( RR  C_  CC  /\  F : RR --> CC  /\  RR  C_  RR )  /\  0  e.  dom  ( RR 
_D  F ) )  ->  F  e.  ( ( ( topGen `  ran  (,) )  CnP  ( TopOpen ` fld )
) `  0 )
)
457449, 450, 451, 455, 456syl31anc 1231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  F  e.  ( ( ( topGen ` 
ran  (,) )  CnP  ( TopOpen
` fld
) ) `  0
) )
458280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  RR  C_  RR )
459 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
460282a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  F : RR --> CC )
46132a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  0  e.  RR )
462 mnfxr 11335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |- -oo  e.  RR*
463462a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
-> -oo  e.  RR* )
464461mnfltd 31391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
-> -oo  <  0 )
465459, 463, 461, 464lptioo2 31496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( -oo (,) 0 ) ) )
466465trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  0  e.  ( ( limPt `  ( topGen `
 ran  (,) )
) `  ( -oo (,) 0 ) )
467 incom 3696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( RR 
i^i  ( -oo (,) 0 ) )  =  ( ( -oo (,) 0 )  i^i  RR )
468 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( -oo (,) 0 )  C_  RR
469 df-ss 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( -oo (,) 0 ) 
C_  RR  <->  ( ( -oo (,) 0 )  i^i  RR )  =  ( -oo (,) 0 ) )
470468, 469mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( -oo (,) 0 )  i^i  RR )  =  ( -oo (,) 0
)
471467, 470eqtr2i 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -oo (,) 0 )  =  ( RR  i^i  ( -oo (,) 0 ) )
472471fveq2i 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
limPt `  ( topGen `  ran  (,) ) ) `  ( -oo (,) 0 ) )  =  ( ( limPt `  ( topGen `  ran  (,) )
) `  ( RR  i^i  ( -oo (,) 0
) ) )
473466, 472eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  e.  ( ( limPt `  ( topGen `
 ran  (,) )
) `  ( RR  i^i  ( -oo (,) 0
) ) )
474473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( RR  i^i  ( -oo (,) 0 ) ) ) )
475 pnfxr 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |- +oo  e.  RR*
476475a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
-> +oo  e.  RR* )
477461ltpnfd 31380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  0  < +oo )
478459, 461, 476, 477lptioo1 31497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( 0 (,) +oo ) ) )
479478trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  0  e.  ( ( limPt `  ( topGen `
 ran  (,) )
) `  ( 0 (,) +oo ) )
480 incom 3696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( RR 
i^i  ( 0 (,) +oo ) )  =  ( ( 0 (,) +oo )  i^i  RR )
481 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( 0 (,) +oo )  C_  RR
482 df-ss 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( 0 (,) +oo )  C_  RR  <->  ( ( 0 (,) +oo )  i^i 
RR )  =  ( 0 (,) +oo )
)
483481, 482mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( 0 (,) +oo )  i^i  RR )  =  ( 0 (,) +oo )
484480, 483eqtr2i 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 0 (,) +oo )  =  ( RR  i^i  (
0 (,) +oo )
)
485484fveq2i 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
limPt `  ( topGen `  ran  (,) ) ) `  (
0 (,) +oo )
)  =  ( (
limPt `  ( topGen `  ran  (,) ) ) `  ( RR  i^i  ( 0 (,) +oo ) ) )
486479, 485eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  e.  ( ( limPt `  ( topGen `
 ran  (,) )
) `  ( RR  i^i  ( 0 (,) +oo ) ) )
487486a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( RR  i^i  (
0 (,) +oo )
) ) )
488 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)
489 mnfle 11354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( -u pi  e.  RR*  -> -oo  <_  -u pi )
490223, 489ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |- -oo  <_  -u pi
491 iooss1 11576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( -oo  e.  RR*  /\ -oo  <_ 
-u pi )  -> 
( -u pi (,) 0
)  C_  ( -oo (,) 0 ) )
492462, 490, 491mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( -u pi (,) 0 )  C_  ( -oo (,) 0 )
493492a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  ( -u pi (,) 0 )  C_  ( -oo (,) 0 ) )
494468, 15sstri 3518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( -oo (,) 0 )  C_  CC
495494a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  ( -oo (,) 0
)  C_  CC )
496493, 495sstrd 3519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  ( -u pi (,) 0 )  C_  CC )
497 0cnd 9601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  0  e.  CC )
498488, 496, 321, 497constlimc 31489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( T. 
->  -u 1  e.  ( ( x  e.  (
-u pi (,) 0
)  |->  -u 1 ) lim CC  0 ) )
499498trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  -u 1  e.  ( ( x  e.  ( -u pi (,) 0 )  |->  -u 1
) lim CC  0 )
500 resabs1 5308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
-u pi (,) 0
)  C_  ( -oo (,) 0 )  ->  (
( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0 ) )  =  ( F  |`  ( -u pi (,) 0 ) ) )
501492, 500ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0
) )  =  ( F  |`  ( -u pi (,) 0 ) )
502326a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( T. 
->  ( -u pi (,) 0 )  C_  RR )
503460, 502feqresmpt 5928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( T. 
->  ( F  |`  ( -u pi (,) 0 ) )  =  ( x  e.  ( -u pi (,) 0 )  |->  ( F `
 x ) ) )
504503trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( F  |`  ( -u pi (,) 0 ) )  =  ( x  e.  (
-u pi (,) 0
)  |->  ( F `  x ) )
505392, 504eqtr2i 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  |->  ( F `
 x ) )  =  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)
506501, 504, 5053eqtrri 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0
) )
507506oveq1i 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( x  e.  ( -u pi (,) 0 )  |->  -u
1 ) lim CC  0 )  =  ( ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )
508 fssres 5757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( F : RR --> CC  /\  ( -oo (,) 0 ) 
C_  RR )  -> 
( F  |`  ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC )
509282, 468, 508mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( F  |`  ( -oo (,) 0
) ) : ( -oo (,) 0 ) --> CC
510509a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  ( F  |`  ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC )
511 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) )  =  ( ( TopOpen ` fld )t  (
( -oo (,) 0 )  u.  { 0 } ) )
512 0le0 10637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  0  <_  0
513 elioc2 11599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR )  ->  ( 0  e.  ( -u pi (,] 0 )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <_ 
0 ) ) )
514223, 32, 513mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( 0  e.  ( -u pi (,] 0 )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <_ 
0 ) )
51532, 231, 512, 514mpbir3an 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  0  e.  ( -u pi (,] 0 )
516243cnfldtop 21159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( TopOpen ` fld )  e.  Top
517 ovex 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( -oo (,] 0 )  e.  _V
518 resttop 19529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( -oo (,] 0
)  e.  _V )  ->  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )  e.  Top )
519516, 517, 518mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
TopOpen ` fld )t  ( -oo (,] 0
) )  e.  Top
520223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( T. 
->  -u pi  e.  RR* )
521 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( topGen ` 
ran  (,) )t  ( -oo (,] 0
) )
522490a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( T. 
-> -oo  <_  -u pi )
523463, 520, 461, 459, 521, 522, 461iocopn 31447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( T. 
->  ( -u pi (,] 0 )  e.  ( ( topGen `  ran  (,) )t  ( -oo (,] 0 ) ) )
524523trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( -u pi (,] 0 )  e.  ( ( topGen `  ran  (,) )t  ( -oo (,] 0
) )
525244oveq1i 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( (
TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )
526 iocssre 11616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( -oo  e.  RR*  /\  0  e.  RR )  ->  ( -oo (,] 0 )  C_  RR )
527462, 32, 526mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( -oo (,] 0 )  C_  RR
528240elexi 3128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  RR  e.  _V
529 restabs 19534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( -oo (,] 0
)  C_  RR  /\  RR  e.  _V )  ->  (
( ( TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0
) ) )
530516, 527, 528, 529mp3an 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )
531525, 530eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0 ) )
532524, 531eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( -u pi (,] 0 )  e.  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )
533 isopn3i 19451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( ( TopOpen ` fld )t  ( -oo (,] 0
) )  e.  Top  /\  ( -u pi (,] 0 )  e.  ( ( TopOpen ` fld )t  ( -oo (,] 0
) ) )  -> 
( ( int `  (
( TopOpen ` fld )t  ( -oo (,] 0
) ) ) `  ( -u pi (,] 0
) )  =  (
-u pi (,] 0
) )
534519, 532, 533mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( int `  ( (
TopOpen ` fld )t  ( -oo (,] 0
) ) ) `  ( -u pi (,] 0
) )  =  (
-u pi (,] 0
)
535534eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( -u pi (,] 0 )  =  ( ( int `  (
( TopOpen ` fld )t  ( -oo (,] 0
) ) ) `  ( -u pi (,] 0
) )
536464trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |- -oo  <  0
537 snunioo2 31431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( -oo  e.  RR*  /\  0  e.  RR*  /\ -oo  <  0 )  ->  (
( -oo (,) 0 )  u.  { 0 } )  =  ( -oo (,] 0 ) )
538462, 215, 536, 537mp3an 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( -oo (,) 0 )  u.  { 0 } )  =  ( -oo (,] 0 )
539538eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( -oo (,] 0 )  =  ( ( -oo (,) 0
)  u.  { 0 } )
540539oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
TopOpen ` fld )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) )
541540fveq2i 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( int `  ( ( TopOpen ` fld )t  ( -oo (,] 0
) ) )  =  ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) )
542 snunioo2 31431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  -u pi  <  0 )  ->  (
( -u pi (,) 0
)  u.  { 0 } )  =  (
-u pi (,] 0
) )
543223, 215, 231, 542mp3an 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
-u pi (,) 0
)  u.  { 0 } )  =  (
-u pi (,] 0
)
544543eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( -u pi (,] 0 )  =  ( ( -u pi (,) 0 )  u.  {
0 } )
545541, 544fveq12i 5877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( int `  ( (
TopOpen ` fld )t  ( -oo (,] 0
) ) ) `  ( -u pi (,] 0
) )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) )
546535, 545eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( -u pi (,] 0 )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) )
547515, 546eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  0  e.  ( ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) )
548547a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  0  e.  (
( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) ) )
549510, 493, 495, 243, 511, 548limcres 22158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  ( ( ( F  |`  ( -oo (,) 0
) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )  =  ( ( F  |`  ( -oo (,) 0
) ) lim CC  0 ) )
550549trud 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,)