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

Theorem fouriersw 37978
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 variable  y is distinct from all other variables.
StepHypRef Expression
1 nnuz 11140 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
2 1zzd 10914 . . . . . . 7  |-  ( T. 
->  1  e.  ZZ )
3 eqidd 2424 . . . . . . . . 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 6252 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  (
2  x.  n )  =  ( 2  x.  k ) )
54oveq1d 6259 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
( 2  x.  n
)  -  1 )  =  ( ( 2  x.  k )  - 
1 ) )
65oveq1d 6259 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( ( 2  x.  n )  -  1 )  x.  X )  =  ( ( ( 2  x.  k )  -  1 )  x.  X ) )
76fveq2d 5824 . . . . . . . . . . 11  |-  ( n  =  k  ->  ( sin `  ( ( ( 2  x.  n )  -  1 )  x.  X ) )  =  ( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) ) )
87, 5oveq12d 6262 . . . . . . . . . 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 467 . . . . . . . . 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 6272 . . . . . . . . . 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 5909 . . . . . . . 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 467 . . . . . . 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 2z 10915 . . . . . . . . . . . . . . 15  |-  2  e.  ZZ
1615a1i 11 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  2  e.  ZZ )
17 nnz 10905 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  k  e.  ZZ )
1816, 17zmulcld 10992 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  ZZ )
19 1zzd 10914 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  e.  ZZ )
2018, 19zsubcld 10991 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  ZZ )
2120zcnd 10987 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  CC )
22 fouriersw.x . . . . . . . . . . . . 13  |-  X  e.  RR
2322recni 9601 . . . . . . . . . . . 12  |-  X  e.  CC
2423a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  X  e.  CC )
2521, 24mulcld 9609 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  -  1 )  x.  X )  e.  CC )
2625sincld 14122 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( sin `  ( ( ( 2  x.  k )  -  1 )  x.  X ) )  e.  CC )
27 0red 9590 . . . . . . . . . 10  |-  ( k  e.  NN  ->  0  e.  RR )
28 2re 10625 . . . . . . . . . . . . . 14  |-  2  e.  RR
2928a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  2  e.  RR )
30 1red 9604 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  e.  RR )
3129, 30remulcld 9617 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  1 )  e.  RR )
3231, 30resubcld 9993 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  1 )  -  1 )  e.  RR )
3320zred 10986 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  RR )
34 0lt1 10082 . . . . . . . . . . . . 13  |-  0  <  1
35 2t1e2 10704 . . . . . . . . . . . . . . 15  |-  ( 2  x.  1 )  =  2
3635oveq1i 6254 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
37 2m1e1 10670 . . . . . . . . . . . . . 14  |-  ( 2  -  1 )  =  1
3836, 37eqtr2i 2446 . . . . . . . . . . . . 13  |-  1  =  ( ( 2  x.  1 )  - 
1 )
3934, 38breqtri 4385 . . . . . . . . . . . 12  |-  0  <  ( ( 2  x.  1 )  -  1 )
4039a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  0  <  ( ( 2  x.  1 )  -  1 ) )
4118zred 10986 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  RR )
42 nnre 10562 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  RR )
43 0le2 10646 . . . . . . . . . . . . . 14  |-  0  <_  2
4443a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  0  <_  2 )
45 nnge1 10581 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  <_  k )
4630, 42, 29, 44, 45lemul2ad 10493 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  1 )  <_  ( 2  x.  k ) )
4731, 41, 30, 46lesub1dd 10175 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  1 )  -  1 )  <_  ( ( 2  x.  k )  - 
1 ) )
4827, 32, 33, 40, 47ltletrd 9741 . . . . . . . . . 10  |-  ( k  e.  NN  ->  0  <  ( ( 2  x.  k )  -  1 ) )
4927, 48gtned 9716 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  =/=  0 )
5026, 21, 49divcld 10329 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) )  e.  CC )
5150adantl 467 . . . . . . 7  |-  ( ( T.  /\  k  e.  NN )  ->  (
( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) )  e.  CC )
52 picn 23351 . . . . . . . . . . 11  |-  pi  e.  CC
5352a1i 11 . . . . . . . . . 10  |-  ( T. 
->  pi  e.  CC )
54 4cn 10633 . . . . . . . . . . 11  |-  4  e.  CC
5554a1i 11 . . . . . . . . . 10  |-  ( T. 
->  4  e.  CC )
56 4ne0 10652 . . . . . . . . . . 11  |-  4  =/=  0
5756a1i 11 . . . . . . . . . 10  |-  ( T. 
->  4  =/=  0
)
5853, 55, 57divcld 10329 . . . . . . . . 9  |-  ( T. 
->  ( pi  /  4
)  e.  CC )
59 eqid 2423 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) ) )
60 0cnd 9582 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  0  e.  CC )
6154a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  4  e.  CC )
62 nncn 10563 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  CC )
63 mulcl 9569 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  CC  /\  pi  e.  CC )  -> 
( n  x.  pi )  e.  CC )
6462, 52, 63sylancl 666 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
n  x.  pi )  e.  CC )
6552a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  pi  e.  CC )
66 nnne0 10588 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  =/=  0 )
67 0re 9589 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
68 pipos 23352 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  pi
6967, 68gtneii 9692 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  =/=  0
7069a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  pi  =/=  0 )
7162, 65, 66, 70mulne0d 10210 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
n  x.  pi )  =/=  0 )
7261, 64, 71divcld 10329 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
4  /  ( n  x.  pi ) )  e.  CC )
7323a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  X  e.  CC )
7462, 73mulcld 9609 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
n  x.  X )  e.  CC )
7574sincld 14122 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  ( sin `  ( n  x.  X ) )  e.  CC )
7672, 75mulcld 9609 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  (
( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  CC )
7760, 76ifcld 3892 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  ->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )  e.  CC )
7859, 77fmpti 5999 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  ( n  x.  pi ) )  x.  ( sin `  (
n  x.  X ) ) ) ) ) : NN --> CC
7978a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( n  e.  NN  |->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) : NN --> CC )
80 eqidd 2424 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) ) )
81 breq2 4365 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
2  ||  n  <->  2  ||  k ) )
82 oveq1 6251 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  k  ->  (
n  x.  pi )  =  ( k  x.  pi ) )
8382oveq2d 6260 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  (
4  /  ( n  x.  pi ) )  =  ( 4  / 
( k  x.  pi ) ) )
84 oveq1 6251 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  k  ->  (
n  x.  X )  =  ( k  x.  X ) )
8584fveq2d 5824 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  ( sin `  ( n  x.  X ) )  =  ( sin `  (
k  x.  X ) ) )
8683, 85oveq12d 6262 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) )  =  ( ( 4  / 
( k  x.  pi ) )  x.  ( sin `  ( k  x.  X ) ) ) )
8781, 86ifbieq2d 3874 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) ) )
8887adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) ) )
89 c0ex 9583 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  _V
90 ovex 6272 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) )  e.  _V
9189, 90ifex 3917 . . . . . . . . . . . . . . . . . . 19  |-  if ( 2  ||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) )  e. 
_V
9291a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  NN  ->  if ( 2  ||  k ,  0 ,  ( ( 4  /  (
k  x.  pi ) )  x.  ( sin `  ( k  x.  X
) ) ) )  e.  _V )
9380, 88, 10, 92fvmptd 5909 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) )
9493adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) ) )
95 simpr 462 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( k  / 
2 )  e.  NN )
96 simpl 458 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  k  e.  NN )
97 2nn 10713 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  NN
98 nndivdvds 14249 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  2  e.  NN )  ->  ( 2  ||  k  <->  ( k  /  2 )  e.  NN ) )
9996, 97, 98sylancl 666 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( 2  ||  k 
<->  ( k  /  2
)  e.  NN ) )
10095, 99mpbird 235 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  2  ||  k
)
101100iftrued 3857 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  if ( 2 
||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) )  =  0 )
10294, 101eqtrd 2457 . . . . . . . . . . . . . . 15  |-  ( ( 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 )
1031023adant1 1023 . . . . . . . . . . . . . 14  |-  ( ( 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 )
104 fouriersw.f . . . . . . . . . . . . . . . . . 18  |-  F  =  ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
105 1re 9588 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR
106105renegcli 9881 . . . . . . . . . . . . . . . . . . . 20  |-  -u 1  e.  RR
107105, 106keepel 3916 . . . . . . . . . . . . . . . . . . 19  |-  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
)  e.  RR
108107a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  e.  RR )
109104, 108fmpti 5999 . . . . . . . . . . . . . . . . 17  |-  F : RR
--> RR
110 fouriersw.t . . . . . . . . . . . . . . . . 17  |-  T  =  ( 2  x.  pi )
111 oveq1 6251 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
x  mod  T )  =  ( y  mod 
T ) )
112111breq1d 4371 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
( x  mod  T
)  <  pi  <->  ( y  mod  T )  <  pi ) )
113112ifbid 3871 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  if ( ( y  mod  T
)  <  pi , 
1 ,  -u 1
) )
114113cbvmptv 4454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( y  e.  RR  |->  if ( ( y  mod 
T )  <  pi ,  1 ,  -u
1 ) )
115104, 114eqtri 2445 . . . . . . . . . . . . . . . . . . . 20  |-  F  =  ( y  e.  RR  |->  if ( ( y  mod 
T )  <  pi ,  1 ,  -u
1 ) )
116115a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  F  =  ( y  e.  RR  |->  if ( ( y  mod  T )  <  pi ,  1 ,  -u 1 ) ) )
117 oveq1 6251 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  +  T )  ->  (
y  mod  T )  =  ( ( x  +  T )  mod 
T ) )
118 pire 23350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  pi  e.  RR
11928, 118remulcli 9603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2  x.  pi )  e.  RR
120110, 119eqeltri 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  T  e.  RR
121120recni 9601 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  T  e.  CC
122121mulid2i 9592 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 1  x.  T )  =  T
123122eqcomi 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  T  =  ( 1  x.  T
)
124123oveq2i 6255 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  +  T )  =  ( x  +  ( 1  x.  T ) )
125124oveq1i 6254 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  +  T )  mod  T )  =  ( ( x  +  ( 1  x.  T
) )  mod  T
)
126117, 125syl6eq 2473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  +  T )  ->  (
y  mod  T )  =  ( ( x  +  ( 1  x.  T ) )  mod 
T ) )
127126adantl 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( y  mod  T
)  =  ( ( x  +  ( 1  x.  T ) )  mod  T ) )
128 simpl 458 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  x  e.  RR )
129 2pos 10647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <  2
13028, 118, 129, 68mulgt0ii 9714 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <  ( 2  x.  pi )
131110eqcomi 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 2  x.  pi )  =  T
132130, 131breqtri 4385 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  <  T
133120, 132elrpii 11251 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  T  e.  RR+
134133a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  T  e.  RR+ )
135 1zzd 10914 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
1  e.  ZZ )
136 modcyc 12077 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  T  e.  RR+  /\  1  e.  ZZ )  ->  (
( x  +  ( 1  x.  T ) )  mod  T )  =  ( x  mod  T ) )
137128, 134, 135, 136syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( ( x  +  ( 1  x.  T
) )  mod  T
)  =  ( x  mod  T ) )
138127, 137eqtrd 2457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( y  mod  T
)  =  ( x  mod  T ) )
139138breq1d 4371 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( ( y  mod 
T )  <  pi  <->  ( x  mod  T )  <  pi ) )
140139ifbid 3871 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  if ( ( y  mod 
T )  <  pi ,  1 ,  -u
1 )  =  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
141 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  x  e.  RR )
142120a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  T  e.  RR )
143141, 142readdcld 9616 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  (
x  +  T )  e.  RR )
144116, 140, 143, 108fvmptd 5909 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  ( F `  ( x  +  T ) )  =  if ( ( x  mod  T )  < 
pi ,  1 , 
-u 1 ) )
145104fvmpt2 5912 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  RR  /\  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  e.  RR )  ->  ( F `  x )  =  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
146107, 145mpan2 675 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  ( F `  x )  =  if ( ( x  mod  T )  < 
pi ,  1 , 
-u 1 ) )
147144, 146eqtr4d 2460 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
148 eqid 2423 . . . . . . . . . . . . . . . . 17  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  =  ( ( RR  _D  F
)  |`  ( -u pi (,) pi ) )
149 snfi 7599 . . . . . . . . . . . . . . . . . 18  |-  { 0 }  e.  Fin
150 eldifi 3525 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  e.  ( -u pi (,) pi ) )
151 0xr 9633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  RR*
152151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  -> 
0  e.  RR* )
153118rexri 9639 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  pi  e.  RR*
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  pi  e.  RR* )
155 elioore 11612 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  RR )
156155adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  RR )
157 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  -> 
0  <  x )
158118renegcli 9881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  -u pi  e.  RR
159158rexri 9639 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  -u pi  e.  RR*
160 iooltub 37502 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( -u pi (,) pi ) )  ->  x  <  pi )
161159, 153, 160mp3an12 1350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( -u pi (,) pi )  ->  x  <  pi )
162161adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  <  pi )
163152, 154, 156, 157, 162eliood 37487 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  ( 0 (,) pi ) )
164 negpilt0 37387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  -u pi  <  0
165158, 67, 164ltleii 9703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  -u pi  <_  0
166 iooss1 11617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
-u pi  e.  RR*  /\  -u pi  <_  0 )  ->  ( 0 (,) pi )  C_  ( -u pi (,) pi ) )
167159, 165, 166mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0 (,) pi )  C_  ( -u pi (,) pi )
168167sseli 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( -u pi (,) pi ) )
169104reseq1i 5058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( F  |`  ( 0 (,) pi ) )  =  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )  |`  (
0 (,) pi ) )
170 ioossre 11642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0 (,) pi )  C_  RR
171 resmpt 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 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
) ) )
172170, 171ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( 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
) )
173 elioore 11612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  RR )
174133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( 0 (,) pi )  ->  T  e.  RR+ )
175 0red 9590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  0  e.  RR )
176 ioogtlb 37484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( 0 (,) pi ) )  ->  0  <  x )
177151, 153, 176mp3an12 1350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  0  <  x )
178175, 173, 177ltled 9729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( 0 (,) pi )  ->  0  <_  x )
179118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  pi  e.  RR )
180120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  T  e.  RR )
181168, 161syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  x  <  pi )
182 pirp 23353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  pi  e.  RR+
183 2timesgt 37398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( pi  e.  RR+  ->  pi  <  ( 2  x.  pi ) )
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  pi  <  ( 2  x.  pi )
185184, 131breqtri 4385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  pi  <  T
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  pi  <  T )
187173, 179, 180, 181, 186lttrd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( 0 (,) pi )  ->  x  <  T )
188 modid 12066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( x  e.  RR  /\  T  e.  RR+ )  /\  ( 0  <_  x  /\  x  <  T ) )  ->  ( x  mod  T )  =  x )
189173, 174, 178, 187, 188syl22anc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( 0 (,) pi )  ->  (
x  mod  T )  =  x )
190189, 181eqbrtrd 4382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( 0 (,) pi )  ->  (
x  mod  T )  <  pi )
191190iftrued 3857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( 0 (,) pi )  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  1 )
192191mpteq2ia 4444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( 0 (,) pi )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( x  e.  ( 0 (,) pi )  |->  1 )
193169, 172, 1923eqtrri 2450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  e.  ( 0 (,) pi )  |->  1 )  =  ( F  |`  ( 0 (,) pi ) )
194193oveq2i 6255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( RR 
_D  ( x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( RR  _D  ( F  |`  ( 0 (,) pi ) ) )
195 reelprrecn 9577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  RR  e.  { RR ,  CC }
196195a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  RR  e.  { RR ,  CC } )
197 iooretop 21723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0 (,) pi )  e.  ( topGen `  ran  (,) )
198 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
199198tgioo2 21758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
200197, 199eleqtri 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0 (,) pi )  e.  ( ( TopOpen ` fld )t  RR )
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  ( 0 (,) pi )  e.  ( ( TopOpen
` fld
)t 
RR ) )
202 1cnd 9605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  1  e.  CC )
203196, 201, 202dvmptconst 37668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  ( RR  _D  (
x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( x  e.  ( 0 (,) pi )  |->  0 ) )
204203trud 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( RR 
_D  ( x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( x  e.  ( 0 (,) pi )  |->  0 )
205 ssid 3421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  RR  C_  RR
206 ax-resscn 9542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  RR  C_  CC
207 fss 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( F : RR --> RR  /\  RR  C_  CC )  ->  F : RR --> CC )
208109, 206, 207mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F : RR
--> CC
209 dvresioo 37676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( RR  C_  RR  /\  F : RR --> CC )  -> 
( RR  _D  ( F  |`  ( 0 (,) pi ) ) )  =  ( ( RR 
_D  F )  |`  ( 0 (,) pi ) ) )
210205, 208, 209mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( RR 
_D  ( F  |`  ( 0 (,) pi ) ) )  =  ( ( RR  _D  F )  |`  (
0 (,) pi ) )
211194, 204, 2103eqtr3i 2453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( 0 (,) pi )  |->  0 )  =  ( ( RR 
_D  F )  |`  ( 0 (,) pi ) )
212211dmeqi 4993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  dom  (
x  e.  ( 0 (,) pi )  |->  0 )  =  dom  (
( RR  _D  F
)  |`  ( 0 (,) pi ) )
213 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( 0 (,) pi )  |->  0 )  =  ( x  e.  ( 0 (,) pi )  |->  0 )
21489, 213dmmpti 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  dom  (
x  e.  ( 0 (,) pi )  |->  0 )  =  ( 0 (,) pi )
215212, 214eqtr3i 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  dom  (
( RR  _D  F
)  |`  ( 0 (,) pi ) )  =  ( 0 (,) pi )
216 ssdmres 5083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 0 (,) pi ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( 0 (,) pi ) )  =  ( 0 (,) pi ) )
217215, 216mpbir 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0 (,) pi )  C_  dom  ( RR  _D  F
)
218217sseli 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  dom  ( RR  _D  F ) )
219168, 218elind 3588 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) ) )
220 dmres 5082 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  =  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) )
221219, 220syl6eleqr 2512 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
222163, 221syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
223222adantlr 719 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  0  <  x )  ->  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
224159a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -u pi  e.  RR* )
225151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  -> 
0  e.  RR* )
226155ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  RR )
227 ioogtlb 37484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( -u pi (,) pi ) )  ->  -u pi  <  x )
228159, 153, 227mp3an12 1350 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) pi )  ->  -u pi  <  x )
229228ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -u pi  <  x )
230 0red 9590 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  -> 
0  e.  RR )
231 neqne 37290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  x  =  0  ->  x  =/=  0 )
232231ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  =/=  0 )
233 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -.  0  <  x )
234226, 230, 232, 233lttri5d 37414 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  <  0 )
235224, 225, 226, 229, 234eliood 37487 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  ( -u pi (,) 0 ) )
23667, 118, 68ltleii 9703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  <_  pi
237 iooss2 11618 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( pi  e.  RR*  /\  0  <_  pi )  ->  ( -u pi (,) 0 ) 
C_  ( -u pi (,) pi ) )
238153, 236, 237mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  ( -u pi (,) pi )
239238sseli 3398 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( -u pi (,) pi ) )
240104reseq1i 5058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( F  |`  ( -u pi (,) 0 ) )  =  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi ,  1 ,  -u 1 ) )  |`  ( -u pi (,) 0 ) )
241 ioossre 11642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -u pi (,) 0 )  C_  RR
242 resmpt 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
-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
) ) )
243241, 242ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 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
) )
244118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  e.  RR )
245 elioore 11612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  RR )
246133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  RR+ )
247245, 246modcld 12047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  mod  T )  e.  RR )
248245, 143syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  e.  RR )
249522timesi 10676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( 2  x.  pi )  =  ( pi  +  pi )
250110, 249eqtri 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  T  =  ( pi  +  pi )
251250oveq2i 6255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -u pi  +  T )  =  ( -u pi  +  ( pi  +  pi ) )
252 negpicn 23354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  -u pi  e.  CC
253252, 52, 52addassi 9597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
-u pi  +  pi )  +  pi )  =  ( -u pi  +  ( pi  +  pi ) )
254253eqcomi 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -u pi  +  ( pi  +  pi ) )  =  ( ( -u pi  +  pi )  +  pi )
25552negidi 9889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( pi  +  -u pi )  =  0
25652, 252, 255addcomli 9771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( -u pi  +  pi )  =  0
257256oveq1i 6254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
-u pi  +  pi )  +  pi )  =  ( 0  +  pi )
25852addid2i 9767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 0  +  pi )  =  pi
259257, 258eqtri 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
-u pi  +  pi )  +  pi )  =  pi
260251, 254, 2593eqtrri 2450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  pi  =  ( -u pi  +  T
)
261260a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  =  ( -u pi  +  T ) )
262158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  -u pi  e.  RR )
263120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  RR )
264239, 228syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  -u pi  <  x )
265262, 245, 263, 264ltadd1dd 10170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( -u pi  +  T )  <  ( x  +  T ) )
266261, 265eqbrtrd 4382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <  ( x  +  T
) )
267244, 248, 266ltled 9729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <_  ( x  +  T
) )
268 0red 9590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  e.  RR )
269158, 120readdcli 9602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( -u pi  +  T )  e.  RR
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( -u pi  +  T )  e.  RR )
27168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  pi )
272271, 260syl6breq 4401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  ( -u pi  +  T ) )
273268, 270, 248, 272, 265lttrd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  ( x  +  T
) )
274268, 248, 273ltled 9729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <_  ( x  +  T
) )
275245recnd 9615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  CC )
276121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  CC )
277275, 276addcomd 9781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( T  +  x ) )
278 iooltub 37502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  x  e.  ( -u pi (,) 0 ) )  ->  x  <  0 )
279159, 151, 278mp3an12 1350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  <  0 )
280 ltaddneg 37405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( x  e.  RR  /\  T  e.  RR )  ->  ( x  <  0  <->  ( T  +  x )  <  T ) )
281245, 120, 280sylancl 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  <  0  <->  ( T  +  x )  <  T
) )
282279, 281mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( T  +  x )  <  T )
283277, 282eqbrtrd 4382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  <  T )
284274, 283jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
0  <_  ( x  +  T )  /\  (
x  +  T )  <  T ) )
285 modid2 12069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( x  +  T
)  e.  RR  /\  T  e.  RR+ )  -> 
( ( ( x  +  T )  mod 
T )  =  ( x  +  T )  <-> 
( 0  <_  (
x  +  T )  /\  ( x  +  T )  <  T
) ) )
286248, 133, 285sylancl 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( ( x  +  T )  mod  T
)  =  ( x  +  T )  <->  ( 0  <_  ( x  +  T )  /\  (
x  +  T )  <  T ) ) )
287284, 286mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( x  +  T
)  mod  T )  =  ( x  +  T ) )
288125a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  RR  ->  (
( x  +  T
)  mod  T )  =  ( ( x  +  ( 1  x.  T ) )  mod 
T ) )
289133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  RR  ->  T  e.  RR+ )
290 1zzd 10914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  RR  ->  1  e.  ZZ )
291141, 289, 290, 136syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  RR  ->  (
( x  +  ( 1  x.  T ) )  mod  T )  =  ( x  mod  T ) )
292288, 291eqtrd 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  RR  ->  (
( x  +  T
)  mod  T )  =  ( x  mod  T ) )
293245, 292syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( x  +  T
)  mod  T )  =  ( x  mod  T ) )
294287, 293eqtr3d 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( x  mod  T ) )
295267, 294breqtrd 4386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <_  ( x  mod  T
) )
296244, 247, 295lensymd 9732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -u pi (,) 0 )  ->  -.  ( x  mod  T )  <  pi )
297296iffalsed 3860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( -u pi (,) 0 )  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  -u 1
)
298297mpteq2ia 4444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  e.  ( -u pi (,) 0 )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( x  e.  ( -u pi (,) 0 )  |->  -u
1 )
299240, 243, 2983eqtrri 2450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( F  |`  ( -u pi (,) 0 ) )
300299oveq2i 6255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( RR 
_D  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
) )  =  ( RR  _D  ( F  |`  ( -u pi (,) 0 ) ) )
301 iooretop 21723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -u pi (,) 0 )  e.  ( topGen `  ran  (,) )
302301, 199eleqtri 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -u pi (,) 0 )  e.  ( ( TopOpen ` fld )t  RR )
303302a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  ( -u pi (,) 0 )  e.  ( ( TopOpen ` fld )t  RR ) )
304202negcld 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  -u 1  e.  CC )
305196, 303, 304dvmptconst 37668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  ( RR  _D  (
x  e.  ( -u pi (,) 0 )  |->  -u
1 ) )  =  ( x  e.  (
-u pi (,) 0
)  |->  0 ) )
306305trud 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( RR 
_D  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
) )  =  ( x  e.  ( -u pi (,) 0 )  |->  0 )
307 dvresioo 37676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( RR  C_  RR  /\  F : RR --> CC )  -> 
( RR  _D  ( F  |`  ( -u pi (,) 0 ) ) )  =  ( ( RR 
_D  F )  |`  ( -u pi (,) 0
) ) )
308205, 208, 307mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( RR 
_D  ( F  |`  ( -u pi (,) 0
) ) )  =  ( ( RR  _D  F )  |`  ( -u pi (,) 0 ) )
309300, 306, 3083eqtr3i 2453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( ( RR 
_D  F )  |`  ( -u pi (,) 0
) )
310309dmeqi 4993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  dom  (
x  e.  ( -u pi (,) 0 )  |->  0 )  =  dom  (
( RR  _D  F
)  |`  ( -u pi (,) 0 ) )
311 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( x  e.  ( -u pi (,) 0 )  |->  0 )
31289, 311dmmpti 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  dom  (
x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( -u pi (,) 0 )
313310, 312eqtr3i 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 )
314 ssdmres 5083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
-u pi (,) 0
)  C_  dom  ( RR 
_D  F )  <->  dom  ( ( RR  _D  F )  |`  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 ) )
315313, 314mpbir 212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  dom  ( RR  _D  F
)
316315sseli 3398 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  dom  ( RR  _D  F ) )
317239, 316elind 3588 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) ) )
318317, 220syl6eleqr 2512 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
319235, 318syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
320223, 319pm2.61dan 798 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  ( -u pi (,) pi )  /\  -.  x  =  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
321150, 320sylan 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  /\  -.  x  =  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
322 eldifn 3526 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  -.  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
323322adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  /\  -.  x  =  0
)  ->  -.  x  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
324321, 323condan 801 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  =  0 )
325 elsn 3950 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  { 0 }  <-> 
x  =  0 )
326324, 325sylibr 215 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  e.  { 0 } )
327326ssriv 3406 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  C_  { 0 }
328 ssfi 7740 . . . . . . . . . . . . . . . . . 18  |-  ( ( { 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 )
329149, 327, 328mp2an 676 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  e. 
Fin
330 inss1 3620 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
-u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  C_  ( -u pi (,) pi )
331220, 330eqsstri 3432 . . . . . . . . . . . . . . . . . . . . 21  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  ( -u pi (,) pi )
332 ioosscn 37483 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u pi (,) pi )  C_  CC
333331, 332sstri 3411 . . . . . . . . . . . . . . . . . . . 20  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  CC
334333a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  C_  CC )
335 dvf 22799 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
336 fresin 5707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  _D  F ) : dom  ( RR 
_D  F ) --> CC 
->  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : ( dom  ( RR  _D  F
)  i^i  ( -u pi (,) pi ) ) --> CC )
337 ffdm 5698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) ) )
338335, 336, 337mp2b 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) )
339338simpli 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) --> CC
340339a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) : dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) ) --> CC )
341159a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  -u pi  e.  RR* )
342151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  -> 
0  e.  RR* )
343 ioossre 11642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) pi )  C_  RR
344331sseli 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  ( -u pi (,) pi ) )
345343, 344sseldi 3400 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  RR )
346345adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  e.  RR )
347344, 228syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  -u pi  <  x )
348347adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  -u pi  <  x )
349 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  <  0 )
350341, 342, 346, 348, 349eliood 37487 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  e.  ( -u pi (,) 0 ) )
351 elun1 3571 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( ( -u pi (,) 0 )  u.  (
0 (,) pi ) ) )
352350, 351syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  e.  ( ( -u pi (,) 0 )  u.  ( 0 (,) pi ) ) )
353 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
354 0red 9590 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  0  e.  RR )
355345adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  RR )
356 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  -.  x  <  0 )
357354, 355, 356nltled 9731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  0  <_  x )
358 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  0  ->  x  =  0 )
359205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  RR  C_  RR )
360 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
361208a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  F : RR --> CC )
362 0red 9590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  0  e.  RR )
363 mnfxr 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |- -oo  e.  RR*
364363a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
-> -oo  e.  RR* )
365362mnfltd 11372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
-> -oo  <  0 )
366360, 364, 362, 365lptioo2 37594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( -oo (,) 0 ) ) )
367 incom 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( RR 
i^i  ( -oo (,) 0 ) )  =  ( ( -oo (,) 0 )  i^i  RR )
368 ioossre 11642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( -oo (,) 0 )  C_  RR
369 df-ss 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( -oo (,) 0 ) 
C_  RR  <->  ( ( -oo (,) 0 )  i^i  RR )  =  ( -oo (,) 0 ) )
370368, 369mpbi 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( -oo (,) 0 )  i^i  RR )  =  ( -oo (,) 0
)
371367, 370eqtr2i 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -oo (,) 0 )  =  ( RR  i^i  ( -oo (,) 0 ) )
372371fveq2i 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
limPt `  ( topGen `  ran  (,) ) ) `  ( -oo (,) 0 ) )  =  ( ( limPt `  ( topGen `  ran  (,) )
) `  ( RR  i^i  ( -oo (,) 0
) ) )
373366, 372syl6eleq 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( RR  i^i  ( -oo (,) 0 ) ) ) )
374 pnfxr 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |- +oo  e.  RR*
375374a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
-> +oo  e.  RR* )
376362ltpnfd 11369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  0  < +oo )
377360, 362, 375, 376lptioo1 37595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( 0 (,) +oo ) ) )
378 incom 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( RR 
i^i  ( 0 (,) +oo ) )  =  ( ( 0 (,) +oo )  i^i  RR )
379 ioossre 11642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0 (,) +oo )  C_  RR
380 df-ss 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 0 (,) +oo )  C_  RR  <->  ( ( 0 (,) +oo )  i^i 
RR )  =  ( 0 (,) +oo )
)
381379, 380mpbi 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 0 (,) +oo )  i^i  RR )  =  ( 0 (,) +oo )
382378, 381eqtr2i 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0 (,) +oo )  =  ( RR  i^i  (
0 (,) +oo )
)
383382fveq2i 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
limPt `  ( topGen `  ran  (,) ) ) `  (
0 (,) +oo )
)  =  ( (
limPt `  ( topGen `  ran  (,) ) ) `  ( RR  i^i  ( 0 (,) +oo ) ) )
384377, 383syl6eleq 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( RR  i^i  (
0 (,) +oo )
) ) )
385 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)
386 mnfle 11381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( -u pi  e.  RR*  -> -oo  <_  -u pi )
387159, 386ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |- -oo  <_  -u pi
388 iooss1 11617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( -oo  e.  RR*  /\ -oo  <_ 
-u pi )  -> 
( -u pi (,) 0
)  C_  ( -oo (,) 0 ) )
389363, 387, 388mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( -u pi (,) 0 )  C_  ( -oo (,) 0 )
390389a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T. 
->  ( -u pi (,) 0 )  C_  ( -oo (,) 0 ) )
391 ioosscn 37483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -oo (,) 0 )  C_  CC
392390, 391syl6ss 3414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  ( -u pi (,) 0 )  C_  CC )
393 0cnd 9582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  0  e.  CC )
394385, 392, 304, 393constlimc 37587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  -u 1  e.  ( ( x  e.  (
-u pi (,) 0
)  |->  -u 1 ) lim CC  0 ) )
395 resabs1 5090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
-u pi (,) 0
)  C_  ( -oo (,) 0 )  ->  (
( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0 ) )  =  ( F  |`  ( -u pi (,) 0 ) ) )
396389, 395ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0
) )  =  ( F  |`  ( -u pi (,) 0 ) )
397299, 396eqtr4i 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0
) )
398397oveq1i 6254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  ( -u pi (,) 0 )  |->  -u
1 ) lim CC  0 )  =  ( ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )
399 fssres 5704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( F : RR --> CC  /\  ( -oo (,) 0 ) 
C_  RR )  -> 
( F  |`  ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC )
400208, 368, 399mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( F  |`  ( -oo (,) 0
) ) : ( -oo (,) 0 ) --> CC
401400a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  ( F  |`  ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC )
402391a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  ( -oo (,) 0
)  C_  CC )
403 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) )  =  ( ( TopOpen ` fld )t  (
( -oo (,) 0 )  u.  { 0 } ) )
404 0le0 10645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  <_  0
405 elioc2 11643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR )  ->  ( 0  e.  ( -u pi (,] 0 )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <_ 
0 ) ) )
406159, 67, 405mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 0  e.  ( -u pi (,] 0 )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <_ 
0 ) )
40767, 164, 404, 406mpbir3an 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  ( -u pi (,] 0 )
408198cnfldtop 21741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( TopOpen ` fld )  e.  Top
409 ovex 6272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -oo (,] 0 )  e.  _V
410 resttop 20113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( -oo (,] 0
)  e.  _V )  ->  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )  e.  Top )
411408, 409, 410mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
TopOpen ` fld )t  ( -oo (,] 0
) )  e.  Top
412159a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  -u pi  e.  RR* )
413 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( topGen ` 
ran  (,) )t  ( -oo (,] 0
) )
414387a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
-> -oo  <_  -u pi )
415364, 412, 362, 360, 413, 414, 362iocopn 37513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  ( -u pi (,] 0 )  e.  ( ( topGen `  ran  (,) )t  ( -oo (,] 0 ) ) )
416415trud 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -u pi (,] 0 )  e.  ( ( topGen `  ran  (,) )t  ( -oo (,] 0
) )
417199oveq1i 6254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( (
TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )
418 iocssre 11660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( -oo  e.  RR*  /\  0  e.  RR )  ->  ( -oo (,] 0 )  C_  RR )
419363, 67, 418mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( -oo (,] 0 )  C_  RR
420195elexi 3027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  RR  e.  _V
421 restabs 20118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( -oo (,] 0
)  C_  RR  /\  RR  e.  _V )  ->  (
( ( TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0
) ) )
422408, 419, 420, 421mp3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )
423417, 422eqtri 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0 ) )
424416, 423eleqtri 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( -u pi (,] 0 )  e.  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )
425 isopn3i 20035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( 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
) )
426411, 424, 425mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( int `  ( (
TopOpen ` fld )t  ( -oo (,] 0
) ) ) `  ( -u pi (,] 0
) )  =  (
-u pi (,] 0
)
427 mnflt0 11373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |- -oo  <  0
428 snunioo2 37498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( -oo  e.  RR*  /\  0  e.  RR*  /\ -oo  <  0 )  ->  (
( -oo (,) 0 )  u.  { 0 } )  =  ( -oo (,] 0 ) )
429363, 151, 427, 428mp3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( -oo (,) 0 )  u.  { 0 } )  =  ( -oo (,] 0 )
430429eqcomi 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( -oo (,] 0 )  =  ( ( -oo (,) 0
)  u.  { 0 } )
431430oveq2i 6255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
TopOpen ` fld )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) )
432431fveq2i 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( int `  ( ( TopOpen ` fld )t  ( -oo (,] 0
) ) )  =  ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) )
433 snunioo2 37498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  -u pi  <  0 )  ->  (
( -u pi (,) 0
)  u.  { 0 } )  =  (
-u pi (,] 0
) )
434159, 151, 164, 433mp3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
-u pi (,) 0
)  u.  { 0 } )  =  (
-u pi (,] 0
)
435434eqcomi 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( -u pi (,] 0 )  =  ( ( -u pi (,) 0 )  u.  {
0 } )
436432, 435fveq12i 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( int `  ( (
TopOpen ` fld )t  ( -oo (,] 0
) ) ) `  ( -u pi (,] 0
) )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) )
437426, 436eqtr3i 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( -u pi (,] 0 )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) )
438407, 437eleqtri 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  e.  ( ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) )
439438a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  0  e.  (
( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) ) )
440401, 390, 402, 198, 403, 439limcres 22778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T. 
->  ( ( ( F  |`  ( -oo (,) 0
) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )  =  ( ( F  |`  ( -oo (,) 0
) ) lim CC  0 ) )
441440trud 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )  =  ( ( F  |`  ( -oo (,) 0 ) ) lim
CC  0 )
442398, 441eqtri 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ( -u pi (,) 0 )  |->  -u
1 ) lim CC  0 )  =  ( ( F  |`  ( -oo (,) 0 ) ) lim CC  0 )
443394, 442syl6eleq 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  -u 1  e.  ( ( F  |`  ( -oo (,) 0 ) ) lim
CC  0 ) )
444 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( 0 (,) pi )  |->  1 )  =  ( x  e.  ( 0 (,) pi )  |->  1 )
445 ioosscn 37483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0 (,) pi )  C_  CC
446445a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  ( 0 (,) pi )  C_  CC )
447444, 446, 202, 393constlimc 37587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  1  e.  (
( x  e.  ( 0 (,) pi ) 
|->  1 ) lim CC  0 ) )
448 ltpnf 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( pi  e.  RR  ->  pi  < +oo )
449 xrltle 11394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( pi  e.  RR*  /\ +oo  e.  RR* )  ->  (
pi  < +oo  ->  pi  <_ +oo ) )
450153, 374, 449mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( pi 
< +oo  ->  pi  <_ +oo )
451118, 448, 450mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  pi  <_ +oo
452 iooss2 11618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( +oo  e.  RR*  /\  pi  <_ +oo )  ->  (
0 (,) pi ) 
C_  ( 0 (,) +oo ) )
453374, 451, 452mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 0 (,) pi )  C_  ( 0 (,) +oo )
454 resabs1 5090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 0 (,) pi ) 
C_  ( 0 (,) +oo )  ->  ( ( F  |`  ( 0 (,) +oo ) )  |`  ( 0 (,) pi ) )  =  ( F  |`  ( 0 (,) pi ) ) )
455453, 454ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( F  |`  ( 0 (,) +oo ) )  |`  ( 0 (,) pi ) )  =  ( F  |`  ( 0 (,) pi ) )
456193, 455eqtr4i 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( 0 (,) pi )  |->  1 )  =  ( ( F  |`  ( 0 (,) +oo ) )  |`  (
0 (,) pi ) )
457456oveq1i 6254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  ( 0 (,) pi )  |->  1 ) lim CC  0 )  =  ( ( ( F  |`  ( 0 (,) +oo ) )  |`  ( 0 (,) pi ) ) lim CC  0
)
458 fssres 5704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( F : RR --> CC  /\  ( 0 (,) +oo )  C_  RR )  -> 
( F  |`  (
0 (,) +oo )
) : ( 0 (,) +oo ) --> CC )
459208, 379, 458mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( F  |`  ( 0 (,) +oo ) ) : ( 0 (,) +oo ) --> CC
460459a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  ( F  |`  (
0 (,) +oo )
) : ( 0 (,) +oo ) --> CC )
461453a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  ( 0 (,) pi )  C_  ( 0 (,) +oo ) )
462 ioosscn 37483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 0 (,) +oo )  C_  CC
463462a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  ( 0 (,) +oo )  C_  CC )
464 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
TopOpen ` fld )t  ( ( 0 (,) +oo )  u.  { 0 } ) )  =  ( ( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) )
465 elico2 11644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( 0  e.  RR  /\  pi  e.  RR* )  ->  (
0  e.  ( 0 [,) pi )  <->  ( 0  e.  RR  /\  0  <_  0  /\  0  < 
pi ) ) )
46667, 153, 465mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 0  e.  ( 0 [,) pi )  <->  ( 0  e.  RR  /\  0  <_  0  /\  0  < 
pi ) )
46767, 404, 68, 466mpbir3an 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  ( 0 [,) pi )
468 ovex 6272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 0 [,) +oo )  e. 
_V
469 resttop 20113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( 0 [,) +oo )  e.  _V )  ->  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) )  e.  Top )
470408, 468, 469mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) )  e.  Top
471153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  pi  e.  RR* )
472 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)  =  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)
473451a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  pi  <_ +oo )
474362, 471, 375, 360, 472, 473icoopn 37518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  ( 0 [,) pi )  e.  ( ( topGen `
 ran  (,) )t  (
0 [,) +oo )
) )
475474trud 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 0 [,) pi )  e.  ( ( topGen `  ran  (,) )t  ( 0 [,) +oo ) )
476199oveq1i 6254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)  =  ( ( ( TopOpen ` fld )t  RR )t  ( 0 [,) +oo ) )
477 rge0ssre 11686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( 0 [,) +oo )  C_  RR
478 restabs 20118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( 0 [,) +oo )  C_  RR  /\  RR  e.  _V )  ->  (
( ( TopOpen ` fld )t  RR )t  ( 0 [,) +oo ) )  =  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) ) )
479408, 477, 420, 478mp3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( TopOpen ` fld )t  RR )t  ( 0 [,) +oo ) )  =  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) )
480476, 479eqtri 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)  =  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) )
481475, 480eleqtri 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( 0 [,) pi )  e.  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) )
482 isopn3i 20035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( TopOpen ` fld )t  ( 0 [,) +oo ) )  e.  Top  /\  ( 0 [,) pi )  e.  ( ( TopOpen
` fld
)t  ( 0 [,) +oo ) ) )  -> 
( ( int `  (
( TopOpen ` fld )t  ( 0 [,) +oo ) ) ) `  ( 0 [,) pi ) )  =  ( 0 [,) pi ) )
483470, 481, 482mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( int `  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) ) ) `  ( 0 [,) pi ) )  =  ( 0 [,) pi )
484 0ltpnf 11370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  0  < +oo
485 snunioo1 37505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  < +oo )  ->  ( ( 0 (,) +oo )  u.  { 0 } )  =  ( 0 [,) +oo ) )
486151, 374, 484, 485mp3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( 0 (,) +oo )  u.  { 0 } )  =  ( 0 [,) +oo )
487486eqcomi 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 0 [,) +oo )  =  ( ( 0 (,) +oo )  u.  { 0 } )
488487oveq2i 6255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) )  =  ( ( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) )
489488fveq2i 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( int `  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) ) )  =  ( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) )
490 snunioo1 37505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  0  < 
pi )  ->  (
( 0 (,) pi )  u.  { 0 } )  =  ( 0 [,) pi ) )
491151, 153, 68, 490mp3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( 0 (,) pi )  u.  { 0 } )  =  ( 0 [,) pi )
492491eqcomi 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( 0 [,) pi )  =  ( ( 0 (,) pi )  u.  {
0 } )
493489, 492fveq12i 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( int `  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) ) ) `  ( 0 [,) pi ) )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) ) `  (
( 0 (,) pi )  u.  { 0 } ) )
494483, 493eqtr3i 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 0 [,) pi )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) ) `  (
( 0 (,) pi )  u.  { 0 } ) )
495467, 494eleqtri 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  e.  ( ( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) ) `  (
( 0 (,) pi )  u.  { 0 } ) )
496495a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  0  e.  (
( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) ) `  (
( 0 (,) pi )  u.  { 0 } ) ) )
497460, 461, 463, 198, 464, 496limcres 22778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T. 
->  ( ( ( F  |`  ( 0 (,) +oo ) )  |`  (
0 (,) pi ) ) lim CC  0 )  =  ( ( F  |`  ( 0 (,) +oo ) ) lim CC  0
) )
498497trud 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F  |`  (
0 (,) +oo )
)  |`  ( 0 (,) pi ) ) lim CC  0 )  =  ( ( F  |`  (
0 (,) +oo )
) lim CC  0 )
499457, 498eqtri 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ( 0 (,) pi )  |->  1 ) lim CC  0 )  =  ( ( F  |`  ( 0 (,) +oo ) ) lim CC  0
)
500447, 499syl6eleq 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  1  e.  (
( F  |`  (
0 (,) +oo )
) lim CC  0 ) )
501 neg1lt0 10662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  -u 1  <  0
502106, 67, 105lttri 9706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
-u 1  <  0  /\  0  <  1
)  ->  -u 1  <  1 )
503501, 34, 502mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -u 1  <  1
504106, 503ltneii 9693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  -u 1  =/=  1
505504a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  -u 1  =/=  1
)
506198, 359, 360, 361, 362, 373, 384, 443, 500, 505jumpncnp 37659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( T. 
->  -.  F  e.  ( ( ( topGen `  ran  (,) )  CnP  ( TopOpen ` fld )
) `  0 )
)
507506trud 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  -.  F  e.  ( ( ( topGen ` 
ran  (,) )  CnP  ( TopOpen
` fld
) ) `  0
)
508206a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  RR  C_  CC )
509208a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  F : RR --> CC )
510205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  RR  C_  RR )
511 inss2 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
-u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  C_  dom  ( RR  _D  F
)
512220, 511eqsstri 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  dom  ( RR  _D  F
)
513512sseli 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  0  e.  dom  ( RR  _D  F ) )
514199, 198dvcnp2 22811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( RR  C_  CC  /\  F : RR --> CC  /\  RR  C_  RR )  /\  0  e.  dom  ( RR 
_D  F ) )  ->  F  e.  ( ( ( topGen `  ran  (,) )  CnP  ( TopOpen ` fld )
) `  0 )
)
515508, 509, 510, 513, 514syl31anc 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  F  e.  ( ( ( topGen ` 
ran  (,) )  CnP  ( TopOpen
` fld
) ) `  0
) )
516507, 515mto 179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  -.  0  e.  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )
517516a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  0  ->  -.  0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
518358, 517eqneltrd 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  0  ->  -.  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
519518necon2ai 2625 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  =/=  0 )
520519adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  =/=  0 )
521354, 355, 357, 520leneltd 9735 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  0  <  x )
522344, 163sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  0  <  x )  ->  x  e.  ( 0 (,) pi ) )
523 elun2 3572 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( ( -u pi (,) 0 )  u.  (
0 (,) pi ) ) )
524522, 523syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  0  <  x )  ->  x  e.  ( ( -u pi (,) 0 )  u.  ( 0 (,) pi ) ) )
525353, 521, 524syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  ( ( -u pi (,) 0 )  u.  (
0 (,) pi ) ) )
526352, 525pm2.61dan 798 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  ( ( -u pi (,) 0 )  u.  (
0 (,) pi ) ) )
527 ovex 6272 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -u pi (,) 0 )  e. 
_V
528 ovex 6272 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0 (,) pi )  e. 
_V
529527, 528unipr 4170 . . . . . . . . . . . . . . . . . . . . . 22  |-  U. {
( -u pi (,) 0
) ,  ( 0 (,) pi ) }  =  ( ( -u pi (,) 0 )  u.  ( 0 (,) pi ) )
530526, 529syl6eleqr 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  U. { ( -u pi (,) 0 ) ,  ( 0 (,) pi ) } )
531530ssriv 3406 . . . . . . . . . . . . . . . . . . . 20  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  U. { ( -u pi (,) 0 ) ,  ( 0 (,) pi ) }
532531a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  C_  U. {
( -u pi (,) 0
) ,  ( 0 (,) pi ) } )
533 ineq2 3596 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( -u pi (,) 0 )  ->  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  x )  =  ( dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) ) )
534 retop 21719 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( topGen ` 
ran  (,) )  e.  Top
535 ovex 6272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( RR 
_D  F )  e. 
_V
536535resex 5105 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  e.  _V
537536dmex 6679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  e. 
_V
538534, 537pm3.2i 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
topGen `  ran  (,) )  e.  Top  /\  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  e. 
_V )
539318ssriv 3406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )
540 ssid 3421 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  ( -u pi (,) 0
)
541301, 539, 5403pm3.2i 1183 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
-u pi (,) 0
)  e.  ( topGen ` 
ran  (,) )  /\  ( -u pi (,) 0 ) 
C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  /\  ( -u pi (,) 0 ) 
C_  ( -u pi (,) 0 ) )
542 restopnb 20128 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( topGen `  ran  (,) )  e.  Top  /\  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  e.  _V )  /\  ( ( -u pi (,) 0 )  e.  (
topGen `  ran  (,) )  /\  ( -u pi (,) 0 )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  /\  ( -u pi (,) 0 )  C_  ( -u pi (,) 0
) ) )  -> 
( ( -u pi (,) 0 )  e.  (
topGen `  ran  (,) )  <->  (
-u pi (,) 0
)  e.  ( (
topGen `  ran  (,) )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) ) )
543538, 541, 542mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
-u pi (,) 0
)  e.  ( topGen ` 
ran  (,) )  <->  ( -u pi (,) 0 )  e.  ( ( topGen `  ran  (,) )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) )
544301, 543mpbi 211 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -u pi (,) 0 )  e.  ( ( topGen `  ran  (,) )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
545 inss2 3621 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) ) 
C_  ( -u pi (,) 0 )
546539, 540ssini 3623 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -u pi (,) 0 )  C_  ( dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) )
547545, 546eqssi 3418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 )
548199oveq1i 6254 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
topGen `  ran  (,) )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  =  ( ( ( TopOpen ` fld )t  RR )t  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
549331, 343sstri 3411 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  RR
550 restabs 20118 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( TopOpen ` fld )  e.  Top  /\ 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  C_  RR  /\  RR  e.  _V )  ->  ( ( ( TopOpen ` fld )t  RR )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  =  ( ( TopOpen ` fld )t  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) ) )
551408, 549, 420, 550mp3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( TopOpen ` fld )t  RR )t  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )  =  ( ( TopOpen ` fld )t  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
552548, 551eqtr2i 2446 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
TopOpen ` fld )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )  =  ( ( topGen `  ran  (,) )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
553544, 547, 5523eltr4i 2514 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) )  e.  ( ( TopOpen ` fld )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
554533, 553syl6eqel 2509 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( -u pi (,) 0 )  ->  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  x )  e.  ( ( TopOpen ` fld )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) )
555554adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  { (
-u pi (,) 0
) ,  ( 0 (,) pi ) }  /\  x  =  (
-u pi (,) 0
) )  ->  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  x )  e.  ( ( TopOpen ` fld )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) )
556 neqne 37290 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  x  =  ( -u pi (,) 0 )  ->  x  =/=  ( -u pi (,) 0 ) )
557 elprn1 37596 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  { (
-u pi (,) 0
) ,  ( 0 (,) pi ) }  /\  x  =/=  ( -u pi (,) 0 ) )  ->  x  =  ( 0 (,) pi ) )
558556, 557sylan2 476 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  { (
-u pi (,) 0
) ,  ( 0 (,) pi ) }  /\  -.  x  =  ( -u pi (,) 0 ) )  ->  x  =  ( 0 (,) pi ) )
559 ineq2 3596 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( 0 (,) pi )  ->  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  x )  =  ( dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  i^i  ( 0 (,) pi ) ) )
560221ssriv 3406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 0 (,) pi )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )
561 ssid 3421 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 0 (,) pi )  C_  ( 0 (,) pi )
562197, 560, 5613pm3.2i 1183 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 0 (,) pi )  e.  ( topGen `  ran  (,) )  /\  ( 0 (,) pi )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  /\  ( 0 (,) pi )  C_  ( 0 (,) pi ) )
563 restopnb 20128 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( topGen `  ran  (,) )  e.  Top  /\  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  e.  _V )  /\  ( ( 0 (,) pi )  e.  (
topGen `  ran  (,) )  /\  ( 0 (,) pi )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  /\  (
0 (,) pi ) 
C_  ( 0 (,) pi ) ) )  ->  ( ( 0 (,) pi )  e.  ( topGen `  ran  (,) )  <->  ( 0 (,) pi )  e.  ( ( topGen ` 
ran  (,) )t  dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) ) ) )
564538, 562, 563mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 0 (,) pi )  e.  ( topGen `  ran  (,) )  <->  ( 0 (,) pi )  e.  ( ( topGen `  ran  (,) )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) )
565197, 564mpbi 211 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0 (,) pi )  e.  ( ( topGen `  ran  (,) )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
566 inss2 3621 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( 0 (,) pi ) ) 
C_  ( 0 (,) pi )
567560, 561ssini 3623 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0 (,) pi )  C_  ( dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  i^i  (
0 (,) pi ) )
568566, 567eqssi 3418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( 0 (,) pi ) )  =  ( 0 (,) pi )
569565, 568, 5523eltr4i 2514 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( 0 (,) pi ) )  e.  ( ( TopOpen ` fld )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
570559, 569syl6eqel 2509 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( 0 (,) pi )