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

Theorem fourierdlem92 38002
Description: The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by its period  T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem92.a  |-  ( ph  ->  A  e.  RR )
fourierdlem92.b  |-  ( ph  ->  B  e.  RR )
fourierdlem92.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem92.m  |-  ( ph  ->  M  e.  NN )
fourierdlem92.t  |-  ( ph  ->  T  e.  RR )
fourierdlem92.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem92.fper  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
fourierdlem92.s  |-  S  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  +  T
) )
fourierdlem92.h  |-  H  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( A  +  T
)  /\  ( p `  m )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ m ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) ) } )
fourierdlem92.f  |-  ( ph  ->  F : RR --> CC )
fourierdlem92.cncf  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem92.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem92.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
Assertion
Ref Expression
fourierdlem92  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
Distinct variable groups:    A, i, m, p    x, A, i    B, i, m, p    x, B    i, F, x    x, L    i, M, x    m, M, p    Q, i, x    Q, p    x, R    S, i, x    S, p    T, i, x    T, m, p    ph, i, x
Allowed substitution hints:    ph( m, p)    P( x, i, m, p)    Q( m)    R( i, m, p)    S( m)    F( m, p)    H( x, i, m, p)    L( i, m, p)

Proof of Theorem fourierdlem92
Dummy variables  y  w  z  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem92.a . . . 4  |-  ( ph  ->  A  e.  RR )
21adantr 466 . . 3  |-  ( (
ph  /\  0  <  T )  ->  A  e.  RR )
3 fourierdlem92.b . . . 4  |-  ( ph  ->  B  e.  RR )
43adantr 466 . . 3  |-  ( (
ph  /\  0  <  T )  ->  B  e.  RR )
5 fourierdlem92.p . . 3  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
6 fourierdlem92.m . . . 4  |-  ( ph  ->  M  e.  NN )
76adantr 466 . . 3  |-  ( (
ph  /\  0  <  T )  ->  M  e.  NN )
8 fourierdlem92.t . . . . 5  |-  ( ph  ->  T  e.  RR )
98adantr 466 . . . 4  |-  ( (
ph  /\  0  <  T )  ->  T  e.  RR )
10 simpr 462 . . . 4  |-  ( (
ph  /\  0  <  T )  ->  0  <  T )
119, 10elrpd 11345 . . 3  |-  ( (
ph  /\  0  <  T )  ->  T  e.  RR+ )
12 fourierdlem92.q . . . 4  |-  ( ph  ->  Q  e.  ( P `
 M ) )
1312adantr 466 . . 3  |-  ( (
ph  /\  0  <  T )  ->  Q  e.  ( P `  M ) )
14 fourierdlem92.fper . . . 4  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
1514adantlr 719 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  x  e.  ( A [,] B
) )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
16 fveq2 5881 . . . . 5  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
1716oveq1d 6320 . . . 4  |-  ( j  =  i  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 i )  +  T ) )
1817cbvmptv 4516 . . 3  |-  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j )  +  T ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( Q `
 i )  +  T ) )
19 fourierdlem92.f . . . 4  |-  ( ph  ->  F : RR --> CC )
2019adantr 466 . . 3  |-  ( (
ph  /\  0  <  T )  ->  F : RR
--> CC )
21 fourierdlem92.cncf . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
2221adantlr 719 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
23 fourierdlem92.r . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
2423adantlr 719 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
25 fourierdlem92.l . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
2625adantlr 719 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
27 eqeq1 2426 . . . . 5  |-  ( y  =  x  ->  (
y  =  ( Q `
 i )  <->  x  =  ( Q `  i ) ) )
28 eqeq1 2426 . . . . . 6  |-  ( y  =  x  ->  (
y  =  ( Q `
 ( i  +  1 ) )  <->  x  =  ( Q `  ( i  +  1 ) ) ) )
29 fveq2 5881 . . . . . 6  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
3028, 29ifbieq2d 3936 . . . . 5  |-  ( y  =  x  ->  if ( y  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  y ) )  =  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
3127, 30ifbieq2d 3936 . . . 4  |-  ( y  =  x  ->  if ( y  =  ( Q `  i ) ,  R ,  if ( y  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  y ) ) )  =  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
3231cbvmptv 4516 . . 3  |-  ( y  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  |->  if ( y  =  ( Q `
 i ) ,  R ,  if ( y  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 y ) ) ) )  =  ( x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
33 eqid 2422 . . 3  |-  ( x  e.  ( ( ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  +  T ) ) `  i ) [,] ( ( j  e.  ( 0 ... M )  |->  ( ( Q `  j )  +  T ) ) `
 ( i  +  1 ) ) ) 
|->  ( ( y  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  if ( y  =  ( Q `  i ) ,  R ,  if ( y  =  ( Q `  (
i  +  1 ) ) ,  L , 
( F `  y
) ) ) ) `
 ( x  -  T ) ) )  =  ( x  e.  ( ( ( j  e.  ( 0 ... M )  |->  ( ( Q `  j )  +  T ) ) `
 i ) [,] ( ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  +  T ) ) `  ( i  +  1 ) ) )  |->  ( ( y  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( y  =  ( Q `  i
) ,  R ,  if ( y  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  y ) ) ) ) `  ( x  -  T
) ) )
342, 4, 5, 7, 11, 13, 15, 18, 20, 22, 24, 26, 32, 33fourierdlem81 37991 . 2  |-  ( (
ph  /\  0  <  T )  ->  S. (
( A  +  T
) [,] ( B  +  T ) ) ( F `  x
)  _d x  =  S. ( A [,] B ) ( F `
 x )  _d x )
35 simpr 462 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  T  =  0 )
3635oveq2d 6321 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  T )  =  ( A  + 
0 ) )
371recnd 9676 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
3837adantr 466 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  A  e.  CC )
3938addid1d 9840 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  0 )  =  A )
4036, 39eqtrd 2463 . . . . . 6  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  T )  =  A )
4135oveq2d 6321 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  T )  =  ( B  + 
0 ) )
423recnd 9676 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
4342adantr 466 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  B  e.  CC )
4443addid1d 9840 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  0 )  =  B )
4541, 44eqtrd 2463 . . . . . 6  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  T )  =  B )
4640, 45oveq12d 6323 . . . . 5  |-  ( (
ph  /\  T  = 
0 )  ->  (
( A  +  T
) [,] ( B  +  T ) )  =  ( A [,] B ) )
4746itgeq1d 37773 . . . 4  |-  ( (
ph  /\  T  = 
0 )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
4847adantlr 719 . . 3  |-  ( ( ( ph  /\  -.  0  <  T )  /\  T  =  0 )  ->  S. ( ( A  +  T ) [,] ( B  +  T ) ) ( F `  x )  _d x  =  S. ( A [,] B
) ( F `  x )  _d x )
49 simpll 758 . . . 4  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ph )
50 simpr 462 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  T  =  0 )
51 simplr 760 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  0  <  T )
52 ioran 492 . . . . . . 7  |-  ( -.  ( T  =  0  \/  0  <  T
)  <->  ( -.  T  =  0  /\  -.  0  <  T ) )
5350, 51, 52sylanbrc 668 . . . . . 6  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  ( T  =  0  \/  0  <  T ) )
5449, 8syl 17 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  T  e.  RR )
55 0red 9651 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  0  e.  RR )
5654, 55lttrid 9780 . . . . . 6  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ( T  <  0  <->  -.  ( T  =  0  \/  0  <  T ) ) )
5753, 56mpbird 235 . . . . 5  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  T  <  0 )
5854lt0neg1d 10190 . . . . 5  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ( T  <  0  <->  0  <  -u T
) )
5957, 58mpbid 213 . . . 4  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  0  <  -u T )
601, 8readdcld 9677 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  +  T
)  e.  RR )
6160recnd 9676 . . . . . . . . . . 11  |-  ( ph  ->  ( A  +  T
)  e.  CC )
628recnd 9676 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  CC )
6361, 62negsubd 9999 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  +  T )  +  -u T )  =  ( ( A  +  T
)  -  T ) )
6437, 62pncand 9994 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
6563, 64eqtrd 2463 . . . . . . . . 9  |-  ( ph  ->  ( ( A  +  T )  +  -u T )  =  A )
663, 8readdcld 9677 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  +  T
)  e.  RR )
6766recnd 9676 . . . . . . . . . . 11  |-  ( ph  ->  ( B  +  T
)  e.  CC )
6867, 62negsubd 9999 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  +  T )  +  -u T )  =  ( ( B  +  T
)  -  T ) )
6942, 62pncand 9994 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  +  T )  -  T
)  =  B )
7068, 69eqtrd 2463 . . . . . . . . 9  |-  ( ph  ->  ( ( B  +  T )  +  -u T )  =  B )
7165, 70oveq12d 6323 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  +  T )  + 
-u T ) [,] ( ( B  +  T )  +  -u T ) )  =  ( A [,] B
) )
7271eqcomd 2430 . . . . . . 7  |-  ( ph  ->  ( A [,] B
)  =  ( ( ( A  +  T
)  +  -u T
) [,] ( ( B  +  T )  +  -u T ) ) )
7372itgeq1d 37773 . . . . . 6  |-  ( ph  ->  S. ( A [,] B ) ( F `
 x )  _d x  =  S. ( ( ( A  +  T )  +  -u T ) [,] (
( B  +  T
)  +  -u T
) ) ( F `
 x )  _d x )
7473adantr 466 . . . . 5  |-  ( (
ph  /\  0  <  -u T )  ->  S. ( A [,] B ) ( F `  x
)  _d x  =  S. ( ( ( A  +  T )  +  -u T ) [,] ( ( B  +  T )  +  -u T ) ) ( F `  x )  _d x )
751adantr 466 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  A  e.  RR )
768adantr 466 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  T  e.  RR )
7775, 76readdcld 9677 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  ( A  +  T )  e.  RR )
783adantr 466 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  B  e.  RR )
7978, 76readdcld 9677 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  ( B  +  T )  e.  RR )
80 eqid 2422 . . . . . 6  |-  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  +  T )  /\  (
p `  m )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  +  T )  /\  (
p `  m )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
816adantr 466 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  M  e.  NN )
8276renegcld 10053 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  -u T  e.  RR )
83 simpr 462 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  0  <  -u T )
8482, 83elrpd 11345 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  -u T  e.  RR+ )
855fourierdlem2 37911 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
866, 85syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
8712, 86mpbid 213 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
8887simpld 460 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
89 elmapi 7504 . . . . . . . . . . . . . . 15  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
9088, 89syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
9190ffvelrnda 6037 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
928adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  T  e.  RR )
9391, 92readdcld 9677 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  +  T )  e.  RR )
94 fourierdlem92.s . . . . . . . . . . . 12  |-  S  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  +  T
) )
9593, 94fmptd 6061 . . . . . . . . . . 11  |-  ( ph  ->  S : ( 0 ... M ) --> RR )
96 reex 9637 . . . . . . . . . . . . 13  |-  RR  e.  _V
9796a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  _V )
98 ovex 6333 . . . . . . . . . . . . 13  |-  ( 0 ... M )  e. 
_V
9998a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... M
)  e.  _V )
10097, 99elmapd 7497 . . . . . . . . . . 11  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
S : ( 0 ... M ) --> RR ) )
10195, 100mpbird 235 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... M ) ) )
10294a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  S  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) ) )
103 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
104103oveq1d 6320 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
105104adantl 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
106 0zd 10956 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  ZZ )
1076nnzd 11046 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ZZ )
108106, 107, 1063jca 1185 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )
)
109 0le0 10706 . . . . . . . . . . . . . . . 16  |-  0  <_  0
110109a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  0 )
111 nnnn0 10883 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  NN  ->  M  e.  NN0 )
112111nn0ge0d 10935 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  ->  0  <_  M )
1136, 112syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  M )
114108, 110, 113jca32 537 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
115 elfz2 11798 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
116114, 115sylibr 215 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  ( 0 ... M ) )
11790, 116ffvelrnd 6038 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  0
)  e.  RR )
118117, 8readdcld 9677 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  e.  RR )
119102, 105, 116, 118fvmptd 5970 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  0
)  =  ( ( Q `  0 )  +  T ) )
120 simprll 770 . . . . . . . . . . . . . 14  |-  ( ( Q  e.  ( RR 
^m  ( 0 ... M ) )  /\  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  0
)  =  A )
12187, 120syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q `  0
)  =  A )
122121oveq1d 6320 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  =  ( A  +  T ) )
123119, 122eqtrd 2463 . . . . . . . . . . 11  |-  ( ph  ->  ( S `  0
)  =  ( A  +  T ) )
124 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
125124oveq1d 6320 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
126125adantl 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
1276nnnn0d 10932 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN0 )
128 nn0uz 11200 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
129127, 128syl6eleq 2517 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
130 eluzfz2 11814 . . . . . . . . . . . . . 14  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
131129, 130syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( 0 ... M ) )
13290, 131ffvelrnd 6038 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  M
)  e.  RR )
133132, 8readdcld 9677 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q `  M )  +  T
)  e.  RR )
134102, 126, 131, 133fvmptd 5970 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  M
)  =  ( ( Q `  M )  +  T ) )
135 simprlr 771 . . . . . . . . . . . . . 14  |-  ( ( Q  e.  ( RR 
^m  ( 0 ... M ) )  /\  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  M
)  =  B )
13687, 135syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q `  M
)  =  B )
137136oveq1d 6320 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q `  M )  +  T
)  =  ( B  +  T ) )
138134, 137eqtrd 2463 . . . . . . . . . . 11  |-  ( ph  ->  ( S `  M
)  =  ( B  +  T ) )
139123, 138jca 534 . . . . . . . . . 10  |-  ( ph  ->  ( ( S ` 
0 )  =  ( A  +  T )  /\  ( S `  M )  =  ( B  +  T ) ) )
14090adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
141 elfzofz 11942 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
142141adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
143140, 142ffvelrnd 6038 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
144 fzofzp1 12014 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
145144adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
146140, 145ffvelrnd 6038 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
1478adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  RR )
14887simprrd 765 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
149148r19.21bi 2791 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
150143, 146, 147, 149ltadd1dd 10231 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) )
151143, 147readdcld 9677 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
15294fvmpt2 5973 . . . . . . . . . . . . 13  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  +  T
)  e.  RR )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
153142, 151, 152syl2anc 665 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
15494, 18eqtr4i 2454 . . . . . . . . . . . . . 14  |-  S  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  +  T
) )
155154a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  +  T ) ) )
156 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
157156oveq1d 6320 . . . . . . . . . . . . . 14  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
158157adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
159146, 147readdcld 9677 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
160155, 158, 145, 159fvmptd 5970 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  +  T ) )
161150, 153, 1603brtr4d 4454 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  <  ( S `  ( i  +  1 ) ) )
162161ralrimiva 2836 . . . . . . . . . 10  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( S `  i )  <  ( S `  ( i  +  1 ) ) )
163101, 139, 162jca32 537 . . . . . . . . 9  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( S `  0 )  =  ( A  +  T )  /\  ( S `  M )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ M ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) )
164 fourierdlem92.h . . . . . . . . . . 11  |-  H  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( A  +  T
)  /\  ( p `  m )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ m ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) ) } )
165164fourierdlem2 37911 . . . . . . . . . 10  |-  ( M  e.  NN  ->  ( S  e.  ( H `  M )  <->  ( S  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( S `  0 )  =  ( A  +  T )  /\  ( S `  M )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ M ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) ) )
1666, 165syl 17 . . . . . . . . 9  |-  ( ph  ->  ( S  e.  ( H `  M )  <-> 
( S  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( S `  0 )  =  ( A  +  T )  /\  ( S `  M )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ M ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) ) )
167163, 166mpbird 235 . . . . . . . 8  |-  ( ph  ->  S  e.  ( H `
 M ) )
168164fveq1i 5882 . . . . . . . 8  |-  ( H `
 M )  =  ( ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  +  T )  /\  (
p `  m )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } ) `
 M )
169167, 168syl6eleq 2517 . . . . . . 7  |-  ( ph  ->  S  e.  ( ( m  e.  NN  |->  { p  e.  ( RR 
^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( A  +  T
)  /\  ( p `  m )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ m ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) ) } ) `  M ) )
170169adantr 466 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  S  e.  ( ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  +  T )  /\  (
p `  m )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } ) `
 M ) )
17160adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR )
17266adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR )
173 simpr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
174 eliccre 37552 . . . . . . . . . . . 12  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  ->  x  e.  RR )
175171, 172, 173, 174syl3anc 1264 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  RR )
176175recnd 9676 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  CC )
17762negcld 9980 . . . . . . . . . . 11  |-  ( ph  -> 
-u T  e.  CC )
178177adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  -u T  e.  CC )
179176, 178addcld 9669 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  CC )
180 simpl 458 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ph )
1811adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  e.  RR )
1823adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  B  e.  RR )
1838renegcld 10053 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u T  e.  RR )
184183adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  -u T  e.  RR )
185175, 184readdcld 9677 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  RR )
18663, 64eqtr2d 2464 . . . . . . . . . . . . 13  |-  ( ph  ->  A  =  ( ( A  +  T )  +  -u T ) )
187186adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  =  ( ( A  +  T )  + 
-u T ) )
188171rexrd 9697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR* )
189172rexrd 9697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR* )
190 iccgelb 11698 . . . . . . . . . . . . . 14  |-  ( ( ( A  +  T
)  e.  RR*  /\  ( B  +  T )  e.  RR*  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
191188, 189, 173, 190syl3anc 1264 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
192171, 175, 184, 191leadd1dd 10234 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( A  +  T
)  +  -u T
)  <_  ( x  +  -u T ) )
193187, 192eqbrtrd 4444 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  <_  ( x  +  -u T ) )
194 iccleub 11697 . . . . . . . . . . . . . 14  |-  ( ( ( A  +  T
)  e.  RR*  /\  ( B  +  T )  e.  RR*  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
195188, 189, 173, 194syl3anc 1264 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
196175, 172, 184, 195leadd1dd 10234 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  <_  ( ( B  +  T )  +  -u T ) )
197172recnd 9676 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  CC )
19862adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  T  e.  CC )
199197, 198negsubd 9999 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  +  -u T
)  =  ( ( B  +  T )  -  T ) )
20069adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  -  T )  =  B )
201199, 200eqtrd 2463 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  +  -u T
)  =  B )
202196, 201breqtrd 4448 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  <_  B )
203181, 182, 185, 193, 202eliccd 37550 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  ( A [,] B ) )
204180, 203jca 534 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( ph  /\  ( x  +  -u T )  e.  ( A [,] B ) ) )
205 eleq1 2495 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  (
y  e.  ( A [,] B )  <->  ( x  +  -u T )  e.  ( A [,] B
) ) )
206205anbi2d 708 . . . . . . . . . . 11  |-  ( y  =  ( x  +  -u T )  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  ( x  +  -u T )  e.  ( A [,] B ) ) ) )
207 oveq1 6312 . . . . . . . . . . . . 13  |-  ( y  =  ( x  +  -u T )  ->  (
y  +  T )  =  ( ( x  +  -u T )  +  T ) )
208207fveq2d 5885 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  ( F `  ( y  +  T ) )  =  ( F `  (
( x  +  -u T )  +  T
) ) )
209 fveq2 5881 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  ( F `  y )  =  ( F `  ( x  +  -u T
) ) )
210208, 209eqeq12d 2444 . . . . . . . . . . 11  |-  ( y  =  ( x  +  -u T )  ->  (
( F `  (
y  +  T ) )  =  ( F `
 y )  <->  ( F `  ( ( x  +  -u T )  +  T
) )  =  ( F `  ( x  +  -u T ) ) ) )
211206, 210imbi12d 321 . . . . . . . . . 10  |-  ( y  =  ( x  +  -u T )  ->  (
( ( ph  /\  y  e.  ( A [,] B ) )  -> 
( F `  (
y  +  T ) )  =  ( F `
 y ) )  <-> 
( ( ph  /\  ( x  +  -u T
)  e.  ( A [,] B ) )  ->  ( F `  ( ( x  +  -u T )  +  T
) )  =  ( F `  ( x  +  -u T ) ) ) ) )
212 eleq1 2495 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
x  e.  ( A [,] B )  <->  y  e.  ( A [,] B ) ) )
213212anbi2d 708 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  y  e.  ( A [,] B ) ) ) )
214 oveq1 6312 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
x  +  T )  =  ( y  +  T ) )
215214fveq2d 5885 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( F `  ( x  +  T ) )  =  ( F `  (
y  +  T ) ) )
216 fveq2 5881 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
217215, 216eqeq12d 2444 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( y  +  T
) )  =  ( F `  y ) ) )
218213, 217imbi12d 321 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  ( A [,] B ) )  -> 
( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  y  e.  ( A [,] B ) )  -> 
( F `  (
y  +  T ) )  =  ( F `
 y ) ) ) )
219218, 14chvarv 2072 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  ( y  +  T
) )  =  ( F `  y ) )
220211, 219vtoclg 3139 . . . . . . . . 9  |-  ( ( x  +  -u T
)  e.  CC  ->  ( ( ph  /\  (
x  +  -u T
)  e.  ( A [,] B ) )  ->  ( F `  ( ( x  +  -u T )  +  T
) )  =  ( F `  ( x  +  -u T ) ) ) )
221179, 204, 220sylc 62 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( (
x  +  -u T
)  +  T ) )  =  ( F `
 ( x  +  -u T ) ) )
222176, 198negsubd 9999 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  =  ( x  -  T ) )
223222oveq1d 6320 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  +  T
)  =  ( ( x  -  T )  +  T ) )
224176, 198npcand 9997 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  -  T
)  +  T )  =  x )
225223, 224eqtrd 2463 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  +  T
)  =  x )
226225fveq2d 5885 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( (
x  +  -u T
)  +  T ) )  =  ( F `
 x ) )
227221, 226eqtr3d 2465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( x  +  -u T ) )  =  ( F `  x ) )
228227adantlr 719 . . . . . 6  |-  ( ( ( ph  /\  0  <  -u T )  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  -> 
( F `  (
x  +  -u T
) )  =  ( F `  x ) )
229 fveq2 5881 . . . . . . . 8  |-  ( j  =  i  ->  ( S `  j )  =  ( S `  i ) )
230229oveq1d 6320 . . . . . . 7  |-  ( j  =  i  ->  (
( S `  j
)  +  -u T
)  =  ( ( S `  i )  +  -u T ) )
231230cbvmptv 4516 . . . . . 6  |-  ( j  e.  ( 0 ... M )  |->  ( ( S `  j )  +  -u T ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( S `
 i )  + 
-u T ) )
23219adantr 466 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  F : RR --> CC )
23319adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
234 ioossre 11703 . . . . . . . . . . 11  |-  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  C_  RR
235234a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  C_  RR )
236233, 235feqresmpt 5935 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  =  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) ) )
237153, 160oveq12d 6323 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  =  ( ( ( Q `  i )  +  T
) (,) ( ( Q `  ( i  +  1 ) )  +  T ) ) )
238143, 146, 147iooshift 37572 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  T ) (,) ( ( Q `  ( i  +  1 ) )  +  T
) )  =  {
w  e.  CC  |  E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )
239237, 238eqtrd 2463 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  =  {
w  e.  CC  |  E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )
240239mpteq1d 4505 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  =  ( x  e.  {
w  e.  CC  |  E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } 
|->  ( F `  x
) ) )
241 simpll 758 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ph )
242 simplr 760 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  i  e.  ( 0..^ M ) )
243238eleq2d 2492 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) )  <->  x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) } ) )
244243biimpar 487 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )
245143rexrd 9697 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
2462453adant3 1025 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  e.  RR* )
247146rexrd 9697 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
2482473adant3 1025 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
249 elioore 11673 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( ( Q `  i )  +  T ) (,) ( ( Q `  ( i  +  1 ) )  +  T
) )  ->  x  e.  RR )
250249adantl 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  x  e.  RR )
2518adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  T  e.  RR )
252250, 251resubcld 10054 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  (
x  -  T )  e.  RR )
2532523adant2 1024 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  RR )
254143recnd 9676 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
25562adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  CC )
256254, 255pncand 9994 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  =  ( Q `  i ) )
257256eqcomd 2430 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
2582573adant3 1025 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
2591513adant3 1025 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
2602503adant2 1024 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  e.  RR )
26183ad2ant1 1026 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  T  e.  RR )
262151rexrd 9697 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR* )
2632623adant3 1025 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  e.  RR* )
264159rexrd 9697 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR* )
2652643adant3 1025 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR* )
266 simp3 1007 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  e.  ( ( ( Q `  i )  +  T
) (,) ( ( Q `  ( i  +  1 ) )  +  T ) ) )
267 ioogtlb 37541 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( Q `  i )  +  T
)  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  +  T )  e.  RR*  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  (
( Q `  i
)  +  T )  <  x )
268263, 265, 266, 267syl3anc 1264 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  <  x
)
269259, 260, 261, 268ltsub1dd 10232 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  <  (
x  -  T ) )
270258, 269eqbrtrd 4444 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  <  (
x  -  T ) )
2711593adant3 1025 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
272 iooltub 37559 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( Q `  i )  +  T
)  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  +  T )  e.  RR*  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  x  <  ( ( Q `  ( i  +  1 ) )  +  T
) )
273263, 265, 266, 272syl3anc 1264 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  <  (
( Q `  (
i  +  1 ) )  +  T ) )
274260, 271, 261, 273ltsub1dd 10232 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  (
( ( Q `  ( i  +  1 ) )  +  T
)  -  T ) )
275146recnd 9676 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
276275, 255pncand 9994 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
2772763adant3 1025 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
278274, 277breqtrd 4448 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  ( Q `  ( i  +  1 ) ) )
279246, 248, 253, 270, 278eliood 37544 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
280241, 242, 244, 279syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( x  -  T )  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
281 fvres 5895 . . . . . . . . . . . 12  |-  ( ( x  -  T )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( x  -  T ) )  =  ( F `  ( x  -  T
) ) )
282280, 281syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  ( x  -  T
) )  =  ( F `  ( x  -  T ) ) )
283241, 244, 252syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( x  -  T )  e.  RR )
28413ad2ant1 1026 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  e.  RR )
28533ad2ant1 1026 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  B  e.  RR )
28664eqcomd 2430 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  =  ( ( A  +  T )  -  T ) )
2872863ad2ant1 1026 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  =  ( ( A  +  T
)  -  T ) )
288603ad2ant1 1026 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  e.  RR )
2891adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR )
2901rexrd 9697 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  e.  RR* )
291290adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
2923rexrd 9697 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  RR* )
293292adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
2945, 6, 12fourierdlem15 37924 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
295294adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
296295, 142ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( A [,] B ) )
297 iccgelb 11698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 i )  e.  ( A [,] B
) )  ->  A  <_  ( Q `  i
) )
298291, 293, 296, 297syl3anc 1264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  <_  ( Q `  i )
)
299289, 143, 147, 298leadd1dd 10234 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A  +  T )  <_  (
( Q `  i
)  +  T ) )
3002993adant3 1025 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  <_  (
( Q `  i
)  +  T ) )
301288, 259, 260, 300, 268lelttrd 9800 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  <  x
)
302288, 260, 261, 301ltsub1dd 10232 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( A  +  T )  -  T )  <  (
x  -  T ) )
303287, 302eqbrtrd 4444 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  <  (
x  -  T ) )
304284, 253, 303ltled 9790 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  <_  (
x  -  T ) )
3051463adant3 1025 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
306295, 145ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
307 iccleub 11697 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 ( i  +  1 ) )  e.  ( A [,] B
) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
308291, 293, 306, 307syl3anc 1264 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  <_  B
)
3093083adant3 1025 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  <_  B
)
310253, 305, 285, 278, 309ltletrd 9802 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  B
)
311253, 285, 310ltled 9790 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <_  B
)
312284, 285, 253, 304, 311eliccd 37550 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  ( A [,] B ) )
313241, 242, 244, 312syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( x  -  T )  e.  ( A [,] B ) )
314241, 313jca 534 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( ph  /\  ( x  -  T
)  e.  ( A [,] B ) ) )
315 eleq1 2495 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  (
y  e.  ( A [,] B )  <->  ( x  -  T )  e.  ( A [,] B ) ) )
316315anbi2d 708 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  T )  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  ( x  -  T
)  e.  ( A [,] B ) ) ) )
317 oveq1 6312 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  -  T )  ->  (
y  +  T )  =  ( ( x  -  T )  +  T ) )
318317fveq2d 5885 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  ( F `  ( y  +  T ) )  =  ( F `  (
( x  -  T
)  +  T ) ) )
319 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  ( F `  y )  =  ( F `  ( x  -  T
) ) )
320318, 319eqeq12d 2444 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  T )  ->  (
( F `  (
y  +  T ) )  =  ( F `
 y )  <->  ( F `  ( ( x  -  T )  +  T
) )  =  ( F `  ( x  -  T ) ) ) )
321316, 320imbi12d 321 . . . . . . . . . . . . 13  |-  ( y  =  ( x  -  T )  ->  (
( ( ph  /\  y  e.  ( A [,] B ) )  -> 
( F `  (
y  +  T ) )  =  ( F `
 y ) )  <-> 
( ( ph  /\  ( x  -  T
)  e.  ( A [,] B ) )  ->  ( F `  ( ( x  -  T )  +  T
) )  =  ( F `  ( x  -  T ) ) ) ) )
322321, 219vtoclg 3139 . . . . . . . . . . . 12  |-  ( ( x  -  T )  e.  RR  ->  (
( ph  /\  (
x  -  T )  e.  ( A [,] B ) )  -> 
( F `  (
( x  -  T
)  +  T ) )  =  ( F `
 ( x  -  T ) ) ) )
323283, 314, 322sylc 62 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( F `  ( ( x  -  T )  +  T
) )  =  ( F `  ( x  -  T ) ) )
324244, 249syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  x  e.  RR )
325 recn 9636 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  x  e.  CC )
326325adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
32762adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
328326, 327npcand 9997 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  -  T )  +  T )  =  x )
329328fveq2d 5885 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( ( x  -  T )  +  T ) )  =  ( F `  x
) )
330241, 324, 329syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( F `  ( ( x  -  T )  +  T
) )  =  ( F `  x ) )
331282, 323, 3303eqtr2rd 2470 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( F `  x )  =  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( x  -  T ) ) )
332331mpteq2dva 4510 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } 
|->  ( F `  x
) )  =  ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
x  -  T ) ) ) )
333236, 240, 3323eqtrd 2467 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  =  ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
x  -  T ) ) ) )
334 ioosscn 37540 . . . . . . . . . . 11  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
335334a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
336 eqeq1 2426 . . . . . . . . . . . . 13  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
337336rexbidv 2936 . . . . . . . . . . . 12  |-  ( w  =  x  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  <->  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) ) )
338 oveq1 6312 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
339338eqeq2d 2436 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
340339cbvrexv 3055 . . . . . . . . . . . 12  |-  ( E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) )
341337, 340syl6bb 264 . . . . . . . . . . 11  |-  ( w  =  x  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) ) )
342341cbvrabv 3079 . . . . . . . . . 10  |-  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  =  { x  e.  CC  |  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) }
343 eqid 2422 . . . . . . . . . 10  |-  ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
x  -  T ) ) )  =  ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
x  -  T ) ) )
344335, 255, 342, 21, 343cncfshift 37691 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } 
|->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
x  -  T ) ) )  e.  ( { w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) }
-cn-> CC ) )
345239eqcomd 2430 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  =  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
346345oveq1d 6320 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) } -cn-> CC )  =  ( ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) -cn-> CC ) )
347344, 346eleqtrd 2509 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } 
|->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
x  -  T ) ) )  e.  ( ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) -cn-> CC ) )
348333, 347eqeltrd 2507 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  e.  ( ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) -cn-> CC ) )
349348adantlr 719 . . . . . 6  |-  ( ( ( ph  /\  0  <  -u T )  /\  i  e.  ( 0..^ M ) )  -> 
( F  |`  (
( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) )  e.  ( ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) )
-cn-> CC ) )
350 ffdm 5760 . . . . . . . . . . . 12  |-  ( F : RR --> CC  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
35119, 350syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
352351simpld 460 . . . . . . . . . 10  |-  ( ph  ->  F : dom  F --> CC )
353352adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : dom  F --> CC )
354 ioossre 11703 . . . . . . . . . 10  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
355 fdm 5750 . . . . . . . . . . 11  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
356233, 355syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  F  =  RR )
357354, 356syl5sseqr 3513 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
358342eqcomi 2435 . . . . . . . . 9  |-  { x  e.  CC  |  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) }  =  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }
359235, 345, 3563sstr4d 3507 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  C_  dom  F )
360342, 359syl5eqssr 3509 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { x  e.  CC  |  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) }  C_  dom  F )
361 simpll 758 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
362361, 290syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
363361, 292syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
364361, 294syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
365 simplr 760 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
366 ioossicc 11727 . . . . . . . . . . . . 13  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
367366sseli 3460 . . . . . . . . . . . 12  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
368367adantl 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
369362, 363, 364, 365, 368fourierdlem1 37910 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( A [,] B
) )
370 eleq1 2495 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
x  e.  ( A [,] B )  <->  z  e.  ( A [,] B ) ) )
371370anbi2d 708 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  z  e.  ( A [,] B ) ) ) )
372 oveq1 6312 . . . . . . . . . . . . . 14  |-  ( x  =  z  ->  (
x  +  T )  =  ( z  +  T ) )
373372fveq2d 5885 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  ( F `  ( x  +  T ) )  =  ( F `  (
z  +  T ) ) )
374 fveq2 5881 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
375373, 374eqeq12d 2444 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( z  +  T
) )  =  ( F `  z ) ) )
376371, 375imbi12d 321 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( ( ph  /\  x  e.  ( A [,] B ) )  -> 
( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( F `  (
z  +  T ) )  =  ( F `
 z ) ) ) )
377376, 14chvarv 2072 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( F `  ( z  +  T
) )  =  ( F `  z ) )
378361, 369, 377syl2anc 665 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( z  +  T ) )  =  ( F `  z
) )
379353, 335, 357, 255, 358, 360, 378, 23limcperiod 37648 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) } ) lim CC  (
( Q `  i
)  +  T ) ) )
380358, 345syl5eq 2475 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { x  e.  CC  |  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) }  =  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
381380reseq2d 5124 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( y  +  T ) } )  =  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) ) )
382153eqcomd 2430 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  =  ( S `  i ) )
383381, 382oveq12d 6323 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( y  +  T ) } ) lim CC  ( ( Q `  i )  +  T ) )  =  ( ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) ) lim CC  ( S `  i )
) )
384379, 383eleqtrd 2509 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) ) lim CC  ( S `
 i ) ) )
385384adantlr 719 . . . . . 6  |-  ( ( ( ph  /\  0  <  -u T )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) ) ) lim CC  ( S `  i ) ) )
386353, 335, 357, 255, 358, 360, 378, 25limcperiod 37648 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) } ) lim CC  (
( Q `  (
i  +  1 ) )  +  T ) ) )
387160eqcomd 2430 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  =  ( S `  ( i  +  1 ) ) )
388381, 387oveq12d 6323 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( y  +  T ) } ) lim CC  ( ( Q `  ( i  +  1 ) )  +  T ) )  =  ( ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) ) lim CC  ( S `  ( i  +  1 ) ) ) )
389386, 388eleqtrd 2509 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) ) lim CC  ( S `
 ( i  +  1 ) ) ) )
390389adantlr 719 . . . . . 6  |-  ( ( ( ph  /\  0  <  -u T )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) ) ) lim CC  ( S `  ( i  +  1 ) ) ) )
391 eqeq1 2426 . . . . . . . 8  |-  ( y  =  x  ->  (
y  =  ( S `
 i )  <->  x  =  ( S `  i ) ) )
392 eqeq1 2426 . . . . . . . . 9  |-  ( y  =  x  ->  (
y  =  ( S `
 ( i  +  1 ) )  <->  x  =  ( S `  ( i  +  1 ) ) ) )
393392, 29ifbieq2d 3936 . . . . . . . 8  |-  ( y  =  x  ->  if ( y  =  ( S `  ( i  +  1 ) ) ,  L ,  ( F `  y ) )  =  if ( x  =  ( S `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
394391, 393ifbieq2d 3936 . . . . . . 7  |-  ( y  =  x  ->  if ( y  =  ( S `  i ) ,  R ,  if ( y  =  ( S `  ( i  +  1 ) ) ,  L ,  ( F `  y ) ) )  =  if ( x  =  ( S `  i ) ,  R ,  if ( x  =  ( S `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
395394cbvmptv 4516 . . . . . 6  |-  ( y  e.  ( ( S `
 i ) [,] ( S `  (
i  +  1 ) ) )  |->  if ( y  =  ( S `
 i ) ,  R ,  if ( y  =  ( S `
 ( i  +  1 ) ) ,  L ,  ( F `
 y ) ) ) )  =  ( x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) )  |->  if ( x  =  ( S `  i ) ,  R ,  if ( x  =  ( S `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
396 eqid 2422 . . . . . 6  |-  ( x  e.  ( ( ( j  e.  ( 0 ... M )  |->  ( ( S `  j
)  +  -u T
) ) `  i
) [,] ( ( j  e.  ( 0 ... M )  |->  ( ( S `  j
)  +  -u T
) ) `  (
i  +  1 ) ) )  |->  ( ( y  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) )  |->  if ( y  =  ( S `  i ) ,  R ,  if ( y  =  ( S `  ( i  +  1 ) ) ,  L ,  ( F `  y ) ) ) ) `  ( x  -  -u T
) ) )  =  ( x  e.  ( ( ( j  e.  ( 0 ... M
)  |->  ( ( S `
 j )  + 
-u T ) ) `
 i ) [,] ( ( j  e.  ( 0 ... M
)  |->  ( ( S `
 j )  + 
-u T ) ) `
 ( i  +  1 ) ) ) 
|->  ( ( y  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) )  |->  if ( y  =  ( S `  i ) ,  R ,  if ( y  =  ( S `  (
i  +  1 ) ) ,  L , 
( F `  y
) ) ) ) `
 ( x  -  -u T ) ) )
39777, 79, 80, 81, 84, 170, 228, 231, 232, 349, 385, 390, 395, 396fourierdlem81 37991 . . . . 5  |-  ( (
ph  /\  0  <  -u T )  ->  S. ( ( ( A  +  T )  + 
-u T ) [,] ( ( B  +  T )  +  -u T ) ) ( F `  x )  _d x  =  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x )
39874, 397eqtr2d 2464 . . . 4  |-  ( (
ph  /\  0  <  -u T )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
39949, 59, 398syl2anc 665 . . 3  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  S. (
( A  +  T
) [,] ( B  +  T ) ) ( F `  x
)  _d x  =  S. ( A [,] B ) ( F `
 x )  _d x )
40048, 399pm2.61dan 798 . 2  |-  ( (
ph  /\  -.  0  <  T )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
40134, 400pm2.61dan 798 1  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
Colors of variables: wff setvar class
Syntax hints:   -.