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

Theorem fourierdlem113 31956
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 6288 . . . . . . 7  |-  ( w  =  y  ->  (
w  mod  ( 2  x.  pi ) )  =  ( y  mod  ( 2  x.  pi ) ) )
32eqeq1d 2445 . . . . . 6  |-  ( w  =  y  ->  (
( w  mod  (
2  x.  pi ) )  =  0  <->  (
y  mod  ( 2  x.  pi ) )  =  0 ) )
4 oveq2 6289 . . . . . . . 8  |-  ( w  =  y  ->  (
( k  +  ( 1  /  2 ) )  x.  w )  =  ( ( k  +  ( 1  / 
2 ) )  x.  y ) )
54fveq2d 5860 . . . . . . 7  |-  ( w  =  y  ->  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  w ) )  =  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  y ) ) )
6 oveq1 6288 . . . . . . . . 9  |-  ( w  =  y  ->  (
w  /  2 )  =  ( y  / 
2 ) )
76fveq2d 5860 . . . . . . . 8  |-  ( w  =  y  ->  ( sin `  ( w  / 
2 ) )  =  ( sin `  (
y  /  2 ) ) )
87oveq2d 6297 . . . . . . 7  |-  ( w  =  y  ->  (
( 2  x.  pi )  x.  ( sin `  ( w  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
95, 8oveq12d 6299 . . . . . 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 3951 . . . . 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 4528 . . . 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 6289 . . . . . . . 8  |-  ( k  =  m  ->  (
2  x.  k )  =  ( 2  x.  m ) )
1312oveq1d 6296 . . . . . . 7  |-  ( k  =  m  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  m )  +  1 ) )
1413oveq1d 6296 . . . . . 6  |-  ( k  =  m  ->  (
( ( 2  x.  k )  +  1 )  /  ( 2  x.  pi ) )  =  ( ( ( 2  x.  m )  +  1 )  / 
( 2  x.  pi ) ) )
15 oveq1 6288 . . . . . . . . 9  |-  ( k  =  m  ->  (
k  +  ( 1  /  2 ) )  =  ( m  +  ( 1  /  2
) ) )
1615oveq1d 6296 . . . . . . . 8  |-  ( k  =  m  ->  (
( k  +  ( 1  /  2 ) )  x.  y )  =  ( ( m  +  ( 1  / 
2 ) )  x.  y ) )
1716fveq2d 5860 . . . . . . 7  |-  ( k  =  m  ->  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  y ) )  =  ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) ) )
1817oveq1d 6296 . . . . . 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 3946 . . . . 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 4524 . . . 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 2496 . . 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 4528 . 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 6288 . . . . . . . 8  |-  ( w  =  y  ->  (
w  +  ( j  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
2726eleq1d 2512 . . . . . . 7  |-  ( w  =  y  ->  (
( w  +  ( j  x.  T ) )  e.  ran  Q  <->  ( y  +  ( j  x.  T ) )  e.  ran  Q ) )
2827rexbidv 2954 . . . . . 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 3094 . . . . 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 3640 . . . 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 5859 . . 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 6291 . 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 6288 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
3433oveq2d 6297 . . . . . . . . . . 11  |-  ( k  =  j  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
3534eleq1d 2512 . . . . . . . . . 10  |-  ( k  =  j  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( j  x.  T ) )  e.  ran  Q ) )
3635cbvrexv 3071 . . . . . . . . 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 3084 . . . . . . 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 3640 . . . . . 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 6204 . . . . . 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 6297 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
w  +  ( k  x.  T ) )  =  ( w  +  ( j  x.  T
) ) )
4443eleq1d 2512 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  (
( w  +  ( k  x.  T ) )  e.  ran  Q  <->  ( w  +  ( j  x.  T ) )  e.  ran  Q ) )
4544cbvrexv 3071 . . . . . . . . . . . 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 3084 . . . . . . . . . 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 3640 . . . . . . . . 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 5859 . . . . . . . 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 6291 . . . . . . 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 6292 . . . . . 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 6203 . . . . . 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 6200 . . . 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 5547 . 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 22829 . . . . 5  |-  pi  e.  RR
6059renegcli 9885 . . . 4  |-  -u pi  e.  RR
6160a1i 11 . . 3  |-  ( ph  -> 
-u pi  e.  RR )
6259a1i 11 . . 3  |-  ( ph  ->  pi  e.  RR )
63 negpilt0 31416 . . . 4  |-  -u pi  <  0
6463a1i 11 . . 3  |-  ( ph  -> 
-u pi  <  0
)
65 pipos 22831 . . . 4  |-  0  <  pi
6665a1i 11 . . 3  |-  ( ph  ->  0  <  pi )
67 picn 22830 . . . . 5  |-  pi  e.  CC
68672timesi 10663 . . . 4  |-  ( 2  x.  pi )  =  ( pi  +  pi )
69 fourierdlem113.t . . . 4  |-  T  =  ( 2  x.  pi )
7067, 67subnegi 9903 . . . 4  |-  ( pi 
-  -u pi )  =  ( pi  +  pi )
7168, 69, 703eqtr4i 2482 . . 3  |-  T  =  ( pi  -  -u pi )
7223fourierdlem2 31845 . . . . . . . 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 16 . . . . . . 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 459 . . . . 5  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
76 elmapi 7442 . . . . 5  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
7775, 76syl 16 . . . 4  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
78 fzfid 12065 . . . 4  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
79 rnffi 31406 . . . 4  |-  ( ( Q : ( 0 ... M ) --> RR 
/\  ( 0 ... M )  e.  Fin )  ->  ran  Q  e.  Fin )
8077, 78, 79syl2anc 661 . . 3  |-  ( ph  ->  ran  Q  e.  Fin )
8123, 24, 25fourierdlem15 31858 . . . 4  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
82 frn 5727 . . . 4  |-  ( Q : ( 0 ... M ) --> ( -u pi [,] pi )  ->  ran  Q  C_  ( -u pi [,] pi ) )
8381, 82syl 16 . . 3  |-  ( ph  ->  ran  Q  C_  ( -u pi [,] pi ) )
8474simprd 463 . . . . 5  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
8584simplrd 31380 . . . 4  |-  ( ph  ->  ( Q `  M
)  =  pi )
86 ffun 5723 . . . . . 6  |-  ( Q : ( 0 ... M ) --> ( -u pi [,] pi )  ->  Fun  Q )
8781, 86syl 16 . . . . 5  |-  ( ph  ->  Fun  Q )
8824nnnn0d 10859 . . . . . . . 8  |-  ( ph  ->  M  e.  NN0 )
89 nn0uz 11126 . . . . . . . 8  |-  NN0  =  ( ZZ>= `  0 )
9088, 89syl6eleq 2541 . . . . . . 7  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
91 eluzfz2 11705 . . . . . . 7  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
9290, 91syl 16 . . . . . 6  |-  ( ph  ->  M  e.  ( 0 ... M ) )
93 fdm 5725 . . . . . . . 8  |-  ( Q : ( 0 ... M ) --> ( -u pi [,] pi )  ->  dom  Q  =  ( 0 ... M ) )
9481, 93syl 16 . . . . . . 7  |-  ( ph  ->  dom  Q  =  ( 0 ... M ) )
9594eqcomd 2451 . . . . . 6  |-  ( ph  ->  ( 0 ... M
)  =  dom  Q
)
9692, 95eleqtrd 2533 . . . . 5  |-  ( ph  ->  M  e.  dom  Q
)
97 fvelrn 6009 . . . . 5  |-  ( ( Fun  Q  /\  M  e.  dom  Q )  -> 
( Q `  M
)  e.  ran  Q
)
9887, 96, 97syl2anc 661 . . . 4  |-  ( ph  ->  ( Q `  M
)  e.  ran  Q
)
9985, 98eqeltrrd 2532 . . 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 2443 . . 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 6200 . . . . 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 2483 . . . . . 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 6204 . . . . . 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 5547 . . 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 2443 . . 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 31894 . 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 9552 . . . 4  |-  RR  C_  CC
113112a1i 11 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  CC )
114 ioossre 11597 . . . . . . 7  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
115114a1i 11 . . . . . 6  |-  ( ph  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR )
1161, 115fssresd 5742 . . . . 5  |-  ( ph  ->  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> RR )
117112a1i 11 . . . . 5  |-  ( ph  ->  RR  C_  CC )
118116, 117fssd 5730 . . . 4  |-  ( ph  ->  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC )
119118adantr 465 . . 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 5730 . . . . . . 7  |-  ( ph  ->  F : RR --> CC )
122121adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
123 ssid 3508 . . . . . . 7  |-  RR  C_  RR
124123a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  RR )
125 eqid 2443 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
126125tgioo2 21286 . . . . . . 7  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
127125, 126dvres 22293 . . . . . 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 1230 . . . . 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 5195 . . . 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 31503 . . . . . . 7  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
131130reseq2i 5260 . . . . . 6  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )  =  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
132131dmeqi 5194 . . . . 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 21375 . . . . 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 5725 . . . . 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 2488 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( RR  _D  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
139 dvcn 22302 . . 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 1232 . 2  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
141120, 113sstrd 3499 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
14277adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
143 fzofzp1 11891 . . . . . . 7  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
144143adantl 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
145142, 144ffvelrnd 6017 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
146145rexrd 9646 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
147 elfzofz 11825 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
148147adantl 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
149142, 148ffvelrnd 6017 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
15074simprrd 758 . . . . 5  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
151150r19.21bi 2812 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
152125, 146, 149, 151lptioo1cn 31606 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
153116adantr 465 . . . 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 22283 . . . . . . 7  |-  ( ph  ->  dom  ( RR  _D  F )  C_  RR )
156 dvfre 22332 . . . . . . . 8  |-  ( ( F : RR --> RR  /\  RR  C_  RR )  -> 
( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
1571, 154, 156syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
158 0re 9599 . . . . . . . . . 10  |-  0  e.  RR
15960, 158, 59lttri 9713 . . . . . . . . 9  |-  ( (
-u pi  <  0  /\  0  <  pi )  ->  -u pi  <  pi )
16063, 65, 159mp2an 672 . . . . . . . 8  |-  -u pi  <  pi
161160a1i 11 . . . . . . 7  |-  ( ph  -> 
-u pi  <  pi )
16284simplld 754 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
163134, 135syl 16 . . . . . . . 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 31574 . . . . . . 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 9646 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
167125, 166, 145, 151lptioo2cn 31605 . . . . . . . 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 31574 . . . . . . 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 465 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ZZ )  ->  F : RR
--> CC )
171 zre 10875 . . . . . . . . . . . 12  |-  ( k  e.  ZZ  ->  k  e.  RR )
172171adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  RR )
173 2re 10612 . . . . . . . . . . . . . . 15  |-  2  e.  RR
174173, 59remulcli 9613 . . . . . . . . . . . . . 14  |-  ( 2  x.  pi )  e.  RR
175174a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  x.  pi )  e.  RR )
17669, 175syl5eqel 2535 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  RR )
177176adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  RR )
178172, 177remulcld 9627 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  x.  T )  e.  RR )
179170adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  F : RR --> CC )
180177adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  T  e.  RR )
181 simplr 755 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  k  e.  ZZ )
182 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  t  e.  RR )
183111adant423 31379 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
184179, 180, 181, 182, 183fperiodmul 31458 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  t  e.  RR )  ->  ( F `  ( t  +  ( k  x.  T ) ) )  =  ( F `  t ) )
185 eqid 2443 . . . . . . . . . 10  |-  ( RR 
_D  F )  =  ( RR  _D  F
)
186170, 178, 184, 185fperdvper 31669 . . . . . . . . 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 804 . . . . . . . 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 459 . . . . . . 7  |-  ( ( ( ph  /\  t  e.  dom  ( RR  _D  F ) )  /\  k  e.  ZZ )  ->  ( t  +  ( k  x.  T ) )  e.  dom  ( RR  _D  F ) )
189187simprd 463 . . . . . . 7  |-  ( ( ( ph  /\  t  e.  dom  ( RR  _D  F ) )  /\  k  e.  ZZ )  ->  ( ( RR  _D  F ) `  (
t  +  ( k  x.  T ) ) )  =  ( ( RR  _D  F ) `
 t ) )
190 fveq2 5856 . . . . . . . . 9  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
191 oveq1 6288 . . . . . . . . . 10  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
192191fveq2d 5860 . . . . . . . . 9  |-  ( j  =  i  ->  ( Q `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
193190, 192oveq12d 6299 . . . . . . . 8  |-  ( j  =  i  ->  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
194193cbvmptv 4528 . . . . . . 7  |-  ( j  e.  ( 0..^ M )  |->  ( ( Q `
 j ) (,) ( Q `  (
j  +  1 ) ) ) )  =  ( i  e.  ( 0..^ M )  |->  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
195 eqid 2443 . . . . . . 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 31914 . . . . . 6  |-  ( ph  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
197196adantr 465 . . . . 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 1694 . . . . . . . . 9  |-  F/ t ( ph  /\  i  e.  ( 0..^ M ) )
199 nfra1 2824 . . . . . . . . 9  |-  F/ t A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z
200198, 199nfan 1914 . . . . . . . 8  |-  F/ t ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
201128, 131syl6eq 2500 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
202201fveq1d 5858 . . . . . . . . . . . . 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 5870 . . . . . . . . . . . . 13  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t )  =  ( ( RR 
_D  F ) `  t ) )
204202, 203sylan9eq 2504 . . . . . . . . . . . 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 5860 . . . . . . . . . . 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 714 . . . . . . . . . 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 755 . . . . . . . . . . 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 5285 . . . . . . . . . . . . . 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 725 . . . . . . . . . . . 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 461 . . . . . . . . . . . 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 3490 . . . . . . . . . . 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 2810 . . . . . . . . . . 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 661 . . . . . . . . . 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 4457 . . . . . . . . 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 434 . . . . . . . 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 2843 . . . . . . 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 434 . . . . . 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 2917 . . . . 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 31684 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =/=  (/) )
222119, 141, 152, 221, 125ellimciota 31574 . 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 31686 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =/=  (/) )
224119, 141, 167, 223, 125ellimciota 31574 . 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 5724 . . . . . . 7  |-  ( ( RR  _D  F ) : dom  ( RR 
_D  F ) --> RR 
->  Rel  ( RR  _D  F ) )
226157, 225syl 16 . . . . . 6  |-  ( ph  ->  Rel  ( RR  _D  F ) )
227 resindm 5308 . . . . . 6  |-  ( Rel  ( RR  _D  F
)  ->  ( ( RR  _D  F )  |`  ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) )  =  ( ( RR  _D  F )  |`  ( -oo (,) X ) ) )
228226, 227syl 16 . . . . 5  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) )  =  ( ( RR 
_D  F )  |`  ( -oo (,) X ) ) )
229 inss2 3704 . . . . . . 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 5742 . . . . 5  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( -oo (,) X )  i^i  dom  ( RR  _D  F ) ) ) : ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) --> RR )
232228, 231feq1dd 31396 . . . 4  |-  ( ph  ->  ( ( RR  _D  F )  |`  ( -oo (,) X ) ) : ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) --> RR )
233232, 117fssd 5730 . . 3  |-  ( ph  ->  ( ( RR  _D  F )  |`  ( -oo (,) X ) ) : ( ( -oo (,) X )  i^i  dom  ( RR  _D  F
) ) --> CC )
234 ioosscn 31481 . . . . 5  |-  ( -oo (,) X )  C_  CC
235 ssinss1 3711 . . . . 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 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  F : RR --> CC )
241177adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  T  e.  RR )
242 simplr 755 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  k  e.  ZZ )
243 simpr 461 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  x  e.  RR )
244 eleq1 2515 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
x  e.  RR  <->  y  e.  RR ) )
245244anbi2d 703 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  y  e.  RR ) ) )
246 oveq1 6288 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
x  +  T )  =  ( y  +  T ) )
247246fveq2d 5860 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( F `  ( x  +  T ) )  =  ( F `  (
y  +  T ) ) )
248 fveq2 5856 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
249247, 248eqeq12d 2465 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( y  +  T
) )  =  ( F `  y ) ) )
250245, 249imbi12d 320 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  y  e.  RR )  ->  ( F `  (
y  +  T ) )  =  ( F `
 y ) ) ) )
251250, 111chvarv 2000 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  T ) )  =  ( F `  y
) )
252251adant423 31379 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  /\  y  e.  RR )  ->  ( F `  ( y  +  T
) )  =  ( F `  y ) )
253240, 241, 242, 243, 252fperiodmul 31458 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  x  e.  RR )  ->  ( F `  ( x  +  ( k  x.  T ) ) )  =  ( F `  x ) )
254170, 178, 253, 185fperdvper 31669 . . . . . . . 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 661 . . . . . . 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 459 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  ( RR  _D  F
)  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T ) )  e. 
dom  ( RR  _D  F ) )
257 oveq2 6289 . . . . . . . . . 10  |-  ( w  =  x  ->  (
pi  -  w )  =  ( pi  -  x ) )
258257oveq1d 6296 . . . . . . . . 9  |-  ( w  =  x  ->  (
( pi  -  w
)  /  T )  =  ( ( pi 
-  x )  /  T ) )
259258fveq2d 5860 . . . . . . . 8  |-  ( w  =  x  ->  ( |_ `  ( ( pi 
-  w )  /  T ) )  =  ( |_ `  (
( pi  -  x
)  /  T ) ) )
260259oveq1d 6296 . . . . . . 7  |-  ( w  =  x  ->  (
( |_ `  (
( pi  -  w
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( pi 
-  x )  /  T ) )  x.  T ) )
261260cbvmptv 4528 . . . . . 6  |-  ( w  e.  RR  |->  ( ( |_ `  ( ( pi  -  w )  /  T ) )  x.  T ) )  =  ( x  e.  RR  |->  ( ( |_
`  ( ( pi 
-  x )  /  T ) )  x.  T ) )
262 eqid 2443 . . . . . 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 31884 . . . . 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 459 . . . 4  |-  ( ph  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  dom  ( RR 
_D  F ) ) )
265125cnfldtop 21269 . . . . . . . . 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 11334 . . . . . . . . . . . 12  |- -oo  e.  RR*
269268a1i 11 . . . . . . . . . . 11  |-  ( y  e.  RR  -> -oo  e.  RR* )
270 rexr 9642 . . . . . . . . . . . 12  |-  ( y  e.  RR  ->  y  e.  RR* )
271 mnflt 11344 . . . . . . . . . . . 12  |-  ( y  e.  RR  -> -oo  <  y )
272269, 270, 271xrltled 31410 . . . . . . . . . . 11  |-  ( y  e.  RR  -> -oo  <_  y )
273 iooss1 11575 . . . . . . . . . . 11  |-  ( ( -oo  e.  RR*  /\ -oo  <_  y )  ->  (
y (,) X ) 
C_  ( -oo (,) X ) )
274269, 272, 273syl2anc 661 . . . . . . . . . 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 3707 . . . . . . . 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 31385 . . . . . . . . 9  |-  CC  =  U. ( TopOpen ` fld )
279278lpss3 19623 . . . . . . . 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 1229 . . . . . . 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 1225 . . . . . 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 31605 . . . . . 6  |-  ( (
ph  /\  y  e.  RR  /\  ( y  < 
X  /\  ( y (,) X )  C_  dom  ( RR  _D  F
) ) )  ->  X  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  (
y (,) X ) ) )
286281, 285sseldd 3490 . . . . 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 2937 . . . 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 463 . . . 4  |-  ( (
ph  /\  x  e.  dom  ( RR  _D  F
)  /\  k  e.  ZZ )  ->  ( ( RR  _D  F ) `
 ( x  +  ( k  x.  T
) ) )  =  ( ( RR  _D  F ) `  x
) )
290 oveq2 6289 . . . . . . . 8  |-  ( y  =  x  ->  (
pi  -  y )  =  ( pi  -  x ) )
291290oveq1d 6296 . . . . . . 7  |-  ( y  =  x  ->  (
( pi  -  y
)  /  T )  =  ( ( pi 
-  x )  /  T ) )
292291fveq2d 5860 . . . . . 6  |-  ( y  =  x  ->  ( |_ `  ( ( pi 
-  y )  /  T ) )  =  ( |_ `  (
( pi  -  x
)  /  T ) ) )
293292oveq1d 6296 . . . . 5  |-  ( y  =  x  ->  (
( |_ `  (
( pi  -  y
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( pi 
-  x )  /  T ) )  x.  T ) )
294293cbvmptv 4528 . . . 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 5856 . . . . . 6  |-  ( z  =  x  ->  (
( y  e.  RR  |->  ( ( |_ `  ( ( pi  -  y )