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

Theorem fouriersw 38132
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 11222 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
2 1zzd 10996 . . . . . . 7  |-  ( T. 
->  1  e.  ZZ )
3 eqidd 2462 . . . . . . . . 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 6322 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  (
2  x.  n )  =  ( 2  x.  k ) )
54oveq1d 6329 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
( 2  x.  n
)  -  1 )  =  ( ( 2  x.  k )  - 
1 ) )
65oveq1d 6329 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( ( 2  x.  n )  -  1 )  x.  X )  =  ( ( ( 2  x.  k )  -  1 )  x.  X ) )
76fveq2d 5891 . . . . . . . . . . 11  |-  ( n  =  k  ->  ( sin `  ( ( ( 2  x.  n )  -  1 )  x.  X ) )  =  ( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) ) )
87, 5oveq12d 6332 . . . . . . . . . 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 472 . . . . . . . . 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 6342 . . . . . . . . . 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 5976 . . . . . . . 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 472 . . . . . . 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 10997 . . . . . . . . . . . . . . 15  |-  2  e.  ZZ
1615a1i 11 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  2  e.  ZZ )
17 nnz 10987 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  k  e.  ZZ )
1816, 17zmulcld 11074 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  ZZ )
19 1zzd 10996 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  e.  ZZ )
2018, 19zsubcld 11073 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  ZZ )
2120zcnd 11069 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  CC )
22 fouriersw.x . . . . . . . . . . . . 13  |-  X  e.  RR
2322recni 9680 . . . . . . . . . . . 12  |-  X  e.  CC
2423a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  X  e.  CC )
2521, 24mulcld 9688 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  -  1 )  x.  X )  e.  CC )
2625sincld 14232 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( sin `  ( ( ( 2  x.  k )  -  1 )  x.  X ) )  e.  CC )
27 0red 9669 . . . . . . . . . 10  |-  ( k  e.  NN  ->  0  e.  RR )
28 2re 10706 . . . . . . . . . . . . . 14  |-  2  e.  RR
2928a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  2  e.  RR )
30 1red 9683 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  e.  RR )
3129, 30remulcld 9696 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  1 )  e.  RR )
3231, 30resubcld 10074 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  1 )  -  1 )  e.  RR )
3320zred 11068 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  RR )
34 0lt1 10163 . . . . . . . . . . . . 13  |-  0  <  1
35 2t1e2 10786 . . . . . . . . . . . . . . 15  |-  ( 2  x.  1 )  =  2
3635oveq1i 6324 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
37 2m1e1 10751 . . . . . . . . . . . . . 14  |-  ( 2  -  1 )  =  1
3836, 37eqtr2i 2484 . . . . . . . . . . . . 13  |-  1  =  ( ( 2  x.  1 )  - 
1 )
3934, 38breqtri 4439 . . . . . . . . . . . 12  |-  0  <  ( ( 2  x.  1 )  -  1 )
4039a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  0  <  ( ( 2  x.  1 )  -  1 ) )
4118zred 11068 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  RR )
42 nnre 10643 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  RR )
43 0le2 10727 . . . . . . . . . . . . . 14  |-  0  <_  2
4443a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  0  <_  2 )
45 nnge1 10662 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  1  <_  k )
4630, 42, 29, 44, 45lemul2ad 10574 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
2  x.  1 )  <_  ( 2  x.  k ) )
4731, 41, 30, 46lesub1dd 10256 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  1 )  -  1 )  <_  ( ( 2  x.  k )  - 
1 ) )
4827, 32, 33, 40, 47ltletrd 9820 . . . . . . . . . 10  |-  ( k  e.  NN  ->  0  <  ( ( 2  x.  k )  -  1 ) )
4927, 48gtned 9795 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  =/=  0 )
5026, 21, 49divcld 10410 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) )  e.  CC )
5150adantl 472 . . . . . . 7  |-  ( ( T.  /\  k  e.  NN )  ->  (
( sin `  (
( ( 2  x.  k )  -  1 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) )  e.  CC )
52 picn 23462 . . . . . . . . . . 11  |-  pi  e.  CC
5352a1i 11 . . . . . . . . . 10  |-  ( T. 
->  pi  e.  CC )
54 4cn 10714 . . . . . . . . . . 11  |-  4  e.  CC
5554a1i 11 . . . . . . . . . 10  |-  ( T. 
->  4  e.  CC )
56 4ne0 10733 . . . . . . . . . . 11  |-  4  =/=  0
5756a1i 11 . . . . . . . . . 10  |-  ( T. 
->  4  =/=  0
)
5853, 55, 57divcld 10410 . . . . . . . . 9  |-  ( T. 
->  ( pi  /  4
)  e.  CC )
59 eqid 2461 . . . . . . . . . . . . . . . 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 9661 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  0  e.  CC )
6154a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  4  e.  CC )
62 nncn 10644 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  CC )
63 mulcl 9648 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  CC  /\  pi  e.  CC )  -> 
( n  x.  pi )  e.  CC )
6462, 52, 63sylancl 673 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
n  x.  pi )  e.  CC )
6552a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  pi  e.  CC )
66 nnne0 10669 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  =/=  0 )
67 0re 9668 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
68 pipos 23463 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  pi
6967, 68gtneii 9771 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  =/=  0
7069a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  pi  =/=  0 )
7162, 65, 66, 70mulne0d 10291 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
n  x.  pi )  =/=  0 )
7261, 64, 71divcld 10410 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
4  /  ( n  x.  pi ) )  e.  CC )
7323a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  X  e.  CC )
7462, 73mulcld 9688 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
n  x.  X )  e.  CC )
7574sincld 14232 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  ( sin `  ( n  x.  X ) )  e.  CC )
7672, 75mulcld 9688 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  (
( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  CC )
7760, 76ifcld 3935 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  ->  if ( 2  ||  n ,  0 ,  ( ( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) ) )  e.  CC )
7859, 77fmpti 6067 . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . . . . 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 4419 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
2  ||  n  <->  2  ||  k ) )
82 oveq1 6321 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  k  ->  (
n  x.  pi )  =  ( k  x.  pi ) )
8382oveq2d 6330 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  (
4  /  ( n  x.  pi ) )  =  ( 4  / 
( k  x.  pi ) ) )
84 oveq1 6321 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  k  ->  (
n  x.  X )  =  ( k  x.  X ) )
8584fveq2d 5891 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  ( sin `  ( n  x.  X ) )  =  ( sin `  (
k  x.  X ) ) )
8683, 85oveq12d 6332 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
( 4  /  (
n  x.  pi ) )  x.  ( sin `  ( n  x.  X
) ) )  =  ( ( 4  / 
( k  x.  pi ) )  x.  ( sin `  ( k  x.  X ) ) ) )
8781, 86ifbieq2d 3917 . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . 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 9662 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  _V
90 ovex 6342 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) )  e.  _V
9189, 90ifex 3960 . . . . . . . . . . . . . . . . . . 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 5976 . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( k  / 
2 )  e.  NN )
96 simpl 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  k  e.  NN )
97 2nn 10795 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  NN
98 nndivdvds 14359 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  2  e.  NN )  ->  ( 2  ||  k  <->  ( k  /  2 )  e.  NN ) )
9996, 97, 98sylancl 673 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  ( 2  ||  k 
<->  ( k  /  2
)  e.  NN ) )
10095, 99mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  2  ||  k
)
101100iftrued 3900 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  ( k  /  2
)  e.  NN )  ->  if ( 2 
||  k ,  0 ,  ( ( 4  /  ( k  x.  pi ) )  x.  ( sin `  (
k  x.  X ) ) ) )  =  0 )
10294, 101eqtrd 2495 . . . . . . . . . . . . . . 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 1032 . . . . . . . . . . . . . 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 9667 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR
106105renegcli 9960 . . . . . . . . . . . . . . . . . . . 20  |-  -u 1  e.  RR
107105, 106keepel 3959 . . . . . . . . . . . . . . . . . . 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 6067 . . . . . . . . . . . . . . . . 17  |-  F : RR
--> RR
110 fouriersw.t . . . . . . . . . . . . . . . . 17  |-  T  =  ( 2  x.  pi )
111 oveq1 6321 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
x  mod  T )  =  ( y  mod 
T ) )
112111breq1d 4425 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
( x  mod  T
)  <  pi  <->  ( y  mod  T )  <  pi ) )
113112ifbid 3914 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  if ( ( y  mod  T
)  <  pi , 
1 ,  -u 1
) )
114113cbvmptv 4508 . . . . . . . . . . . . . . . . . . . . 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 2483 . . . . . . . . . . . . . . . . . . . 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 6321 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  +  T )  ->  (
y  mod  T )  =  ( ( x  +  T )  mod 
T ) )
118 pire 23461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  pi  e.  RR
11928, 118remulcli 9682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 2  x.  pi )  e.  RR
120110, 119eqeltri 2535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  T  e.  RR
121120recni 9680 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  T  e.  CC
122121mulid2i 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 1  x.  T )  =  T
123122eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  T  =  ( 1  x.  T
)
124123oveq2i 6325 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  +  T )  =  ( x  +  ( 1  x.  T ) )
125124oveq1i 6324 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  +  T )  mod  T )  =  ( ( x  +  ( 1  x.  T
) )  mod  T
)
126117, 125syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  +  T )  ->  (
y  mod  T )  =  ( ( x  +  ( 1  x.  T ) )  mod 
T ) )
127126adantl 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( y  mod  T
)  =  ( ( x  +  ( 1  x.  T ) )  mod  T ) )
128 simpl 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  x  e.  RR )
129 2pos 10728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <  2
13028, 118, 129, 68mulgt0ii 9793 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <  ( 2  x.  pi )
131110eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 2  x.  pi )  =  T
132130, 131breqtri 4439 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  <  T
133120, 132elrpii 11333 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  T  e.  RR+
134133a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  ->  T  e.  RR+ )
135 1zzd 10996 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
1  e.  ZZ )
136 modcyc 12163 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  T  e.  RR+  /\  1  e.  ZZ )  ->  (
( x  +  ( 1  x.  T ) )  mod  T )  =  ( x  mod  T ) )
137128, 134, 135, 136syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( ( x  +  ( 1  x.  T
) )  mod  T
)  =  ( x  mod  T ) )
138127, 137eqtrd 2495 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( y  mod  T
)  =  ( x  mod  T ) )
139138breq1d 4425 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  y  =  ( x  +  T ) )  -> 
( ( y  mod 
T )  <  pi  <->  ( x  mod  T )  <  pi ) )
140139ifbid 3914 . . . . . . . . . . . . . . . . . . 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 9695 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  (
x  +  T )  e.  RR )
144116, 140, 143, 108fvmptd 5976 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  ( F `  ( x  +  T ) )  =  if ( ( x  mod  T )  < 
pi ,  1 , 
-u 1 ) )
145104fvmpt2 5979 . . . . . . . . . . . . . . . . . . 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 682 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  ( F `  x )  =  if ( ( x  mod  T )  < 
pi ,  1 , 
-u 1 ) )
147144, 146eqtr4d 2498 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
148 eqid 2461 . . . . . . . . . . . . . . . . 17  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  =  ( ( RR  _D  F
)  |`  ( -u pi (,) pi ) )
149 snfi 7675 . . . . . . . . . . . . . . . . . 18  |-  { 0 }  e.  Fin
150 eldifi 3566 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  e.  ( -u pi (,) pi ) )
151 0xr 9712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  RR*
152151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  -> 
0  e.  RR* )
153118rexri 9718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  pi  e.  RR*
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  pi  e.  RR* )
155 elioore 11694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( -u pi (,) pi )  ->  x  e.  RR )
156155adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  RR )
157 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  -> 
0  <  x )
158118renegcli 9960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  -u pi  e.  RR
159158rexri 9718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  -u pi  e.  RR*
160 iooltub 37647 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( -u pi (,) pi ) )  ->  x  <  pi )
161159, 153, 160mp3an12 1363 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( -u pi (,) pi )  ->  x  <  pi )
162161adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  <  pi )
163152, 154, 156, 157, 162eliood 37632 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( -u pi (,) pi )  /\  0  <  x )  ->  x  e.  ( 0 (,) pi ) )
164 negpilt0 37527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  -u pi  <  0
165158, 67, 164ltleii 9782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  -u pi  <_  0
166 iooss1 11699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
-u pi  e.  RR*  /\  -u pi  <_  0 )  ->  ( 0 (,) pi )  C_  ( -u pi (,) pi ) )
167159, 165, 166mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0 (,) pi )  C_  ( -u pi (,) pi )
168167sseli 3439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( -u pi (,) pi ) )
169104reseq1i 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( F  |`  ( 0 (,) pi ) )  =  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )  |`  (
0 (,) pi ) )
170 ioossre 11724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0 (,) pi )  C_  RR
171 resmpt 5172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  RR )
174133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( 0 (,) pi )  ->  T  e.  RR+ )
175 0red 9669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  0  e.  RR )
176 ioogtlb 37629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( 0 (,) pi ) )  ->  0  <  x )
177151, 153, 176mp3an12 1363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  0  <  x )
178175, 173, 177ltled 9808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  pi  e.  RR+
183 2timesgt 37538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( pi  e.  RR+  ->  pi  <  ( 2  x.  pi ) )
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  pi  <  ( 2  x.  pi )
185184, 131breqtri 4439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  pi  <  T
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( 0 (,) pi )  ->  pi  <  T )
187173, 179, 180, 181, 186lttrd 9821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( 0 (,) pi )  ->  x  <  T )
188 modid 12152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( x  e.  RR  /\  T  e.  RR+ )  /\  ( 0  <_  x  /\  x  <  T ) )  ->  ( x  mod  T )  =  x )
189173, 174, 178, 187, 188syl22anc 1277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( 0 (,) pi )  ->  (
x  mod  T )  =  x )
190189, 181eqbrtrd 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( 0 (,) pi )  ->  (
x  mod  T )  <  pi )
191190iftrued 3900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( 0 (,) pi )  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  1 )
192191mpteq2ia 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( 0 (,) pi )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( x  e.  ( 0 (,) pi )  |->  1 )
193169, 172, 1923eqtrri 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  e.  ( 0 (,) pi )  |->  1 )  =  ( F  |`  ( 0 (,) pi ) )
194193oveq2i 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( RR 
_D  ( x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( RR  _D  ( F  |`  ( 0 (,) pi ) ) )
195 reelprrecn 9656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  RR  e.  { RR ,  CC }
196195a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  RR  e.  { RR ,  CC } )
197 iooretop 21834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0 (,) pi )  e.  ( topGen `  ran  (,) )
198 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
199198tgioo2 21869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
200197, 199eleqtri 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0 (,) pi )  e.  ( ( TopOpen ` fld )t  RR )
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  ( 0 (,) pi )  e.  ( ( TopOpen
` fld
)t 
RR ) )
202 1cnd 9684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  1  e.  CC )
203196, 201, 202dvmptconst 37822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  ( RR  _D  (
x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( x  e.  ( 0 (,) pi )  |->  0 ) )
204203trud 1463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( RR 
_D  ( x  e.  ( 0 (,) pi )  |->  1 ) )  =  ( x  e.  ( 0 (,) pi )  |->  0 )
205 ssid 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  RR  C_  RR
206 ax-resscn 9621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  RR  C_  CC
207 fss 5759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( F : RR --> RR  /\  RR  C_  CC )  ->  F : RR --> CC )
208109, 206, 207mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F : RR
--> CC
209 dvresioo 37830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( RR  C_  RR  /\  F : RR --> CC )  -> 
( RR  _D  ( F  |`  ( 0 (,) pi ) ) )  =  ( ( RR 
_D  F )  |`  ( 0 (,) pi ) ) )
210205, 208, 209mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( RR 
_D  ( F  |`  ( 0 (,) pi ) ) )  =  ( ( RR  _D  F )  |`  (
0 (,) pi ) )
211194, 204, 2103eqtr3i 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( 0 (,) pi )  |->  0 )  =  ( ( RR 
_D  F )  |`  ( 0 (,) pi ) )
212211dmeqi 5054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  dom  (
x  e.  ( 0 (,) pi )  |->  0 )  =  dom  (
( RR  _D  F
)  |`  ( 0 (,) pi ) )
213 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  ( 0 (,) pi )  |->  0 )  =  ( x  e.  ( 0 (,) pi )  |->  0 )
21489, 213dmmpti 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  dom  (
x  e.  ( 0 (,) pi )  |->  0 )  =  ( 0 (,) pi )
215212, 214eqtr3i 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  dom  (
( RR  _D  F
)  |`  ( 0 (,) pi ) )  =  ( 0 (,) pi )
216 ssdmres 5144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 0 (,) pi ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( 0 (,) pi ) )  =  ( 0 (,) pi ) )
217215, 216mpbir 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0 (,) pi )  C_  dom  ( RR  _D  F
)
218217sseli 3439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  dom  ( RR  _D  F ) )
219168, 218elind 3629 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( 0 (,) pi )  ->  x  e.  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) ) )
220 dmres 5143 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  =  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) )
221219, 220syl6eleqr 2550 . . . . . . . . . . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  RR )
227 ioogtlb 37629 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  x  e.  ( -u pi (,) pi ) )  ->  -u pi  <  x )
228159, 153, 227mp3an12 1363 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) pi )  ->  -u pi  <  x )
229228ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -u pi  <  x )
230 0red 9669 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  -> 
0  e.  RR )
231 neqne 2642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  x  =  0  ->  x  =/=  0 )
232231ad2antlr 738 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  =/=  0 )
233 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  -.  0  <  x )
234226, 230, 232, 233lttri5d 37554 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  <  0 )
235224, 225, 226, 229, 234eliood 37632 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  e.  (
-u pi (,) pi )  /\  -.  x  =  0 )  /\  -.  0  <  x )  ->  x  e.  ( -u pi (,) 0 ) )
23667, 118, 68ltleii 9782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  <_  pi
237 iooss2 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( pi  e.  RR*  /\  0  <_  pi )  ->  ( -u pi (,) 0 ) 
C_  ( -u pi (,) pi ) )
238153, 236, 237mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  ( -u pi (,) pi )
239238sseli 3439 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( -u pi (,) pi ) )
240104reseq1i 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( F  |`  ( -u pi (,) 0 ) )  =  ( ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi ,  1 ,  -u 1 ) )  |`  ( -u pi (,) 0 ) )
241 ioossre 11724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -u pi (,) 0 )  C_  RR
242 resmpt 5172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  RR )
246133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  RR+ )
247245, 246modcld 12133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( 2  x.  pi )  =  ( pi  +  pi )
250110, 249eqtri 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  T  =  ( pi  +  pi )
251250oveq2i 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -u pi  +  T )  =  ( -u pi  +  ( pi  +  pi ) )
252 negpicn 23465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  -u pi  e.  CC
253252, 52, 52addassi 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
-u pi  +  pi )  +  pi )  =  ( -u pi  +  ( pi  +  pi ) )
254253eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -u pi  +  ( pi  +  pi ) )  =  ( ( -u pi  +  pi )  +  pi )
25552negidi 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( pi  +  -u pi )  =  0
25652, 252, 255addcomli 9850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( -u pi  +  pi )  =  0
257256oveq1i 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
-u pi  +  pi )  +  pi )  =  ( 0  +  pi )
25852addid2i 9846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 0  +  pi )  =  pi
259257, 258eqtri 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
-u pi  +  pi )  +  pi )  =  pi
260251, 254, 2593eqtrri 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( -u pi  +  T )  <  ( x  +  T ) )
266261, 265eqbrtrd 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <  ( x  +  T
) )
267244, 248, 266ltled 9808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <_  ( x  +  T
) )
268 0red 9669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  e.  RR )
269158, 120readdcli 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  ( -u pi  +  T ) )
273268, 270, 248, 272, 265lttrd 9821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <  ( x  +  T
) )
274268, 248, 273ltled 9808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  0  <_  ( x  +  T
) )
275245recnd 9694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  CC )
276121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  T  e.  CC )
277275, 276addcomd 9860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( T  +  x ) )
278 iooltub 37647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  x  e.  ( -u pi (,) 0 ) )  ->  x  <  0 )
279159, 151, 278mp3an12 1363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  <  0 )
280 ltaddneg 37545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( x  e.  RR  /\  T  e.  RR )  ->  ( x  <  0  <->  ( T  +  x )  <  T ) )
281245, 120, 280sylancl 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  <  0  <->  ( T  +  x )  <  T
) )
282279, 281mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( -u pi (,) 0 )  ->  ( T  +  x )  <  T )
283277, 282eqbrtrd 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  <  T )
284274, 283jca 539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
0  <_  ( x  +  T )  /\  (
x  +  T )  <  T ) )
285 modid2 12155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( x  +  T
)  e.  RR  /\  T  e.  RR+ )  -> 
( ( ( x  +  T )  mod 
T )  =  ( x  +  T )  <-> 
( 0  <_  (
x  +  T )  /\  ( x  +  T )  <  T
) ) )
286248, 133, 285sylancl 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
( ( x  +  T )  mod  T
)  =  ( x  +  T )  <->  ( 0  <_  ( x  +  T )  /\  (
x  +  T )  <  T ) ) )
287284, 286mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  RR  ->  1  e.  ZZ )
291141, 289, 290, 136syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  e.  RR  ->  (
( x  +  ( 1  x.  T ) )  mod  T )  =  ( x  mod  T ) )
292288, 291eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -u pi (,) 0 )  ->  (
x  +  T )  =  ( x  mod  T ) )
295267, 294breqtrd 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( -u pi (,) 0 )  ->  pi  <_  ( x  mod  T
) )
296244, 247, 295lensymd 9811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -u pi (,) 0 )  ->  -.  ( x  mod  T )  <  pi )
297296iffalsed 3903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( -u pi (,) 0 )  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  -u 1
)
298297mpteq2ia 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  e.  ( -u pi (,) 0 )  |->  if ( ( x  mod  T
)  <  pi , 
1 ,  -u 1
) )  =  ( x  e.  ( -u pi (,) 0 )  |->  -u
1 )
299240, 243, 2983eqtrri 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( F  |`  ( -u pi (,) 0 ) )
300299oveq2i 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( RR 
_D  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
) )  =  ( RR  _D  ( F  |`  ( -u pi (,) 0 ) ) )
301 iooretop 21834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -u pi (,) 0 )  e.  ( topGen `  ran  (,) )
302301, 199eleqtri 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -u pi (,) 0 )  e.  ( ( TopOpen ` fld )t  RR )
303302a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  ( -u pi (,) 0 )  e.  ( ( TopOpen ` fld )t  RR ) )
304202negcld 9998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  -u 1  e.  CC )
305196, 303, 304dvmptconst 37822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  ( RR  _D  (
x  e.  ( -u pi (,) 0 )  |->  -u
1 ) )  =  ( x  e.  (
-u pi (,) 0
)  |->  0 ) )
306305trud 1463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( RR 
_D  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
) )  =  ( x  e.  ( -u pi (,) 0 )  |->  0 )
307 dvresioo 37830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( RR  C_  RR  /\  F : RR --> CC )  -> 
( RR  _D  ( F  |`  ( -u pi (,) 0 ) ) )  =  ( ( RR 
_D  F )  |`  ( -u pi (,) 0
) ) )
308205, 208, 307mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( RR 
_D  ( F  |`  ( -u pi (,) 0
) ) )  =  ( ( RR  _D  F )  |`  ( -u pi (,) 0 ) )
309300, 306, 3083eqtr3i 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( ( RR 
_D  F )  |`  ( -u pi (,) 0
) )
310309dmeqi 5054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  dom  (
x  e.  ( -u pi (,) 0 )  |->  0 )  =  dom  (
( RR  _D  F
)  |`  ( -u pi (,) 0 ) )
311 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( x  e.  ( -u pi (,) 0 )  |->  0 )
31289, 311dmmpti 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  dom  (
x  e.  ( -u pi (,) 0 )  |->  0 )  =  ( -u pi (,) 0 )
313310, 312eqtr3i 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 )
314 ssdmres 5144 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
-u pi (,) 0
)  C_  dom  ( RR 
_D  F )  <->  dom  ( ( RR  _D  F )  |`  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 ) )
315313, 314mpbir 214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  dom  ( RR  _D  F
)
316315sseli 3439 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  dom  ( RR  _D  F ) )
317239, 316elind 3629 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( -u pi (,) 0 )  ->  x  e.  ( ( -u pi (,) pi )  i^i  dom  ( RR  _D  F
) ) )
318317, 220syl6eleqr 2550 . . . . . . . . . . . . . . . . . . . . . . . 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 805 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  ( -u pi (,) pi )  /\  -.  x  =  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
321150, 320sylan 478 . . . . . . . . . . . . . . . . . . . . 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 3567 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  -.  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
323322adantr 471 . . . . . . . . . . . . . . . . . . . . 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 808 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  =  0 )
325 elsn 3993 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  { 0 }  <-> 
x  =  0 )
326324, 325sylibr 217 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( -u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  ->  x  e.  { 0 } )
327326ssriv 3447 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  C_  { 0 }
328 ssfi 7817 . . . . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . . . . 17  |-  ( (
-u pi (,) pi )  \  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )  e. 
Fin
330 inss1 3663 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
-u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  C_  ( -u pi (,) pi )
331220, 330eqsstri 3473 . . . . . . . . . . . . . . . . . . . . 21  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  ( -u pi (,) pi )
332 ioosscn 37628 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u pi (,) pi )  C_  CC
333331, 332sstri 3452 . . . . . . . . . . . . . . . . . . . 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 22910 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
336 fresin 5774 . . . . . . . . . . . . . . . . . . . . . 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 5765 . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . 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 11724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) pi )  C_  RR
344331sseli 3439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  ( -u pi (,) pi ) )
345343, 344sseldi 3441 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  RR )
346345adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  -u pi  <  x )
349 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  <  0 )
350341, 342, 346, 348, 349eliood 37632 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  x  <  0 )  ->  x  e.  ( -u pi (,) 0 ) )
351 elun1 3612 . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
354 0red 9669 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  0  e.  RR )
355345adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  RR )
356 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  -.  x  <  0 )
357354, 355, 356nltled 9810 . . . . . . . . . . . . . . . . . . . . . . . . 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 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
361208a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  F : RR --> CC )
362 0red 9669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  0  e.  RR )
363 mnfxr 11442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |- -oo  e.  RR*
364363a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
-> -oo  e.  RR* )
365362mnfltd 11454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
-> -oo  <  0 )
366360, 364, 362, 365lptioo2 37748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( -oo (,) 0 ) ) )
367 incom 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( RR 
i^i  ( -oo (,) 0 ) )  =  ( ( -oo (,) 0 )  i^i  RR )
368 ioossre 11724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( -oo (,) 0 )  C_  RR
369 df-ss 3429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( -oo (,) 0 ) 
C_  RR  <->  ( ( -oo (,) 0 )  i^i  RR )  =  ( -oo (,) 0 ) )
370368, 369mpbi 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( -oo (,) 0 )  i^i  RR )  =  ( -oo (,) 0
)
371367, 370eqtr2i 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( -oo (,) 0 )  =  ( RR  i^i  ( -oo (,) 0 ) )
372371fveq2i 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
limPt `  ( topGen `  ran  (,) ) ) `  ( -oo (,) 0 ) )  =  ( ( limPt `  ( topGen `  ran  (,) )
) `  ( RR  i^i  ( -oo (,) 0
) ) )
373366, 372syl6eleq 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( RR  i^i  ( -oo (,) 0 ) ) ) )
374 pnfxr 11440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |- +oo  e.  RR*
375374a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
-> +oo  e.  RR* )
376362ltpnfd 11451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  0  < +oo )
377360, 362, 375, 376lptioo1 37749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( 0 (,) +oo ) ) )
378 incom 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( RR 
i^i  ( 0 (,) +oo ) )  =  ( ( 0 (,) +oo )  i^i  RR )
379 ioossre 11724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0 (,) +oo )  C_  RR
380 df-ss 3429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 0 (,) +oo )  C_  RR  <->  ( ( 0 (,) +oo )  i^i 
RR )  =  ( 0 (,) +oo )
)
381379, 380mpbi 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 0 (,) +oo )  i^i  RR )  =  ( 0 (,) +oo )
382378, 381eqtr2i 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0 (,) +oo )  =  ( RR  i^i  (
0 (,) +oo )
)
383382fveq2i 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
limPt `  ( topGen `  ran  (,) ) ) `  (
0 (,) +oo )
)  =  ( (
limPt `  ( topGen `  ran  (,) ) ) `  ( RR  i^i  ( 0 (,) +oo ) ) )
384377, 383syl6eleq 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  0  e.  (
( limPt `  ( topGen ` 
ran  (,) ) ) `  ( RR  i^i  (
0 (,) +oo )
) ) )
385 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)
386 mnfle 11463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( -u pi  e.  RR*  -> -oo  <_  -u pi )
387159, 386ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |- -oo  <_  -u pi
388 iooss1 11699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( -oo  e.  RR*  /\ -oo  <_ 
-u pi )  -> 
( -u pi (,) 0
)  C_  ( -oo (,) 0 ) )
389363, 387, 388mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( -u pi (,) 0 )  C_  ( -oo (,) 0 )
390389a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T. 
->  ( -u pi (,) 0 )  C_  ( -oo (,) 0 ) )
391 ioosscn 37628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -oo (,) 0 )  C_  CC
392390, 391syl6ss 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  ( -u pi (,) 0 )  C_  CC )
393 0cnd 9661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  0  e.  CC )
394385, 392, 304, 393constlimc 37741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  -u 1  e.  ( ( x  e.  (
-u pi (,) 0
)  |->  -u 1 ) lim CC  0 ) )
395 resabs1 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -u pi (,) 0 )  |->  -u 1
)  =  ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0
) )
398397oveq1i 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  ( -u pi (,) 0 )  |->  -u
1 ) lim CC  0 )  =  ( ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )
399 fssres 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( F : RR --> CC  /\  ( -oo (,) 0 ) 
C_  RR )  -> 
( F  |`  ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC )
400208, 368, 399mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) )  =  ( ( TopOpen ` fld )t  (
( -oo (,) 0 )  u.  { 0 } ) )
404 0le0 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  <_  0
405 elioc2 11725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR )  ->  ( 0  e.  ( -u pi (,] 0 )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <_ 
0 ) ) )
406159, 67, 405mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 0  e.  ( -u pi (,] 0 )  <->  ( 0  e.  RR  /\  -u pi  <  0  /\  0  <_ 
0 ) )
40767, 164, 404, 406mpbir3an 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  ( -u pi (,] 0 )
408198cnfldtop 21852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( TopOpen ` fld )  e.  Top
409 ovex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -oo (,] 0 )  e.  _V
410 resttop 20224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( -oo (,] 0
)  e.  _V )  ->  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )  e.  Top )
411408, 409, 410mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
TopOpen ` fld )t  ( -oo (,] 0
) )  e.  Top
412159a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  -u pi  e.  RR* )
413 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 37658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  ( -u pi (,] 0 )  e.  ( ( topGen `  ran  (,) )t  ( -oo (,] 0 ) ) )
416415trud 1463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -u pi (,] 0 )  e.  ( ( topGen `  ran  (,) )t  ( -oo (,] 0
) )
417199oveq1i 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( (
TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )
418 iocssre 11742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( -oo  e.  RR*  /\  0  e.  RR )  ->  ( -oo (,] 0 )  C_  RR )
419363, 67, 418mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( -oo (,] 0 )  C_  RR
420195elexi 3066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  RR  e.  _V
421 restabs 20229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( TopOpen ` fld )t  RR )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )
423417, 422eqtri 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
topGen `  ran  (,) )t  ( -oo (,] 0 ) )  =  ( ( TopOpen ` fld )t  ( -oo (,] 0 ) )
424416, 423eleqtri 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( -u pi (,] 0 )  e.  ( ( TopOpen ` fld )t  ( -oo (,] 0
) )
425 isopn3i 20146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( int `  ( (
TopOpen ` fld )t  ( -oo (,] 0
) ) ) `  ( -u pi (,] 0
) )  =  (
-u pi (,] 0
)
427 mnflt0 11455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |- -oo  <  0
428 snunioo2 37643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( -oo  e.  RR*  /\  0  e.  RR*  /\ -oo  <  0 )  ->  (
( -oo (,) 0 )  u.  { 0 } )  =  ( -oo (,] 0 ) )
429363, 151, 427, 428mp3an 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( -oo (,) 0 )  u.  { 0 } )  =  ( -oo (,] 0 )
430429eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( -oo (,] 0 )  =  ( ( -oo (,) 0
)  u.  { 0 } )
431430oveq2i 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
TopOpen ` fld )t  ( -oo (,] 0
) )  =  ( ( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) )
432431fveq2i 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( int `  ( ( TopOpen ` fld )t  ( -oo (,] 0
) ) )  =  ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) )
433 snunioo2 37643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  -u pi  <  0 )  ->  (
( -u pi (,) 0
)  u.  { 0 } )  =  (
-u pi (,] 0
) )
434159, 151, 164, 433mp3an 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
-u pi (,) 0
)  u.  { 0 } )  =  (
-u pi (,] 0
)
435434eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( -u pi (,] 0 )  =  ( ( -u pi (,) 0 )  u.  {
0 } )
436432, 435fveq12i 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( -u pi (,] 0 )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( -oo (,) 0 )  u.  {
0 } ) ) ) `  ( (
-u pi (,) 0
)  u.  { 0 } ) )
438407, 437eleqtri 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T. 
->  ( ( ( F  |`  ( -oo (,) 0
) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )  =  ( ( F  |`  ( -oo (,) 0
) ) lim CC  0 ) )
441440trud 1463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F  |`  ( -oo (,) 0 ) )  |`  ( -u pi (,) 0 ) ) lim CC  0 )  =  ( ( F  |`  ( -oo (,) 0 ) ) lim
CC  0 )
442398, 441eqtri 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ( -u pi (,) 0 )  |->  -u
1 ) lim CC  0 )  =  ( ( F  |`  ( -oo (,) 0 ) ) lim CC  0 )
443394, 442syl6eleq 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  -u 1  e.  ( ( F  |`  ( -oo (,) 0 ) ) lim
CC  0 ) )
444 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( 0 (,) pi )  |->  1 )  =  ( x  e.  ( 0 (,) pi )  |->  1 )
445 ioosscn 37628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0 (,) pi )  C_  CC
446445a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( T. 
->  ( 0 (,) pi )  C_  CC )
447444, 446, 202, 393constlimc 37741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T. 
->  1  e.  (
( x  e.  ( 0 (,) pi ) 
|->  1 ) lim CC  0 ) )
448 ltpnf 11450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( pi  e.  RR  ->  pi  < +oo )
449 xrltle 11476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( pi  e.  RR*  /\ +oo  e.  RR* )  ->  (
pi  < +oo  ->  pi  <_ +oo ) )
450153, 374, 449mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( pi 
< +oo  ->  pi  <_ +oo )
451118, 448, 450mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  pi  <_ +oo
452 iooss2 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( +oo  e.  RR*  /\  pi  <_ +oo )  ->  (
0 (,) pi ) 
C_  ( 0 (,) +oo ) )
453374, 451, 452mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 0 (,) pi )  C_  ( 0 (,) +oo )
454 resabs1 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( 0 (,) pi )  |->  1 )  =  ( ( F  |`  ( 0 (,) +oo ) )  |`  (
0 (,) pi ) )
457456oveq1i 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  ( 0 (,) pi )  |->  1 ) lim CC  0 )  =  ( ( ( F  |`  ( 0 (,) +oo ) )  |`  ( 0 (,) pi ) ) lim CC  0
)
458 fssres 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( F : RR --> CC  /\  ( 0 (,) +oo )  C_  RR )  -> 
( F  |`  (
0 (,) +oo )
) : ( 0 (,) +oo ) --> CC )
459208, 379, 458mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 37628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 0 (,) +oo )  C_  CC
463462a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( T. 
->  ( 0 (,) +oo )  C_  CC )
464 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
TopOpen ` fld )t  ( ( 0 (,) +oo )  u.  { 0 } ) )  =  ( ( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) )
465 elico2 11726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( 0  e.  RR  /\  pi  e.  RR* )  ->  (
0  e.  ( 0 [,) pi )  <->  ( 0  e.  RR  /\  0  <_  0  /\  0  < 
pi ) ) )
46667, 153, 465mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 0  e.  ( 0 [,) pi )  <->  ( 0  e.  RR  /\  0  <_  0  /\  0  < 
pi ) )
46767, 404, 68, 466mpbir3an 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  ( 0 [,) pi )
468 ovex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 0 [,) +oo )  e. 
_V
469 resttop 20224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( 0 [,) +oo )  e.  _V )  ->  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) )  e.  Top )
470408, 468, 469mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) )  e.  Top
471153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  pi  e.  RR* )
472 eqid 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)  =  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)
473451a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( T. 
->  pi  <_ +oo )
474362, 471, 375, 360, 472, 473icoopn 37663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( T. 
->  ( 0 [,) pi )  e.  ( ( topGen `
 ran  (,) )t  (
0 [,) +oo )
) )
475474trud 1463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 0 [,) pi )  e.  ( ( topGen `  ran  (,) )t  ( 0 [,) +oo ) )
476199oveq1i 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)  =  ( ( ( TopOpen ` fld )t  RR )t  ( 0 [,) +oo ) )
477 rge0ssre 11768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( 0 [,) +oo )  C_  RR
478 restabs 20229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( TopOpen ` fld )t  RR )t  ( 0 [,) +oo ) )  =  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) )
480476, 479eqtri 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
topGen `  ran  (,) )t  (
0 [,) +oo )
)  =  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) )
481475, 480eleqtri 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( 0 [,) pi )  e.  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) )
482 isopn3i 20146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( int `  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) ) ) `  ( 0 [,) pi ) )  =  ( 0 [,) pi )
484 0ltpnf 11452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  0  < +oo
485 snunioo1 37650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  < +oo )  ->  ( ( 0 (,) +oo )  u.  { 0 } )  =  ( 0 [,) +oo ) )
486151, 374, 484, 485mp3an 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( 0 (,) +oo )  u.  { 0 } )  =  ( 0 [,) +oo )
487486eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 0 [,) +oo )  =  ( ( 0 (,) +oo )  u.  { 0 } )
488487oveq2i 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) )  =  ( ( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) )
489488fveq2i 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( int `  ( ( TopOpen ` fld )t  ( 0 [,) +oo ) ) )  =  ( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) )
490 snunioo1 37650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  0  < 
pi )  ->  (
( 0 (,) pi )  u.  { 0 } )  =  ( 0 [,) pi ) )
491151, 153, 68, 490mp3an 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( 0 (,) pi )  u.  { 0 } )  =  ( 0 [,) pi )
492491eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( 0 [,) pi )  =  ( ( 0 (,) pi )  u.  {
0 } )
493489, 492fveq12i 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( int `  ( (
TopOpen ` fld )t  ( 0 [,) +oo ) ) ) `  ( 0 [,) pi ) )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) ) `  (
( 0 (,) pi )  u.  { 0 } ) )
494483, 493eqtr3i 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 0 [,) pi )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( 0 (,) +oo )  u. 
{ 0 } ) ) ) `  (
( 0 (,) pi )  u.  { 0 } ) )
495467, 494eleqtri 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T. 
->  ( ( ( F  |`  ( 0 (,) +oo ) )  |`  (
0 (,) pi ) ) lim CC  0 )  =  ( ( F  |`  ( 0 (,) +oo ) ) lim CC  0
) )
498497trud 1463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F  |`  (
0 (,) +oo )
)  |`  ( 0 (,) pi ) ) lim CC  0 )  =  ( ( F  |`  (
0 (,) +oo )
) lim CC  0 )
499457, 498eqtri 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ( 0 (,) pi )  |->  1 ) lim CC  0 )  =  ( ( F  |`  ( 0 (,) +oo ) ) lim CC  0
)
500447, 499syl6eleq 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  1  e.  (
( F  |`  (
0 (,) +oo )
) lim CC  0 ) )
501 neg1lt0 10743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  -u 1  <  0
502106, 67, 105lttri 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
-u 1  <  0  /\  0  <  1
)  ->  -u 1  <  1 )
503501, 34, 502mp2an 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -u 1  <  1
504106, 503ltneii 9772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  -u 1  =/=  1
505504a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( T. 
->  -u 1  =/=  1
)
506198, 359, 360, 361, 362, 373, 384, 443, 500, 505jumpncnp 37813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( T. 
->  -.  F  e.  ( ( ( topGen `  ran  (,) )  CnP  ( TopOpen ` fld )
) `  0 )
)
507506trud 1463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
-u pi (,) pi )  i^i  dom  ( RR  _D  F ) )  C_  dom  ( RR  _D  F
)
512220, 511eqsstri 3473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  dom  ( RR  _D  F
)
513512sseli 3439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  0  e.  dom  ( RR  _D  F ) )
514199, 198dvcnp2 22922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 0  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  F  e.  ( ( ( topGen ` 
ran  (,) )  CnP  ( TopOpen
` fld
) ) `  0
) )
516507, 515mto 181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  0  ->  -.  x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) )
519518necon2ai 2664 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  =/=  0 )
520519adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  =/=  0 )
521354, 355, 357, 520leneltd 9814 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  0  <  x )
522344, 163sylan 478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  0  <  x )  ->  x  e.  ( 0 (,) pi ) )
523 elun2 3613 . . . . . . . . . . . . . . . . . . . . . . . . 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 671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  /\  -.  x  <  0
)  ->  x  e.  ( ( -u pi (,) 0 )  u.  (
0 (,) pi ) ) )
526352, 525pm2.61dan 805 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  ( ( -u pi (,) 0 )  u.  (
0 (,) pi ) ) )
527 ovex 6342 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -u pi (,) 0 )  e. 
_V
528 ovex 6342 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0 (,) pi )  e. 
_V
529527, 528unipr 4224 . . . . . . . . . . . . . . . . . . . . . 22  |-  U. {
( -u pi (,) 0
) ,  ( 0 (,) pi ) }  =  ( ( -u pi (,) 0 )  u.  ( 0 (,) pi ) )
530526, 529syl6eleqr 2550 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  ->  x  e.  U. { ( -u pi (,) 0 ) ,  ( 0 (,) pi ) } )
531530ssriv 3447 . . . . . . . . . . . . . . . . . . . 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 3639 . . . . . . . . . . . . . . . . . . . . . . 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 21830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( topGen ` 
ran  (,) )  e.  Top
535 ovex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( RR 
_D  F )  e. 
_V
536535resex 5166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  e.  _V
537536dmex 6752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  e. 
_V
538534, 537pm3.2i 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
topGen `  ran  (,) )  e.  Top  /\  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  e. 
_V )
539318ssriv 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )
540 ssid 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -u pi (,) 0 )  C_  ( -u pi (,) 0
)
541301, 539, 5403pm3.2i 1192 . . . . . . . . . . . . . . . . . . . . . . . . . 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 20239 . . . . . . . . . . . . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
-u pi (,) 0
)  e.  ( topGen ` 
ran  (,) )  <->  ( -u pi (,) 0 )  e.  ( ( topGen `  ran  (,) )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) )
544301, 543mpbi 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -u pi (,) 0 )  e.  ( ( topGen `  ran  (,) )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
545 inss2 3664 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) ) 
C_  ( -u pi (,) 0 )
546539, 540ssini 3666 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -u pi (,) 0 )  C_  ( dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) )
547545, 546eqssi 3459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( -u pi (,) 0 ) )  =  ( -u pi (,) 0 )
548199oveq1i 6324 . . . . . . . . . . . . . . . . . . . . . . . . 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 3452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  dom  (
( RR  _D  F
)  |`  ( -u pi (,) pi ) )  C_  RR
550 restabs 20229 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . . . . . . . . . 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 2484 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
TopOpen ` fld )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )  =  ( ( topGen `  ran  (,) )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
553544, 547, 5523eltr4i 2552 . . . . . . . . . . . . . . . . . . . . . . 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 2547 . . . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . . . 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 2642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  x  =  ( -u pi (,) 0 )  ->  x  =/=  ( -u pi (,) 0 ) )
557 elprn1 37750 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  { (
-u pi (,) 0
) ,  ( 0 (,) pi ) }  /\  x  =/=  ( -u pi (,) 0 ) )  ->  x  =  ( 0 (,) pi ) )
558556, 557sylan2 481 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  { (
-u pi (,) 0
) ,  ( 0 (,) pi ) }  /\  -.  x  =  ( -u pi (,) 0 ) )  ->  x  =  ( 0 (,) pi ) )
559 ineq2 3639 . . . . . . . . . . . . . . . . . . . . . . 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 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 0 (,) pi )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )
561 ssid 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 0 (,) pi )  C_  ( 0 (,) pi )
562197, 560, 5613pm3.2i 1192 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 0 (,) pi )  e.  ( topGen `  ran  (,) )  /\  ( 0 (,) pi )  C_  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  /\  ( 0 (,) pi )  C_  ( 0 (,) pi ) )
563 restopnb 20239 . . . . . . . . . . . . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 0 (,) pi )  e.  ( topGen `  ran  (,) )  <->  ( 0 (,) pi )  e.  ( ( topGen `  ran  (,) )t  dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) ) ) )
565197, 564mpbi 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0 (,) pi )  e.  ( ( topGen `  ran  (,) )t 
dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) ) )
566 inss2 3664 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( 0 (,) pi ) ) 
C_  ( 0 (,) pi )
567560, 561ssini 3666 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0 (,) pi )  C_  ( dom  ( ( RR 
_D  F )  |`  ( -u pi (,) pi ) )  i^i  (
0 (,) pi ) )
568566, 567eqssi 3459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )  i^i  ( 0 (,) pi ) )  =  ( 0 (,) pi )
569565, 568, 5523eltr4i 2552 . . . . . . . . . . . . . . . . . . . . . . 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 2547 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( 0 (,)