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

Theorem fourierdlem113 37351
Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem113.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem113.t  |-  T  =  ( 2  x.  pi )
fourierdlem113.per  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
fourierdlem113.x  |-  ( ph  ->  X  e.  RR )
fourierdlem113.l  |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
fourierdlem113.r  |-  ( ph  ->  R  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
fourierdlem113.p  |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... n ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem113.m  |-  ( ph  ->  M  e.  NN )
fourierdlem113.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem113.dvcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem113.dvlb  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =/=  (/) )
fourierdlem113.dvub  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =/=  (/) )
fourierdlem113.a  |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
fourierdlem113.b  |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) )
fourierdlem113.15  |-  S  =  ( n  e.  NN  |->  ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )
fourierdlem113.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( pi  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem113.exq  |-  ( ph  ->  ( E `  X
)  e.  ran  Q
)
Assertion
Ref Expression
fourierdlem113  |-  ( ph  ->  (  seq 1 (  +  ,  S )  ~~>  ( ( ( L  +  R )  / 
2 )  -  (
( A `  0
)  /  2 ) )  /\  ( ( ( A `  0
)  /  2 )  +  sum_ n  e.  NN  ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )  =  ( ( L  +  R )  /  2 ) ) )
Distinct variable groups:    A, n    B, n    x, E    i, F, n, x    i, L, n    i, M, x, n    M, p, i, n    Q, i, x, n    Q, p    R, i, n    T, i, x, n    T, p   
i, X, x, n    X, p    ph, i, x, n
Allowed substitution hints:    ph( p)    A( x, i, p)    B( x, i, p)    P( x, i, n, p)    R( x, p)    S( x, i, n, p)    E( i, n, p)    F( p)    L( x, p)

Proof of Theorem fourierdlem113
Dummy variables  j 
k  m  w  y  t  u  z  f  g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem113.f . 2  |-  ( ph  ->  F : RR --> RR )
2 oveq1 6284 . . . . . . 7  |-  ( w  =  y  ->  (
w  mod  ( 2  x.  pi ) )  =  ( y  mod  ( 2  x.  pi ) ) )
32eqeq1d 2404 . . . . . 6  |-  ( w  =  y  ->  (
( w  mod  (
2  x.  pi ) )  =  0  <->  (
y  mod  ( 2  x.  pi ) )  =  0 ) )
4 oveq2 6285 . . . . . . . 8  |-  ( w  =  y  ->  (
( k  +  ( 1  /  2 ) )  x.  w )  =  ( ( k  +  ( 1  / 
2 ) )  x.  y ) )
54fveq2d 5852 . . . . . . 7  |-  ( w  =  y  ->  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  w ) )  =  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  y ) ) )
6 oveq1 6284 . . . . . . . . 9  |-  ( w  =  y  ->  (
w  /  2 )  =  ( y  / 
2 ) )
76fveq2d 5852 . . . . . . . 8  |-  ( w  =  y  ->  ( sin `  ( w  / 
2 ) )  =  ( sin `  (
y  /  2 ) ) )
87oveq2d 6293 . . . . . . 7  |-  ( w  =  y  ->  (
( 2  x.  pi )  x.  ( sin `  ( w  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
95, 8oveq12d 6295 . . . . . 6  |-  ( w  =  y  ->  (
( sin `  (
( k  +  ( 1  /  2 ) )  x.  w ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
w  /  2 ) ) ) )  =  ( ( sin `  (
( k  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )
103, 9ifbieq2d 3909 . . . . 5  |-  ( w  =  y  ->  if ( ( w  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( k  +  ( 1  /  2 ) )  x.  w ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
w  /  2 ) ) ) ) )  =  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  /  ( 2  x.  pi ) ) ,  ( ( sin `  ( ( k  +  ( 1  /  2
) )  x.  y
) )  /  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) ) )
1110cbvmptv 4486 . . . 4  |-  ( w  e.  RR  |->  if ( ( w  mod  (
2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  /  (
2  x.  pi ) ) ,  ( ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  w ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
w  /  2 ) ) ) ) ) )  =  ( y  e.  RR  |->  if ( ( y  mod  (
2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  /  (
2  x.  pi ) ) ,  ( ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )
12 oveq2 6285 . . . . . . . 8  |-  ( k  =  m  ->  (
2  x.  k )  =  ( 2  x.  m ) )
1312oveq1d 6292 . . . . . . 7  |-  ( k  =  m  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  m )  +  1 ) )
1413oveq1d 6292 . . . . . 6  |-  ( k  =  m  ->  (
( ( 2  x.  k )  +  1 )  /  ( 2  x.  pi ) )  =  ( ( ( 2  x.  m )  +  1 )  / 
( 2  x.  pi ) ) )
15 oveq1 6284 . . . . . . . . 9  |-  ( k  =  m  ->  (
k  +  ( 1  /  2 ) )  =  ( m  +  ( 1  /  2
) ) )
1615oveq1d 6292 . . . . . . . 8  |-  ( k  =  m  ->  (
( k  +  ( 1  /  2 ) )  x.  y )  =  ( ( m  +  ( 1  / 
2 ) )  x.  y ) )
1716fveq2d 5852 . . . . . . 7  |-  ( k  =  m  ->  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  y ) )  =  ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) ) )
1817oveq1d 6292 . . . . . 6  |-  ( k  =  m  ->  (
( sin `  (
( k  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  =  ( ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )
1914, 18ifeq12d 3904 . . . . 5  |-  ( k  =  m  ->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( k  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  /  ( 2  x.  pi ) ) ,  ( ( sin `  ( ( m  +  ( 1  /  2
) )  x.  y
) )  /  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) ) )
2019mpteq2dv 4481 . . . 4  |-  ( k  =  m  ->  (
y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( k  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )  =  ( y  e.  RR  |->  if ( ( y  mod  (
2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  /  (
2  x.  pi ) ) ,  ( ( sin `  ( ( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
2111, 20syl5eq 2455 . . 3  |-  ( k  =  m  ->  (
w  e.  RR  |->  if ( ( w  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( k  +  ( 1  /  2 ) )  x.  w ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
w  /  2 ) ) ) ) ) )  =  ( y  e.  RR  |->  if ( ( y  mod  (
2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  /  (
2  x.  pi ) ) ,  ( ( sin `  ( ( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
2221cbvmptv 4486 . 2  |-  ( k  e.  NN  |->  ( w  e.  RR  |->  if ( ( w  mod  (
2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  k )  +  1 )  /  (
2  x.  pi ) ) ,  ( ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  w ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
w  /  2 ) ) ) ) ) ) )  =  ( m  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
23 fourierdlem113.p . 2  |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... n ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
24 fourierdlem113.m . 2  |-  ( ph  ->  M  e.  NN )
25 fourierdlem113.q . 2  |-  ( ph  ->  Q  e.  ( P `
 M ) )
26 oveq1 6284 . . . . . . . 8  |-  ( w  =  y  ->  (
w  +  ( j  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
2726eleq1d 2471 . . . . . . 7  |-  ( w  =  y  ->  (
( w  +  ( j  x.  T ) )  e.  ran  Q  <->  ( y  +  ( j  x.  T ) )  e.  ran  Q ) )
2827rexbidv 2917 . . . . . 6  |-  ( w  =  y  ->  ( E. j  e.  ZZ  ( w  +  (
j  x.  T ) )  e.  ran  Q  <->  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q ) )
2928cbvrabv 3057 . . . . 5  |-  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q }  =  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q }
3029uneq2i 3593 . . . 4  |-  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } )  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q }
)
3130fveq2i 5851 . . 3  |-  ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  =  ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q }
) )
3231oveq1i 6287 . 2  |-  ( (
# `  ( {
( -u pi  +  X
) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 )  =  ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q }
) )  -  1 )
33 oveq1 6284 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
3433oveq2d 6293 . . . . . . . . . . 11  |-  ( k  =  j  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
3534eleq1d 2471 . . . . . . . . . 10  |-  ( k  =  j  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( j  x.  T ) )  e.  ran  Q ) )
3635cbvrexv 3034 . . . . . . . . 9  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q )
3736a1i 11 . . . . . . . 8  |-  ( y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q ) )
3837rabbiia 3047 . . . . . . 7  |-  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }  =  { y  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q }
3938uneq2i 3593 . . . . . 6  |-  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q }
)
40 isoeq5 6201 . . . . . 6  |-  ( ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  ran  Q }
)  ->  ( g  Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) ) )
4139, 40ax-mp 5 . . . . 5  |-  ( g 
Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) )
4241a1i 11 . . . 4  |-  ( g  =  f  ->  (
g  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) ) )
4333oveq2d 6293 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
w  +  ( k  x.  T ) )  =  ( w  +  ( j  x.  T
) ) )
4443eleq1d 2471 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  (
( w  +  ( k  x.  T ) )  e.  ran  Q  <->  ( w  +  ( j  x.  T ) )  e.  ran  Q ) )
4544cbvrexv 3034 . . . . . . . . . . . 12  |-  ( E. k  e.  ZZ  (
w  +  ( k  x.  T ) )  e.  ran  Q  <->  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q )
4645a1i 11 . . . . . . . . . . 11  |-  ( w  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  ->  ( E. k  e.  ZZ  ( w  +  (
k  x.  T ) )  e.  ran  Q  <->  E. j  e.  ZZ  (
w  +  ( j  x.  T ) )  e.  ran  Q ) )
4746rabbiia 3047 . . . . . . . . . 10  |-  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q }  =  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q }
4847uneq2i 3593 . . . . . . . . 9  |-  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } )  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } )
4948fveq2i 5851 . . . . . . . 8  |-  ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  =  ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )
5049oveq1i 6287 . . . . . . 7  |-  ( (
# `  ( {
( -u pi  +  X
) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 )  =  ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 )
5150oveq2i 6288 . . . . . 6  |-  ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) )  =  ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) )
52 isoeq4 6200 . . . . . 6  |-  ( ( 0 ... ( (
# `  ( {
( -u pi  +  X
) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) )  =  ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) )  -> 
( g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) )  <->  g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) ) )
5351, 52ax-mp 5 . . . . 5  |-  ( g 
Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) )  <->  g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) )
5453a1i 11 . . . 4  |-  ( g  =  f  ->  (
g  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) )  <->  g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) ) )
55 isoeq1 6197 . . . 4  |-  ( g  =  f  ->  (
g  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) ) )
5642, 54, 553bitrd 279 . . 3  |-  ( g  =  f  ->  (
g  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) ) )
5756cbviotav 5538 . 2  |-  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) )  =  ( iota f
f  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. j  e.  ZZ  ( w  +  ( j  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  ran  Q } ) ) )
58 fourierdlem113.x . 2  |-  ( ph  ->  X  e.  RR )
59 pire 23141 . . . . 5  |-  pi  e.  RR
6059renegcli 9915 . . . 4  |-  -u pi  e.  RR
6160a1i 11 . . 3  |-  ( ph  -> 
-u pi  e.  RR )
6259a1i 11 . . 3  |-  ( ph  ->  pi  e.  RR )
63 negpilt0 36816 . . . 4  |-  -u pi  <  0
6463a1i 11 . . 3  |-  ( ph  -> 
-u pi  <  0
)
65 pipos 23143 . . . 4  |-  0  <  pi
6665a1i 11 . . 3  |-  ( ph  ->  0  <  pi )
67 picn 23142 . . . . 5  |-  pi  e.  CC
68672timesi 10696 . . . 4  |-  ( 2  x.  pi )  =  ( pi  +  pi )
69 fourierdlem113.t . . . 4  |-  T  =  ( 2  x.  pi )
7067, 67subnegi 9933 . . . 4  |-  ( pi 
-  -u pi )  =  ( pi  +  pi )
7168, 69, 703eqtr4i 2441 . . 3  |-  T  =  ( pi  -  -u pi )
7223fourierdlem2 37240 . . . . . . . 8  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
7324, 72syl 17 . . . . . . 7  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
7425, 73mpbid 210 . . . . . 6  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
7574simpld 457 . . . . 5  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
76 elmapi 7477 . . . . 5  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
7775, 76syl 17 . . . 4  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
78 fzfid 12122 . . . 4  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
79 rnffi 36807 . . . 4  |-  ( ( Q : ( 0 ... M ) --> RR 
/\  ( 0 ... M )  e.  Fin )  ->  ran  Q  e.  Fin )
8077, 78, 79syl2anc 659 . . 3  |-  ( ph  ->  ran  Q  e.  Fin )
8123, 24, 25fourierdlem15 37253 . . . 4  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
82 frn 5719 . . . 4  |-  ( Q : ( 0 ... M ) --> ( -u pi [,] pi )  ->  ran  Q  C_  ( -u pi [,] pi ) )
8381, 82syl 17 . . 3  |-  ( ph  ->  ran  Q  C_  ( -u pi [,] pi ) )
8474simprd 461 . . . . 5  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
8584simplrd 755 . . . 4  |-  ( ph  ->  ( Q `  M
)  =  pi )
86 ffun 5715 . . . . . 6  |-  ( Q : ( 0 ... M ) --> ( -u pi [,] pi )  ->  Fun  Q )
8781, 86syl 17 . . . . 5  |-  ( ph  ->  Fun  Q )
8824nnnn0d 10892 . . . . . . . 8  |-  ( ph  ->  M  e.  NN0 )
89 nn0uz 11160 . . . . . . . 8  |-  NN0  =  ( ZZ>= `  0 )
9088, 89syl6eleq 2500 . . . . . . 7  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
91 eluzfz2 11746 . . . . . . 7  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
9290, 91syl 17 . . . . . 6  |-  ( ph  ->  M  e.  ( 0 ... M ) )
93 fdm 5717 . . . . . . . 8  |-  ( Q : ( 0 ... M ) --> ( -u pi [,] pi )  ->  dom  Q  =  ( 0 ... M ) )
9481, 93syl 17 . . . . . . 7  |-  ( ph  ->  dom  Q  =  ( 0 ... M ) )
9594eqcomd 2410 . . . . . 6  |-  ( ph  ->  ( 0 ... M
)  =  dom  Q
)
9692, 95eleqtrd 2492 . . . . 5  |-  ( ph  ->  M  e.  dom  Q
)
97 fvelrn 6001 . . . . 5  |-  ( ( Fun  Q  /\  M  e.  dom  Q )  -> 
( Q `  M
)  e.  ran  Q
)
9887, 96, 97syl2anc 659 . . . 4  |-  ( ph  ->  ( Q `  M
)  e.  ran  Q
)
9985, 98eqeltrrd 2491 . . 3  |-  ( ph  ->  pi  e.  ran  Q
)
100 fourierdlem113.e . . 3  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( pi  -  x
)  /  T ) )  x.  T ) ) )
101 fourierdlem113.exq . . 3  |-  ( ph  ->  ( E `  X
)  e.  ran  Q
)
102 eqid 2402 . . 3  |-  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } )  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } )
103 isoeq1 6197 . . . . 5  |-  ( g  =  f  ->  (
g  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
10430, 48, 393eqtr4ri 2442 . . . . . 6  |-  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } )
105 isoeq5 6201 . . . . . 6  |-  ( ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } )  ->  (
f  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
106104, 105ax-mp 5 . . . . 5  |-  ( f 
Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) ) )
107103, 106syl6bb 261 . . . 4  |-  ( g  =  f  ->  (
g  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
108107cbviotav 5538 . . 3  |-  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) )  =  ( iota f
f  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { w  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) ) )
109 eqid 2402 . . 3  |-  { w  e.  ( ( -u pi  +  X ) (,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q }  =  { w  e.  ( ( -u pi  +  X ) (,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q }
11061, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109fourierdlem51 37289 . 2  |-  ( ph  ->  X  e.  ran  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
w  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( w  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
111 fourierdlem113.per . 2  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
112 ax-resscn 9578 . . . 4  |-  RR  C_  CC
113112a1i 11 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  CC )
114 ioossre 11638 . . . . . . 7  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
115114a1i 11 . . . . . 6  |-  ( ph  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR )
1161, 115fssresd 5734 . . . . 5  |-  ( ph  ->  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> RR )
117112a1i 11 . . . . 5  |-  ( ph  ->  RR  C_  CC )
118116, 117fssd 5722 . . . 4  |-  ( ph  ->  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC )
119118adantr 463 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
120114a1i 11 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
1211, 117fssd 5722 . . . . . . 7  |-  ( ph  ->  F : RR --> CC )
122121adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
123 ssid 3460 . . . . . . 7  |-  RR  C_  RR
124123a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  RR )
125 eqid 2402 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
126125tgioo2 21598 . . . . . . 7  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
127125, 126dvres 22605 . . . . . 6  |-  ( ( ( RR  C_  CC  /\  F : RR --> CC )  /\  ( RR  C_  RR  /\  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) )
128113, 122, 124, 120, 127syl22anc 1231 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) )
129128dmeqd 5025 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( RR  _D  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )  =  dom  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) )
130 ioontr 36898 . . . . . . 7  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
131130reseq2i 5090 . . . . . 6  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )  =  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
132131dmeqi 5024 . . . . 5  |-  dom  (
( RR  _D  F
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )  =  dom  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
133132a1i 11 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )  =  dom  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
134 fourierdlem113.dvcn . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
135 cncff 21687 . . . . 5  |-  ( ( ( RR  _D  F
)  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
136 fdm 5717 . . . . 5  |-  ( ( ( RR  _D  F
)  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC  ->  dom  ( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
137134, 135, 1363syl 20 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
138129, 133, 1373eqtrd 2447 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( RR  _D  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
139 dvcn 22614 . . 3  |-  ( ( ( RR  C_  CC  /\  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC 
/\  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )  /\  dom  ( RR 
_D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
140113, 119, 120, 138, 139syl31anc 1233 . 2  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
141120, 113sstrd 3451 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
14277adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
143 fzofzp1 11944 . . . . . . 7  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
144143adantl 464 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
145142, 144ffvelrnd 6009 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
146145rexrd 9672 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
147 elfzofz 11872 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
148147adantl 464 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
149142, 148ffvelrnd 6009 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
15074simprrd 759 . . . . 5  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
151150r19.21bi 2772 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
152125, 146, 149, 151lptioo1cn 37001 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
153116adantr 463 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> RR )
154123a1i 11 . . . . . . . 8  |-  ( ph  ->  RR  C_  RR )
155117, 121, 154dvbss 22595 . . . . . . 7  |-  ( ph  ->  dom  ( RR  _D  F )  C_  RR )
156 dvfre 22644 . . . . . . . 8  |-  ( ( F : RR --> RR  /\  RR  C_  RR )  -> 
( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
1571, 154, 156syl2anc 659 . . . . . . 7  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
158 0re 9625 . . . . . . . . . 10  |-  0  e.  RR
15960, 158, 59lttri 9741 . . . . . . . . 9  |-  ( (
-u pi  <  0  /\  0  <  pi )  ->  -u pi  <  pi )
16063, 65, 159mp2an 670 . . . . . . . 8  |-  -u pi  <  pi
161160a1i 11 . . . . . . 7  |-  ( ph  -> 
-u pi  <  pi )
16284simplld 753 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
163134, 135syl 17 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
164 fourierdlem113.dvlb . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =/=  (/) )
165163, 141, 152, 164, 125ellimciota 36969 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( iota x x  e.  ( (
( RR  _D  F
)  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  e.  ( ( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
166149rexrd 9672 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
167125, 166, 145, 151lptioo2cn 37000 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
168 fourierdlem113.dvub . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =/=  (/) )
169163, 141, 167, 168, 125ellimciota 36969 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( iota x x  e.  ( (
( RR  _D  F
)  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
170121adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ZZ )  ->  F : RR
--> CC )
171 zre 10908 . . . . . . . . . . . 12  |-  ( k  e.  ZZ  ->  k  e.  RR )
172171adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  RR )
173 2re 10645 . . . . . . . . . . . . . . 15  |-  2  e.  RR
174173, 59remulcli 9639 . . . . . . . . . . . . . 14  |-  ( 2  x.  pi )  e.  RR
175174a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  x.  pi )  e.  RR )
17669, 175syl5eqel 2494 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  RR )
177176adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  RR )
178172, 177remulcld 9653 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  x.  T )  e.  RR )
179170adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  F : RR --> CC )
180177adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  T  e.  RR )
181 simplr 754 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  k  e.  ZZ )
182 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  t  e.  RR )
183111adant423 36782 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
184179, 180, 181, 182, 183fperiodmul 36853 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  ( F `  ( t  +  ( k  x.  T ) ) )  =  ( F `  t ) )
185 eqid 2402 . . . . . . . . . 10  |-  ( RR 
_D  F )  =  ( RR  _D  F
)
186170, 178, 184, 185fperdvper 37064 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  dom  ( RR  _D  F ) )  -> 
( ( t  +  ( k  x.  T
) )  e.  dom  ( RR  _D  F
)  /\  ( ( RR  _D  F ) `  ( t  +  ( k  x.  T ) ) )  =  ( ( RR  _D  F
) `  t )
) )
187186an32s 805 . . . . . . . 8  |-  ( ( ( ph  /\  t  e.  dom  ( RR  _D  F ) )  /\  k  e.  ZZ )  ->  ( ( t  +  ( k  x.  T
) )  e.  dom  ( RR  _D  F
)  /\  ( ( RR  _D  F ) `  ( t  +  ( k  x.  T ) ) )  =  ( ( RR  _D  F
) `  t )
) )
188187simpld 457 . . . . . . 7  |-  ( ( ( ph  /\  t  e.  dom  ( RR  _D  F ) )  /\  k  e.  ZZ )  ->  ( t  +  ( k  x.  T ) )  e.  dom  ( RR  _D  F ) )
189187simprd 461 . . . . . . 7  |-  ( ( ( ph  /\  t  e.  dom  ( RR  _D  F ) )  /\  k  e.  ZZ )  ->  ( ( RR  _D  F ) `  (
t  +  ( k  x.  T ) ) )  =  ( ( RR  _D  F ) `
 t ) )
190 fveq2 5848 . . . . . . . . 9  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
191 oveq1 6284 . . . . . . . . . 10  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
192191fveq2d 5852 . . . . . . . . 9  |-  ( j  =  i  ->  ( Q `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
193190, 192oveq12d 6295 . . . . . . . 8  |-  ( j  =  i  ->  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
194193cbvmptv 4486 . . . . . . 7  |-  ( j  e.  ( 0..^ M )  |->  ( ( Q `
 j ) (,) ( Q `  (
j  +  1 ) ) ) )  =  ( i  e.  ( 0..^ M )  |->  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
195 eqid 2402 . . . . . . 7  |-  ( t  e.  RR  |->  ( t  +  ( ( |_
`  ( ( pi 
-  t )  /  T ) )  x.  T ) ) )  =  ( t  e.  RR  |->  ( t  +  ( ( |_ `  ( ( pi  -  t )  /  T
) )  x.  T
) ) )
196155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195fourierdlem71 37309 . . . . . 6  |-  ( ph  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
197196adantr 463 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
198 nfv 1728 . . . . . . . . 9  |-  F/ t ( ph  /\  i  e.  ( 0..^ M ) )
199 nfra1 2784 . . . . . . . . 9  |-  F/ t A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z
200198, 199nfan 1956 . . . . . . . 8  |-  F/ t ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
201128, 131syl6eq 2459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
202201fveq1d 5850 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) `  t )  =  ( ( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t ) )
203 fvres 5862 . . . . . . . . . . . . 13  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t )  =  ( ( RR 
_D  F ) `  t ) )
204202, 203sylan9eq 2463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) `
 t )  =  ( ( RR  _D  F ) `  t
) )
205204fveq2d 5852 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR 
_D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) `  t ) )  =  ( abs `  (
( RR  _D  F
) `  t )
) )
206205adantlr 713 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( RR  _D  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) `
 t ) )  =  ( abs `  (
( RR  _D  F
) `  t )
) )
207 simplr 754 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
208 ssdmres 5114 . . . . . . . . . . . . . 14  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
209137, 208sylibr 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  ( RR  _D  F
) )
210209ad2antrr 724 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  dom  ( RR 
_D  F ) )
211 simpr 459 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
212210, 211sseldd 3442 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
t  e.  dom  ( RR  _D  F ) )
213 rspa 2770 . . . . . . . . . . 11  |-  ( ( A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z  /\  t  e.  dom  ( RR 
_D  F ) )  ->  ( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
214207, 212, 213syl2anc 659 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
215206, 214eqbrtrd 4414 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( RR  _D  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) `
 t ) )  <_  z )
216215ex 432 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z
)  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( abs `  ( ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) `  t ) )  <_  z )
)
217200, 216ralrimi 2803 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z
)  ->  A. t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) `
 t ) )  <_  z )
218217ex 432 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z  ->  A. t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) `
 t ) )  <_  z ) )
219218reximdv 2877 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( E. z  e.  RR  A. t  e. 
dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z  ->  E. z  e.  RR  A. t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) `  t ) )  <_ 
z ) )
220197, 219mpd 15 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. z  e.  RR  A. t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) `  t ) )  <_ 
z )
221149, 145, 153, 138, 220ioodvbdlimc1 37079 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =/=  (/) )
222119, 141, 152, 221, 125ellimciota 36969 . 2  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( iota y
y  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
223149, 145, 153, 138, 220ioodvbdlimc2 37081 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =/=  (/) )
224119, 141, 167, 223, 125ellimciota 36969 . 2  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( iota y
y  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
225 frel 5716 . . . . . . 7  |-  ( ( RR  _D  F ) : dom  ( RR 
_D  F ) --> RR 
->  Rel  ( RR  _D  F ) )
226157, 225syl 17 . . . . . 6  |-  ( ph  ->  Rel  ( RR  _D  F ) )
227 resindm 5137 . . . . . 6  |-  ( Rel  ( RR  _D  F
)  ->  ( ( RR  _D  F )  |`  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) )  =  ( ( RR  _D  F )  |`  ( -oo (,) X ) ) )
228226, 227syl 17 . . . . 5  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) )  =  ( ( RR 
_D  F )  |`  ( -oo (,) X ) ) )
229 inss2 3659 . . . . . . 7  |-  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F ) )  C_  dom  ( RR  _D  F
)
230229a1i 11 . . . . . 6  |-  ( ph  ->  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) )  C_  dom  ( RR  _D  F
) )
231157, 230fssresd 5734 . . . . 5  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) : ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) --> RR )
232228, 231feq1dd 36797 . . . 4  |-  ( ph  ->  ( ( RR  _D  F )  |`  ( -oo (,) X ) ) : ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) --> RR )
233232, 117fssd 5722 . . 3  |-  ( ph  ->  ( ( RR  _D  F )  |`  ( -oo (,) X ) ) : ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) --> CC )
234 ioosscn 36876 . . . . 5  |-  ( -oo (,) X )  C_  CC
235 ssinss1 3666 . . . . 5  |-  ( ( -oo (,) X ) 
C_  CC  ->  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F ) )  C_  CC )
236234, 235ax-mp 5 . . . 4  |-  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F ) )  C_  CC
237236a1i 11 . . 3  |-  ( ph  ->  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) )  C_  CC )
238 3simpb 995 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  ( RR  _D  F
)  /\  k  e.  ZZ )  ->  ( ph  /\  k  e.  ZZ ) )
239 simp2 998 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  ( RR  _D  F
)  /\  k  e.  ZZ )  ->  x  e. 
dom  ( RR  _D  F ) )
240170adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  F : RR --> CC )
241177adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  T  e.  RR )
242 simplr 754 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  k  e.  ZZ )
243 simpr 459 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  x  e.  RR )
244 eleq1 2474 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
x  e.  RR  <->  y  e.  RR ) )
245244anbi2d 702 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  y  e.  RR ) ) )
246 oveq1 6284 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
x  +  T )  =  ( y  +  T ) )
247246fveq2d 5852 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( F `  ( x  +  T ) )  =  ( F `  (
y  +  T ) ) )
248 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
249247, 248eqeq12d 2424 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( y  +  T
) )  =  ( F `  y ) ) )
250245, 249imbi12d 318 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  y  e.  RR )  ->  ( F `  (
y  +  T ) )  =  ( F `
 y ) ) ) )
251250, 111chvarv 2041 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  T ) )  =  ( F `  y
) )
252251adant423 36782 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  /\  y  e.  RR )  ->  ( F `  ( y  +  T
) )  =  ( F `  y ) )
253240, 241, 242, 243, 252fperiodmul 36853 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  ( F `  ( x  +  ( k  x.  T ) ) )  =  ( F `  x ) )
254170, 178, 253, 185fperdvper 37064 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  dom  ( RR  _D  F ) )  -> 
( ( x  +  ( k  x.  T
) )  e.  dom  ( RR  _D  F
)  /\  ( ( RR  _D  F ) `  ( x  +  (
k  x.  T ) ) )  =  ( ( RR  _D  F
) `  x )
) )
255238, 239, 254syl2anc 659 . . . . . . 7  |-  ( (
ph  /\  x  e.  dom  ( RR  _D  F
)  /\  k  e.  ZZ )  ->  ( ( x  +  ( k  x.  T ) )  e.  dom  ( RR 
_D  F )  /\  ( ( RR  _D  F ) `  (
x  +  ( k  x.  T ) ) )  =  ( ( RR  _D  F ) `
 x ) ) )
256255simpld 457 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  ( RR  _D  F
)  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T ) )  e. 
dom  ( RR  _D  F ) )
257 oveq2 6285 . . . . . . . . . 10  |-  ( w  =  x  ->  (
pi  -  w )  =  ( pi  -  x ) )
258257oveq1d 6292 . . . . . . . . 9  |-  ( w  =  x  ->  (
( pi  -  w
)  /  T )  =  ( ( pi 
-  x )  /  T ) )
259258fveq2d 5852 . . . . . . . 8  |-  ( w  =  x  ->  ( |_ `  ( ( pi 
-  w )  /  T ) )  =  ( |_ `  (
( pi  -  x
)  /  T ) ) )
260259oveq1d 6292 . . . . . . 7  |-  ( w  =  x  ->  (
( |_ `  (
( pi  -  w
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( pi 
-  x )  /  T ) )  x.  T ) )
261260cbvmptv 4486 . . . . . 6  |-  ( w  e.  RR  |->  ( ( |_ `  ( ( pi  -  w )  /  T ) )  x.  T ) )  =  ( x  e.  RR  |->  ( ( |_
`  ( ( pi 
-  x )  /  T ) )  x.  T ) )
262 eqid 2402 . . . . . 6  |-  ( x  e.  RR  |->  ( x  +  ( ( w  e.  RR  |->  ( ( |_ `  ( ( pi  -  w )  /  T ) )  x.  T ) ) `
 x ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( w  e.  RR  |->  ( ( |_ `  ( ( pi  -  w )  /  T ) )  x.  T ) ) `
 x ) ) )
26361, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209fourierdlem41 37279 . . . . 5  |-  ( ph  ->  ( E. y  e.  RR  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  /\  E. y  e.  RR  ( X  <  y  /\  ( X (,) y )  C_  dom  ( RR  _D  F
) ) ) )
264263simpld 457 . . . 4  |-  ( ph  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  dom  ( RR 
_D  F ) ) )
265125cnfldtop 21581 . . . . . . . . 9  |-  ( TopOpen ` fld )  e.  Top
266265a1i 11 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  ->  ( TopOpen
` fld
)  e.  Top )
267236a1i 11 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  ->  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) )  C_  CC )
268 mnfxr 11375 . . . . . . . . . . . 12  |- -oo  e.  RR*
269268a1i 11 . . . . . . . . . . 11  |-  ( y  e.  RR  -> -oo  e.  RR* )
270 rexr 9668 . . . . . . . . . . . 12  |-  ( y  e.  RR  ->  y  e.  RR* )
271 mnflt 11385 . . . . . . . . . . . 12  |-  ( y  e.  RR  -> -oo  <  y )
272269, 270, 271xrltled 36810 . . . . . . . . . . 11  |-  ( y  e.  RR  -> -oo  <_  y )
273 iooss1 11616 . . . . . . . . . . 11  |-  ( ( -oo  e.  RR*  /\ -oo  <_  y )  ->  (
y (,) X ) 
C_  ( -oo (,) X ) )
274269, 272, 273syl2anc 659 . . . . . . . . . 10  |-  ( y  e.  RR  ->  (
y (,) X ) 
C_  ( -oo (,) X ) )
2752743ad2ant2 1019 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  ->  (
y (,) X ) 
C_  ( -oo (,) X ) )
276 simp3 999 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  ->  (
y (,) X ) 
C_  dom  ( RR  _D  F ) )
277275, 276ssind 3662 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  ->  (
y (,) X ) 
C_  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) )
278 unicntop 36787 . . . . . . . . 9  |-  CC  =  U. ( TopOpen ` fld )
279278lpss3 19936 . . . . . . . 8  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) )  C_  CC  /\  ( y (,) X
)  C_  ( ( -oo (,) X )  i^i 
dom  ( RR  _D  F ) ) )  ->  ( ( limPt `  ( TopOpen ` fld ) ) `  (
y (,) X ) )  C_  ( ( limPt `  ( TopOpen ` fld ) ) `  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) )
280266, 267, 277, 279syl3anc 1230 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  ->  (
( limPt `  ( TopOpen ` fld ) ) `  (
y (,) X ) )  C_  ( ( limPt `  ( TopOpen ` fld ) ) `  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) )
2812803adant3l 1226 . . . . . 6  |-  ( (
ph  /\  y  e.  RR  /\  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) ) )  -> 
( ( limPt `  ( TopOpen
` fld
) ) `  (
y (,) X ) )  C_  ( ( limPt `  ( TopOpen ` fld ) ) `  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) )
2822703ad2ant2 1019 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR  /\  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) ) )  -> 
y  e.  RR* )
283583ad2ant1 1018 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR  /\  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) ) )  ->  X  e.  RR )
284 simp3l 1025 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR  /\  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) ) )  -> 
y  <  X )
285125, 282, 283, 284lptioo2cn 37000 . . . . . 6  |-  ( (
ph  /\  y  e.  RR  /\  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) ) )  ->  X  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  (
y (,) X ) ) )
286281, 285sseldd 3442 . . . . 5  |-  ( (
ph  /\  y  e.  RR  /\  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) ) )  ->  X  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) )
287286rexlimdv3a 2897 . . . 4  |-  ( ph  ->  ( E. y  e.  RR  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) )  ->  X  e.  ( ( limPt `  ( TopOpen
` fld
) ) `  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) ) )
288264, 287mpd 15 . . 3  |-  ( ph  ->  X  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) )
289255simprd 461 . . . 4  |-  ( (
ph  /\  x  e.  dom  ( RR  _D  F
)  /\  k  e.  ZZ )  ->  ( ( RR  _D  F ) `
 ( x  +  ( k  x.  T
) ) )  =  ( ( RR  _D  F ) `  x
) )
290 oveq2 6285 . . . . . . . 8  |-  ( y  =  x  ->  (
pi  -  y )  =  ( pi  -  x ) )
291290oveq1d 6292 . . . . . . 7  |-  ( y  =  x  ->  (
( pi  -  y
)  /  T )  =  ( ( pi 
-  x )  /  T ) )
292291fveq2d 5852 . . . . . 6  |-  ( y  =  x  ->  ( |_ `  ( ( pi 
-  y )  /  T ) )  =  ( |_ `  (
( pi  -  x
)  /  T ) ) )
293292oveq1d 6292 . . . . 5  |-  ( y  =  x  ->  (
( |_ `  (
( pi  -  y
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( pi 
-  x )  /  T ) )  x.  T ) )
294293cbvmptv 4486 . . . 4  |-  ( y  e.  RR  |->  ( ( |_ `  ( ( pi  -  y )  /  T ) )  x.  T ) )  =  ( x  e.  RR  |->  ( ( |_
`  ( ( pi 
-  x )  /  T ) )  x.  T ) )
295 id 22 . . . . . 6  |-  ( z  =  x  ->  z  =  x )
296 fveq2 5848 . . . . . 6  |-  ( z  =  x  ->  (
( y  e.  RR  |->  ( ( |_ `  ( ( pi  -  y )