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

Theorem fourierdlem92 32184
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 465 . . 3  |-  ( (
ph  /\  0  <  T )  ->  A  e.  RR )
3 fourierdlem92.b . . . 4  |-  ( ph  ->  B  e.  RR )
43adantr 465 . . 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 465 . . 3  |-  ( (
ph  /\  0  <  T )  ->  M  e.  NN )
8 fourierdlem92.t . . . . 5  |-  ( ph  ->  T  e.  RR )
98adantr 465 . . . 4  |-  ( (
ph  /\  0  <  T )  ->  T  e.  RR )
10 simpr 461 . . . 4  |-  ( (
ph  /\  0  <  T )  ->  0  <  T )
119, 10elrpd 11279 . . 3  |-  ( (
ph  /\  0  <  T )  ->  T  e.  RR+ )
12 fourierdlem92.q . . . 4  |-  ( ph  ->  Q  e.  ( P `
 M ) )
1312adantr 465 . . 3  |-  ( (
ph  /\  0  <  T )  ->  Q  e.  ( P `  M ) )
14 fourierdlem92.fper . . . 4  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
1514adantlr 714 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  x  e.  ( A [,] B
) )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
16 fveq2 5872 . . . . 5  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
1716oveq1d 6311 . . . 4  |-  ( j  =  i  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 i )  +  T ) )
1817cbvmptv 4548 . . 3  |-  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j )  +  T ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( Q `
 i )  +  T ) )
19 fourierdlem92.f . . . 4  |-  ( ph  ->  F : RR --> CC )
2019adantr 465 . . 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 714 . . 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 714 . . 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 714 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
27 eqeq1 2461 . . . . 5  |-  ( y  =  x  ->  (
y  =  ( Q `
 i )  <->  x  =  ( Q `  i ) ) )
28 eqeq1 2461 . . . . . 6  |-  ( y  =  x  ->  (
y  =  ( Q `
 ( i  +  1 ) )  <->  x  =  ( Q `  ( i  +  1 ) ) ) )
29 fveq2 5872 . . . . . 6  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
3028, 29ifbieq2d 3969 . . . . 5  |-  ( y  =  x  ->  if ( y  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  y ) )  =  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
3127, 30ifbieq2d 3969 . . . 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 4548 . . 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 2457 . . 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 32173 . 2  |-  ( (
ph  /\  0  <  T )  ->  S. (
( A  +  T
) [,] ( B  +  T ) ) ( F `  x
)  _d x  =  S. ( A [,] B ) ( F `
 x )  _d x )
35 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  T  =  0 )
3635oveq2d 6312 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  T )  =  ( A  + 
0 ) )
371recnd 9639 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
3837adantr 465 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  A  e.  CC )
3938addid1d 9797 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  0 )  =  A )
4036, 39eqtrd 2498 . . . . . 6  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  T )  =  A )
4135oveq2d 6312 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  T )  =  ( B  + 
0 ) )
423recnd 9639 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
4342adantr 465 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  B  e.  CC )
4443addid1d 9797 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  0 )  =  B )
4541, 44eqtrd 2498 . . . . . 6  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  T )  =  B )
4640, 45oveq12d 6314 . . . . 5  |-  ( (
ph  /\  T  = 
0 )  ->  (
( A  +  T
) [,] ( B  +  T ) )  =  ( A [,] B ) )
4746itgeq1d 31958 . . . 4  |-  ( (
ph  /\  T  = 
0 )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
4847adantlr 714 . . 3  |-  ( ( ( ph  /\  -.  0  <  T )  /\  T  =  0 )  ->  S. ( ( A  +  T ) [,] ( B  +  T ) ) ( F `  x )  _d x  =  S. ( A [,] B
) ( F `  x )  _d x )
49 simpll 753 . . . 4  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ph )
50 simpr 461 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  T  =  0 )
51 simplr 755 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  0  <  T )
52 ioran 490 . . . . . . 7  |-  ( -.  ( T  =  0  \/  0  <  T
)  <->  ( -.  T  =  0  /\  -.  0  <  T ) )
5350, 51, 52sylanbrc 664 . . . . . 6  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  ( T  =  0  \/  0  <  T ) )
5449, 8syl 16 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  T  e.  RR )
55 0red 9614 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  0  e.  RR )
5654, 55lttrid 9740 . . . . . 6  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ( T  <  0  <->  -.  ( T  =  0  \/  0  <  T ) ) )
5753, 56mpbird 232 . . . . 5  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  T  <  0 )
5854lt0neg1d 10143 . . . . 5  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ( T  <  0  <->  0  <  -u T
) )
5957, 58mpbid 210 . . . 4  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  0  <  -u T )
601, 8readdcld 9640 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  +  T
)  e.  RR )
6160recnd 9639 . . . . . . . . . . 11  |-  ( ph  ->  ( A  +  T
)  e.  CC )
628recnd 9639 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  CC )
6361, 62negsubd 9956 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  +  T )  +  -u T )  =  ( ( A  +  T
)  -  T ) )
6437, 62pncand 9951 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
6563, 64eqtrd 2498 . . . . . . . . 9  |-  ( ph  ->  ( ( A  +  T )  +  -u T )  =  A )
663, 8readdcld 9640 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  +  T
)  e.  RR )
6766recnd 9639 . . . . . . . . . . 11  |-  ( ph  ->  ( B  +  T
)  e.  CC )
6867, 62negsubd 9956 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  +  T )  +  -u T )  =  ( ( B  +  T
)  -  T ) )
6942, 62pncand 9951 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  +  T )  -  T
)  =  B )
7068, 69eqtrd 2498 . . . . . . . . 9  |-  ( ph  ->  ( ( B  +  T )  +  -u T )  =  B )
7165, 70oveq12d 6314 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  +  T )  + 
-u T ) [,] ( ( B  +  T )  +  -u T ) )  =  ( A [,] B
) )
7271eqcomd 2465 . . . . . . 7  |-  ( ph  ->  ( A [,] B
)  =  ( ( ( A  +  T
)  +  -u T
) [,] ( ( B  +  T )  +  -u T ) ) )
7372itgeq1d 31958 . . . . . 6  |-  ( ph  ->  S. ( A [,] B ) ( F `
 x )  _d x  =  S. ( ( ( A  +  T )  +  -u T ) [,] (
( B  +  T
)  +  -u T
) ) ( F `
 x )  _d x )
7473adantr 465 . . . . 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 465 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  A  e.  RR )
768adantr 465 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  T  e.  RR )
7775, 76readdcld 9640 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  ( A  +  T )  e.  RR )
783adantr 465 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  B  e.  RR )
7978, 76readdcld 9640 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  ( B  +  T )  e.  RR )
80 eqid 2457 . . . . . 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 465 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  M  e.  NN )
8276renegcld 10007 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  -u T  e.  RR )
83 simpr 461 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  0  <  -u T )
8482, 83elrpd 11279 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  -u T  e.  RR+ )
855fourierdlem2 32094 . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
89 elmapi 7459 . . . . . . . . . . . . . . 15  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
9088, 89syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
9190ffvelrnda 6032 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
928adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  T  e.  RR )
9391, 92readdcld 9640 . . . . . . . . . . . 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 6056 . . . . . . . . . . 11  |-  ( ph  ->  S : ( 0 ... M ) --> RR )
96 reex 9600 . . . . . . . . . . . . 13  |-  RR  e.  _V
9796a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  _V )
98 ovex 6324 . . . . . . . . . . . . 13  |-  ( 0 ... M )  e. 
_V
9998a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... M
)  e.  _V )
10097, 99elmapd 7452 . . . . . . . . . . 11  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
S : ( 0 ... M ) --> RR ) )
10195, 100mpbird 232 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... M ) ) )
10294a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  S  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) ) )
103 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
104103oveq1d 6311 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
105104adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
106 0zd 10897 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  ZZ )
1076nnzd 10989 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ZZ )
108106, 107, 1063jca 1176 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )
)
109 0le0 10646 . . . . . . . . . . . . . . . 16  |-  0  <_  0
110109a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  0 )
111 nnnn0 10823 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  NN  ->  M  e.  NN0 )
112111nn0ge0d 10876 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  ->  0  <_  M )
1136, 112syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  M )
114108, 110, 113jca32 535 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
115 elfz2 11704 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
116114, 115sylibr 212 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  ( 0 ... M ) )
11790, 116ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  0
)  e.  RR )
118117, 8readdcld 9640 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  e.  RR )
119102, 105, 116, 118fvmptd 5961 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  0
)  =  ( ( Q `  0 )  +  T ) )
120 simprll 763 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q `  0
)  =  A )
122121oveq1d 6311 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  =  ( A  +  T ) )
123119, 122eqtrd 2498 . . . . . . . . . . 11  |-  ( ph  ->  ( S `  0
)  =  ( A  +  T ) )
124 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
125124oveq1d 6311 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
126125adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
1276nnnn0d 10873 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN0 )
128 nn0uz 11140 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
129127, 128syl6eleq 2555 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
130 eluzfz2 11719 . . . . . . . . . . . . . 14  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
131129, 130syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( 0 ... M ) )
13290, 131ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  M
)  e.  RR )
133132, 8readdcld 9640 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q `  M )  +  T
)  e.  RR )
134102, 126, 131, 133fvmptd 5961 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  M
)  =  ( ( Q `  M )  +  T ) )
135 simprlr 764 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q `  M
)  =  B )
137136oveq1d 6311 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q `  M )  +  T
)  =  ( B  +  T ) )
138134, 137eqtrd 2498 . . . . . . . . . . 11  |-  ( ph  ->  ( S `  M
)  =  ( B  +  T ) )
139123, 138jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( ( S ` 
0 )  =  ( A  +  T )  /\  ( S `  M )  =  ( B  +  T ) ) )
14090adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
141 elfzofz 11841 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
142141adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
143140, 142ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
144 fzofzp1 11912 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
145144adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
146140, 145ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
1478adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  RR )
14887simprrd 758 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
149148r19.21bi 2826 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
150143, 146, 147, 149ltadd1dd 10184 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) )
151143, 147readdcld 9640 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
15294fvmpt2 5964 . . . . . . . . . . . . 13  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  +  T
)  e.  RR )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
153142, 151, 152syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
15494, 18eqtr4i 2489 . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . 15  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
157156oveq1d 6311 . . . . . . . . . . . . . 14  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
158157adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
159146, 147readdcld 9640 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
160155, 158, 145, 159fvmptd 5961 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  +  T ) )
161150, 153, 1603brtr4d 4486 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  <  ( S `  ( i  +  1 ) ) )
162161ralrimiva 2871 . . . . . . . . . 10  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( S `  i )  <  ( S `  ( i  +  1 ) ) )
163101, 139, 162jca32 535 . . . . . . . . 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 32094 . . . . . . . . . 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 16 . . . . . . . . 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 232 . . . . . . . 8  |-  ( ph  ->  S  e.  ( H `
 M ) )
168164fveq1i 5873 . . . . . . . 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 2555 . . . . . . 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 465 . . . . . 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 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR )
17266adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR )
173 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
174 eliccre 31743 . . . . . . . . . . . 12  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  ->  x  e.  RR )
175171, 172, 173, 174syl3anc 1228 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  RR )
176175recnd 9639 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  CC )
17762negcld 9937 . . . . . . . . . . 11  |-  ( ph  -> 
-u T  e.  CC )
178177adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  -u T  e.  CC )
179176, 178addcld 9632 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  CC )
180 simpl 457 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ph )
1811adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  e.  RR )
1823adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  B  e.  RR )
1838renegcld 10007 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u T  e.  RR )
184183adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  -u T  e.  RR )
185175, 184readdcld 9640 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  RR )
18663, 64eqtr2d 2499 . . . . . . . . . . . . 13  |-  ( ph  ->  A  =  ( ( A  +  T )  +  -u T ) )
187186adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  =  ( ( A  +  T )  + 
-u T ) )
188171rexrd 9660 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR* )
189172rexrd 9660 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR* )
190 iccgelb 11606 . . . . . . . . . . . . . 14  |-  ( ( ( A  +  T
)  e.  RR*  /\  ( B  +  T )  e.  RR*  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
191188, 189, 173, 190syl3anc 1228 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
192171, 175, 184, 191leadd1dd 10187 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( A  +  T
)  +  -u T
)  <_  ( x  +  -u T ) )
193187, 192eqbrtrd 4476 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  <_  ( x  +  -u T ) )
194 iccleub 11605 . . . . . . . . . . . . . 14  |-  ( ( ( A  +  T
)  e.  RR*  /\  ( B  +  T )  e.  RR*  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
195188, 189, 173, 194syl3anc 1228 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
196175, 172, 184, 195leadd1dd 10187 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  <_  ( ( B  +  T )  +  -u T ) )
197172recnd 9639 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  CC )
19862adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  T  e.  CC )
199197, 198negsubd 9956 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  +  -u T
)  =  ( ( B  +  T )  -  T ) )
20069adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  -  T )  =  B )
201199, 200eqtrd 2498 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  +  -u T
)  =  B )
202196, 201breqtrd 4480 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  <_  B )
203181, 182, 185, 193, 202eliccd 31741 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  ( A [,] B ) )
204180, 203jca 532 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( ph  /\  ( x  +  -u T )  e.  ( A [,] B ) ) )
205 eleq1 2529 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  (
y  e.  ( A [,] B )  <->  ( x  +  -u T )  e.  ( A [,] B
) ) )
206205anbi2d 703 . . . . . . . . . . 11  |-  ( y  =  ( x  +  -u T )  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  ( x  +  -u T )  e.  ( A [,] B ) ) ) )
207 oveq1 6303 . . . . . . . . . . . . 13  |-  ( y  =  ( x  +  -u T )  ->  (
y  +  T )  =  ( ( x  +  -u T )  +  T ) )
208207fveq2d 5876 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  ( F `  ( y  +  T ) )  =  ( F `  (
( x  +  -u T )  +  T
) ) )
209 fveq2 5872 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  ( F `  y )  =  ( F `  ( x  +  -u T
) ) )
210208, 209eqeq12d 2479 . . . . . . . . . . 11  |-  ( y  =  ( x  +  -u T )  ->  (
( F `  (
y  +  T ) )  =  ( F `
 y )  <->  ( F `  ( ( x  +  -u T )  +  T
) )  =  ( F `  ( x  +  -u T ) ) ) )
211206, 210imbi12d 320 . . . . . . . . . 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 2529 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
x  e.  ( A [,] B )  <->  y  e.  ( A [,] B ) ) )
213212anbi2d 703 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  y  e.  ( A [,] B ) ) ) )
214 oveq1 6303 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
x  +  T )  =  ( y  +  T ) )
215214fveq2d 5876 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( F `  ( x  +  T ) )  =  ( F `  (
y  +  T ) ) )
216 fveq2 5872 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
217215, 216eqeq12d 2479 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( y  +  T
) )  =  ( F `  y ) ) )
218213, 217imbi12d 320 . . . . . . . . . . 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 2015 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  ( y  +  T
) )  =  ( F `  y ) )
220211, 219vtoclg 3167 . . . . . . . . 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 60 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( (
x  +  -u T
)  +  T ) )  =  ( F `
 ( x  +  -u T ) ) )
222176, 198negsubd 9956 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  =  ( x  -  T ) )
223222oveq1d 6311 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  +  T
)  =  ( ( x  -  T )  +  T ) )
224176, 198npcand 9954 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  -  T
)  +  T )  =  x )
225223, 224eqtrd 2498 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  +  T
)  =  x )
226225fveq2d 5876 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( (
x  +  -u T
)  +  T ) )  =  ( F `
 x ) )
227221, 226eqtr3d 2500 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( x  +  -u T ) )  =  ( F `  x ) )
228227adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  0  <  -u T )  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  -> 
( F `  (
x  +  -u T
) )  =  ( F `  x ) )
229 fveq2 5872 . . . . . . . 8  |-  ( j  =  i  ->  ( S `  j )  =  ( S `  i ) )
230229oveq1d 6311 . . . . . . 7  |-  ( j  =  i  ->  (
( S `  j
)  +  -u T
)  =  ( ( S `  i )  +  -u T ) )
231230cbvmptv 4548 . . . . . 6  |-  ( j  e.  ( 0 ... M )  |->  ( ( S `  j )  +  -u T ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( S `
 i )  + 
-u T ) )
23219adantr 465 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  F : RR --> CC )
23319adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
234 ioossre 11611 . . . . . . . . . . 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 5927 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  =  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) ) )
237153, 160oveq12d 6314 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  =  ( ( ( Q `  i )  +  T
) (,) ( ( Q `  ( i  +  1 ) )  +  T ) ) )
238143, 146, 147iooshift 31765 . . . . . . . . . . 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 2498 . . . . . . . . . 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 4538 . . . . . . . . 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 753 . . . . . . . . . . . . 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 755 . . . . . . . . . . . . 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 2527 . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . 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 9660 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
2462453adant3 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  e.  RR* )
247146rexrd 9660 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
2482473adant3 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
249 elioore 11584 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( ( Q `  i )  +  T ) (,) ( ( Q `  ( i  +  1 ) )  +  T
) )  ->  x  e.  RR )
250249adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  x  e.  RR )
2518adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  T  e.  RR )
252250, 251resubcld 10008 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  (
x  -  T )  e.  RR )
2532523adant2 1015 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  RR )
254143recnd 9639 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
25562adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  CC )
256254, 255pncand 9951 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  =  ( Q `  i ) )
257256eqcomd 2465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
2582573adant3 1016 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
2591513adant3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
2602503adant2 1015 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  e.  RR )
26183ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  T  e.  RR )
262151rexrd 9660 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR* )
2632623adant3 1016 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  e.  RR* )
264159rexrd 9660 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR* )
2652643adant3 1016 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR* )
266 simp3 998 . . . . . . . . . . . . . . . . 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 31731 . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  <  x
)
269259, 260, 261, 268ltsub1dd 10185 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  <  (
x  -  T ) )
270258, 269eqbrtrd 4476 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  <  (
x  -  T ) )
2711593adant3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
272 iooltub 31751 . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  <  (
( Q `  (
i  +  1 ) )  +  T ) )
274260, 271, 261, 273ltsub1dd 10185 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  (
( ( Q `  ( i  +  1 ) )  +  T
)  -  T ) )
275146recnd 9639 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
276275, 255pncand 9951 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
2772763adant3 1016 . . . . . . . . . . . . . . 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 4480 . . . . . . . . . . . . . 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 31734 . . . . . . . . . . . . 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 1228 . . . . . . . . . . . 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 5886 . . . . . . . . . . . 12  |-  ( ( x  -  T )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( x  -  T ) )  =  ( F `  ( x  -  T
) ) )
282280, 281syl 16 . . . . . . . . . . 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 661 . . . . . . . . . . . 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 1017 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  e.  RR )
28533ad2ant1 1017 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  B  e.  RR )
28664eqcomd 2465 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  =  ( ( A  +  T )  -  T ) )
2872863ad2ant1 1017 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  =  ( ( A  +  T
)  -  T ) )
288603ad2ant1 1017 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  e.  RR )
2891adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR )
2901rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  e.  RR* )
291290adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
2923rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  RR* )
293292adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
2945, 6, 12fourierdlem15 32107 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
295294adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
296295, 142ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( A [,] B ) )
297 iccgelb 11606 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 i )  e.  ( A [,] B
) )  ->  A  <_  ( Q `  i
) )
298291, 293, 296, 297syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  <_  ( Q `  i )
)
299289, 143, 147, 298leadd1dd 10187 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A  +  T )  <_  (
( Q `  i
)  +  T ) )
3002993adant3 1016 . . . . . . . . . . . . . . . . . . 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 9757 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  <  x
)
302288, 260, 261, 301ltsub1dd 10185 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( A  +  T )  -  T )  <  (
x  -  T ) )
303287, 302eqbrtrd 4476 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  <  (
x  -  T ) )
304284, 253, 303ltled 9750 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  <_  (
x  -  T ) )
3051463adant3 1016 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
306295, 145ffvelrnd 6033 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
307 iccleub 11605 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 ( i  +  1 ) )  e.  ( A [,] B
) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
308291, 293, 306, 307syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  <_  B
)
3093083adant3 1016 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  <_  B
)
310253, 305, 285, 278, 309ltletrd 9759 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  B
)
311253, 285, 310ltled 9750 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <_  B
)
312284, 285, 253, 304, 311eliccd 31741 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  ( A [,] B ) )
313241, 242, 244, 312syl3anc 1228 . . . . . . . . . . . . 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 532 . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  (
y  e.  ( A [,] B )  <->  ( x  -  T )  e.  ( A [,] B ) ) )
316315anbi2d 703 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  T )  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  ( x  -  T
)  e.  ( A [,] B ) ) ) )
317 oveq1 6303 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  -  T )  ->  (
y  +  T )  =  ( ( x  -  T )  +  T ) )
318317fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  ( F `  ( y  +  T ) )  =  ( F `  (
( x  -  T
)  +  T ) ) )
319 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  ( F `  y )  =  ( F `  ( x  -  T
) ) )
320318, 319eqeq12d 2479 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  T )  ->  (
( F `  (
y  +  T ) )  =  ( F `
 y )  <->  ( F `  ( ( x  -  T )  +  T
) )  =  ( F `  ( x  -  T ) ) ) )
321316, 320imbi12d 320 . . . . . . . . . . . . 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 3167 . . . . . . . . . . . 12  |-  ( ( x  -  T )  e.  RR  ->  (
( ph  /\  (
x  -  T )  e.  ( A [,] B ) )  -> 
( F `  (
( x  -  T
)  +  T ) )  =  ( F `
 ( x  -  T ) ) ) )
323283, 314, 322sylc 60 . . . . . . . . . . 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 16 . . . . . . . . . . . 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 9599 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  x  e.  CC )
326325adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
32762adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
328326, 327npcand 9954 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  -  T )  +  T )  =  x )
329328fveq2d 5876 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( ( x  -  T )  +  T ) )  =  ( F `  x
) )
330241, 324, 329syl2anc 661 . . . . . . . . . . 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 2505 . . . . . . . . . 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 4543 . . . . . . . . 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 2502 . . . . . . . 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 31730 . . . . . . . . . . 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 2461 . . . . . . . . . . . . 13  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
337336rexbidv 2968 . . . . . . . . . . . 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 6303 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
339338eqeq2d 2471 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
340339cbvrexv 3085 . . . . . . . . . . . 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 261 . . . . . . . . . . 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 3108 . . . . . . . . . 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 2457 . . . . . . . . . 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 31879 . . . . . . . . 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 2465 . . . . . . . . . 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 6311 . . . . . . . . 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 2547 . . . . . . . 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 2545 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  e.  ( ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) -cn-> CC ) )
349348adantlr 714 . . . . . 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 5751 . . . . . . . . . . . 12  |-  ( F : RR --> CC  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
35119, 350syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
352351simpld 459 . . . . . . . . . 10  |-  ( ph  ->  F : dom  F --> CC )
353352adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : dom  F --> CC )
354 ioossre 11611 . . . . . . . . . 10  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
355 fdm 5741 . . . . . . . . . . 11  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
356233, 355syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  F  =  RR )
357354, 356syl5sseqr 3548 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
358342eqcomi 2470 . . . . . . . . 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 3542 . . . . . . . . . 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 3544 . . . . . . . . 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 753 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
362361, 290syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
363361, 292syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
364361, 294syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
365 simplr 755 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
366 ioossicc 11635 . . . . . . . . . . . . 13  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
367366sseli 3495 . . . . . . . . . . . 12  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
368367adantl 466 . . . . . . . . . . 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 32093 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( A [,] B
) )
370 eleq1 2529 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
x  e.  ( A [,] B )  <->  z  e.  ( A [,] B ) ) )
371370anbi2d 703 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  z  e.  ( A [,] B ) ) ) )
372 oveq1 6303 . . . . . . . . . . . . . 14  |-  ( x  =  z  ->  (
x  +  T )  =  ( z  +  T ) )
373372fveq2d 5876 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  ( F `  ( x  +  T ) )  =  ( F `  (
z  +  T ) ) )
374 fveq2 5872 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
375373, 374eqeq12d 2479 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( z  +  T
) )  =  ( F `  z ) ) )
376371, 375imbi12d 320 . . . . . . . . . . 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 2015 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( F `  ( z  +  T
) )  =  ( F `  z ) )
378361, 369, 377syl2anc 661 . . . . . . . . 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 31837 . . . . . . . 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 2510 . . . . . . . . . 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 5283 . . . . . . . . 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 2465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  =  ( S `  i ) )
383381, 382oveq12d 6314 . . . . . . . 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 2547 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) ) lim CC  ( S `
 i ) ) )
385384adantlr 714 . . . . . 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 31837 . . . . . . . 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 2465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  =  ( S `  ( i  +  1 ) ) )
388381, 387oveq12d 6314 . . . . . . . 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 2547 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) ) lim CC  ( S `
 ( i  +  1 ) ) ) )
390389adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  0  <  -u T )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) ) ) lim CC  ( S `  ( i  +  1 ) ) ) )
391 eqeq1 2461 . . . . . . . 8  |-  ( y  =  x  ->  (
y  =  ( S `
 i )  <->  x  =  ( S `  i ) ) )
392 eqeq1 2461 . . . . . . . . 9  |-  ( y  =  x  ->  (
y  =  ( S `
 ( i  +  1 ) )  <->  x  =  ( S `  ( i  +  1 ) ) ) )
393392, 29ifbieq2d 3969 . . . . . . . 8  |-  ( y  =  x  ->  if ( y  =  ( S `  ( i  +  1 ) ) ,  L ,  ( F `  y ) )  =  if ( x  =  ( S `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
394391, 393ifbieq2d 3969 . . . . . . 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 4548 . . . . . 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 2457 . . . . . 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 32173 . . . . 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 2499 . . . 4  |-  ( (
ph  /\  0  <  -u T )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
39949, 59, 398syl2anc 661 . . 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 791 . 2  |-  ( (
ph  /\  -.  0  <  T )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
40134, 400pm2.61dan 791 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: