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

Theorem fourierdlem92 31822
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 11266 . . 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 nfcv 2629 . . . 4  |-  F/_ i
( ( Q `  j )  +  T
)
17 nfcv 2629 . . . 4  |-  F/_ j
( ( Q `  i )  +  T
)
18 fveq2 5872 . . . . 5  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
1918oveq1d 6310 . . . 4  |-  ( j  =  i  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 i )  +  T ) )
2016, 17, 19cbvmpt 4543 . . 3  |-  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j )  +  T ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( Q `
 i )  +  T ) )
21 fourierdlem92.f . . . 4  |-  ( ph  ->  F : RR --> CC )
2221adantr 465 . . 3  |-  ( (
ph  /\  0  <  T )  ->  F : RR
--> CC )
23 fourierdlem92.cncf . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
2423adantlr 714 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
25 fourierdlem92.r . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
2625adantlr 714 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
27 fourierdlem92.l . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
2827adantlr 714 . . 3  |-  ( ( ( ph  /\  0  <  T )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
29 nfcv 2629 . . . 4  |-  F/_ x if ( y  =  ( Q `  i ) ,  R ,  if ( y  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  y ) ) )
30 nfcv 2629 . . . 4  |-  F/_ y if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )
31 eqeq1 2471 . . . . 5  |-  ( y  =  x  ->  (
y  =  ( Q `
 i )  <->  x  =  ( Q `  i ) ) )
32 eqidd 2468 . . . . 5  |-  ( y  =  x  ->  R  =  R )
33 eqeq1 2471 . . . . . 6  |-  ( y  =  x  ->  (
y  =  ( Q `
 ( i  +  1 ) )  <->  x  =  ( Q `  ( i  +  1 ) ) ) )
34 eqidd 2468 . . . . . 6  |-  ( y  =  x  ->  L  =  L )
35 fveq2 5872 . . . . . 6  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
3633, 34, 35ifeq123d 31337 . . . . 5  |-  ( y  =  x  ->  if ( y  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  y ) )  =  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
3731, 32, 36ifeq123d 31337 . . . 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 ) ) ) )
3829, 30, 37cbvmpt 4543 . . 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 ) ) ) )
39 eqid 2467 . . 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
) ) )
402, 4, 5, 7, 11, 13, 15, 20, 22, 24, 26, 28, 38, 39fourierdlem81 31811 . 2  |-  ( (
ph  /\  0  <  T )  ->  S. (
( A  +  T
) [,] ( B  +  T ) ) ( F `  x
)  _d x  =  S. ( A [,] B ) ( F `
 x )  _d x )
41 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  T  =  0 )
4241oveq2d 6311 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  T )  =  ( A  + 
0 ) )
431recnd 9634 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
4443adantr 465 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  A  e.  CC )
4544addid1d 9791 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  0 )  =  A )
4642, 45eqtrd 2508 . . . . . 6  |-  ( (
ph  /\  T  = 
0 )  ->  ( A  +  T )  =  A )
4741oveq2d 6311 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  T )  =  ( B  + 
0 ) )
483recnd 9634 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
4948adantr 465 . . . . . . . 8  |-  ( (
ph  /\  T  = 
0 )  ->  B  e.  CC )
5049addid1d 9791 . . . . . . 7  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  0 )  =  B )
5147, 50eqtrd 2508 . . . . . 6  |-  ( (
ph  /\  T  = 
0 )  ->  ( B  +  T )  =  B )
5246, 51oveq12d 6313 . . . . 5  |-  ( (
ph  /\  T  = 
0 )  ->  (
( A  +  T
) [,] ( B  +  T ) )  =  ( A [,] B ) )
53 itgeq1 22047 . . . . 5  |-  ( ( ( A  +  T
) [,] ( B  +  T ) )  =  ( A [,] B )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
5452, 53syl 16 . . . 4  |-  ( (
ph  /\  T  = 
0 )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
5554adantlr 714 . . 3  |-  ( ( ( ph  /\  -.  0  <  T )  /\  T  =  0 )  ->  S. ( ( A  +  T ) [,] ( B  +  T ) ) ( F `  x )  _d x  =  S. ( A [,] B
) ( F `  x )  _d x )
56 simpll 753 . . . 4  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ph )
57 simpr 461 . . . . . . . 8  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  T  =  0 )
58 simplr 754 . . . . . . . 8  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  0  <  T )
5957, 58jca 532 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ( -.  T  =  0  /\  -.  0  <  T ) )
60 ioran 490 . . . . . . 7  |-  ( -.  ( T  =  0  \/  0  <  T
)  <->  ( -.  T  =  0  /\  -.  0  <  T ) )
6159, 60sylibr 212 . . . . . 6  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  -.  ( T  =  0  \/  0  <  T ) )
6256, 8syl 16 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  T  e.  RR )
63 0re 9608 . . . . . . . 8  |-  0  e.  RR
6463a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  0  e.  RR )
65 axlttri 9668 . . . . . . 7  |-  ( ( T  e.  RR  /\  0  e.  RR )  ->  ( T  <  0  <->  -.  ( T  =  0  \/  0  <  T
) ) )
6662, 64, 65syl2anc 661 . . . . . 6  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ( T  <  0  <->  -.  ( T  =  0  \/  0  <  T ) ) )
6761, 66mpbird 232 . . . . 5  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  T  <  0 )
6862lt0neg1d 10134 . . . . 5  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  ( T  <  0  <->  0  <  -u T
) )
6967, 68mpbid 210 . . . 4  |-  ( ( ( ph  /\  -.  0  <  T )  /\  -.  T  =  0
)  ->  0  <  -u T )
70 ax-resscn 9561 . . . . . . . . . . . . 13  |-  RR  C_  CC
711, 8readdcld 9635 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  T
)  e.  RR )
7270, 71sseldi 3507 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  +  T
)  e.  CC )
7370, 8sseldi 3507 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  CC )
7472, 73negsubd 9948 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  +  T )  +  -u T )  =  ( ( A  +  T
)  -  T ) )
7543, 73pncand 9943 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
7674, 75eqtr2d 2509 . . . . . . . . . 10  |-  ( ph  ->  A  =  ( ( A  +  T )  +  -u T ) )
7776eqcomd 2475 . . . . . . . . 9  |-  ( ph  ->  ( ( A  +  T )  +  -u T )  =  A )
783, 8readdcld 9635 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  +  T
)  e.  RR )
7970, 78sseldi 3507 . . . . . . . . . . 11  |-  ( ph  ->  ( B  +  T
)  e.  CC )
8079, 73negsubd 9948 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  +  T )  +  -u T )  =  ( ( B  +  T
)  -  T ) )
8148, 73pncand 9943 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  +  T )  -  T
)  =  B )
8280, 81eqtrd 2508 . . . . . . . . 9  |-  ( ph  ->  ( ( B  +  T )  +  -u T )  =  B )
8377, 82oveq12d 6313 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  +  T )  + 
-u T ) [,] ( ( B  +  T )  +  -u T ) )  =  ( A [,] B
) )
84 eqidd 2468 . . . . . . . 8  |-  ( ph  ->  ( A [,] B
)  =  ( A [,] B ) )
8583, 84eqtr2d 2509 . . . . . . 7  |-  ( ph  ->  ( A [,] B
)  =  ( ( ( A  +  T
)  +  -u T
) [,] ( ( B  +  T )  +  -u T ) ) )
86 itgeq1 22047 . . . . . . 7  |-  ( ( A [,] B )  =  ( ( ( A  +  T )  +  -u T ) [,] ( ( B  +  T )  +  -u T ) )  ->  S. ( A [,] B
) ( F `  x )  _d x  =  S. ( ( ( A  +  T
)  +  -u T
) [,] ( ( B  +  T )  +  -u T ) ) ( F `  x
)  _d x )
8785, 86syl 16 . . . . . 6  |-  ( ph  ->  S. ( A [,] B ) ( F `
 x )  _d x  =  S. ( ( ( A  +  T )  +  -u T ) [,] (
( B  +  T
)  +  -u T
) ) ( F `
 x )  _d x )
8887adantr 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 )
891adantr 465 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  A  e.  RR )
908adantr 465 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  T  e.  RR )
9189, 90readdcld 9635 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  ( A  +  T )  e.  RR )
923adantr 465 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  B  e.  RR )
9392, 90readdcld 9635 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  ( B  +  T )  e.  RR )
94 eqid 2467 . . . . . 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 ) ) ) } )
956adantr 465 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  M  e.  NN )
9690renegcld 9998 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  -u T  e.  RR )
97 simpr 461 . . . . . . 7  |-  ( (
ph  /\  0  <  -u T )  ->  0  <  -u T )
9896, 97elrpd 11266 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  -u T  e.  RR+ )
995fourierdlem2 31732 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
1006, 99syl 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 ) ) ) ) ) )
10112, 100mpbid 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 ) ) ) ) )
102101simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
103 elmapi 7452 . . . . . . . . . . . . . . 15  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
104102, 103syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
105104ffvelrnda 6032 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
1068adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  T  e.  RR )
107105, 106readdcld 9635 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  +  T )  e.  RR )
108 fourierdlem92.s . . . . . . . . . . . 12  |-  S  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  +  T
) )
109107, 108fmptd 6056 . . . . . . . . . . 11  |-  ( ph  ->  S : ( 0 ... M ) --> RR )
110 reex 9595 . . . . . . . . . . . . 13  |-  RR  e.  _V
111110a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  _V )
112 ovex 6320 . . . . . . . . . . . . 13  |-  ( 0 ... M )  e. 
_V
113112a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... M
)  e.  _V )
114 elmapg 7445 . . . . . . . . . . . 12  |-  ( ( RR  e.  _V  /\  ( 0 ... M
)  e.  _V )  ->  ( S  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
S : ( 0 ... M ) --> RR ) )
115111, 113, 114syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
S : ( 0 ... M ) --> RR ) )
116109, 115mpbird 232 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... M ) ) )
117108a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) ) )
118 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
119118oveq1d 6310 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
120119adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
121 0z 10887 . . . . . . . . . . . . . . . . . 18  |-  0  e.  ZZ
122121a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  e.  ZZ )
1236nnzd 10977 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  ZZ )
124122, 123, 1223jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )
)
12563leidi 10099 . . . . . . . . . . . . . . . . 17  |-  0  <_  0
126125a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <_  0 )
127 nnnn0 10814 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN  ->  M  e.  NN0 )
128 nn0ge0 10833 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN0  ->  0  <_  M )
129127, 128syl 16 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  NN  ->  0  <_  M )
1306, 129syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <_  M )
131124, 126, 130jca32 535 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
132 elfz2 11691 . . . . . . . . . . . . . . 15  |-  ( 0  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
133131, 132sylibr 212 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  ( 0 ... M ) )
134104, 133ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Q `  0
)  e.  RR )
135134, 8readdcld 9635 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  e.  RR )
136117, 120, 133, 135fvmptd 5962 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S `  0
)  =  ( ( Q `  0 )  +  T ) )
137 simprll 761 . . . . . . . . . . . . . . 15  |-  ( ( 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 )
138101, 137syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  0
)  =  A )
139138oveq1d 6310 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  =  ( A  +  T ) )
140136, 139eqtrd 2508 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  0
)  =  ( A  +  T ) )
141 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
142141oveq1d 6310 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
143142adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
1446, 127syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  NN0 )
145 nn0uz 11128 . . . . . . . . . . . . . . . 16  |-  NN0  =  ( ZZ>= `  0 )
146144, 145syl6eleq 2565 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
147 eluzfz2 11706 . . . . . . . . . . . . . . 15  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
148146, 147syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ( 0 ... M ) )
149104, 148ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Q `  M
)  e.  RR )
150149, 8readdcld 9635 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q `  M )  +  T
)  e.  RR )
151117, 143, 148, 150fvmptd 5962 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S `  M
)  =  ( ( Q `  M )  +  T ) )
152 simprlr 762 . . . . . . . . . . . . . . 15  |-  ( ( 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 )
153101, 152syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  M
)  =  B )
154153oveq1d 6310 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q `  M )  +  T
)  =  ( B  +  T ) )
155151, 154eqtrd 2508 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  M
)  =  ( B  +  T ) )
156140, 155jca 532 . . . . . . . . . . 11  |-  ( ph  ->  ( ( S ` 
0 )  =  ( A  +  T )  /\  ( S `  M )  =  ( B  +  T ) ) )
157104adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
158 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
159 elfzofz 11823 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
160158, 159syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
161157, 160ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
162 fzofzp1 11889 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
163158, 162syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
164157, 163ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
1658adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  RR )
166101simprd 463 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
167166simprd 463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
168167r19.21bi 2836 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
169161, 164, 165, 168ltadd1dd 10175 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) )
170161, 165readdcld 9635 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
171160, 170jca 532 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  e.  ( 0 ... M
)  /\  ( ( Q `  i )  +  T )  e.  RR ) )
172108fvmpt2 5964 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  +  T
)  e.  RR )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
173171, 172syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
174108, 20eqtr4i 2499 . . . . . . . . . . . . . . . 16  |-  S  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  +  T
) )
175174a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  +  T ) ) )
176 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
177176oveq1d 6310 . . . . . . . . . . . . . . . 16  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
178177adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
179164, 165readdcld 9635 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
180175, 178, 163, 179fvmptd 5962 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  +  T ) )
181173, 180breq12d 4466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i )  < 
( S `  (
i  +  1 ) )  <->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) ) )
182169, 181mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  <  ( S `  ( i  +  1 ) ) )
183182ralrimiva 2881 . . . . . . . . . . 11  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( S `  i )  <  ( S `  ( i  +  1 ) ) )
184156, 183jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( S `
 0 )  =  ( A  +  T
)  /\  ( S `  M )  =  ( B  +  T ) )  /\  A. i  e.  ( 0..^ M ) ( S `  i
)  <  ( S `  ( i  +  1 ) ) ) )
185116, 184jca 532 . . . . . . . . 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 ) ) ) ) )
186 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 ) ) ) } )
187186fourierdlem2 31732 . . . . . . . . . 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 ) ) ) ) ) )
1886, 187syl 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 ) ) ) ) ) )
189185, 188mpbird 232 . . . . . . . 8  |-  ( ph  ->  S  e.  ( H `
 M ) )
190186fveq1i 5873 . . . . . . . . 9  |-  ( 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 )
191190a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 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 ) )
192189, 191eleqtrd 2557 . . . . . . 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 ) )
193192adantr 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 ) )
19471adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR )
19578adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR )
196 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
197 eliccre 31427 . . . . . . . . . . . 12  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  ->  x  e.  RR )
198194, 195, 196, 197syl3anc 1228 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  RR )
19970, 198sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  CC )
20073negcld 9929 . . . . . . . . . . 11  |-  ( ph  -> 
-u T  e.  CC )
201200adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  -u T  e.  CC )
202199, 201addcld 9627 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  CC )
203 simpl 457 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ph )
2048renegcld 9998 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u T  e.  RR )
205204adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  -u T  e.  RR )
206198, 205readdcld 9635 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  RR )
20776adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  =  ( ( A  +  T )  + 
-u T ) )
208194rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR* )
209195rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR* )
210 iccgelb 11593 . . . . . . . . . . . . . . 15  |-  ( ( ( A  +  T
)  e.  RR*  /\  ( B  +  T )  e.  RR*  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
211208, 209, 196, 210syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
212194, 198, 205leadd1d 10158 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( A  +  T
)  <_  x  <->  ( ( A  +  T )  +  -u T )  <_ 
( x  +  -u T ) ) )
213211, 212mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( A  +  T
)  +  -u T
)  <_  ( x  +  -u T ) )
214207, 213eqbrtrd 4473 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  <_  ( x  +  -u T ) )
215 iccleub 11592 . . . . . . . . . . . . . . 15  |-  ( ( ( A  +  T
)  e.  RR*  /\  ( B  +  T )  e.  RR*  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
216208, 209, 196, 215syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
217198, 195, 205leadd1d 10158 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  <_  ( B  +  T )  <->  ( x  +  -u T )  <_ 
( ( B  +  T )  +  -u T ) ) )
218216, 217mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  <_  ( ( B  +  T )  +  -u T ) )
21970, 195sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  CC )
220203, 73syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  T  e.  CC )
221219, 220negsubd 9948 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  +  -u T
)  =  ( ( B  +  T )  -  T ) )
22281adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  -  T )  =  B )
223221, 222eqtrd 2508 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  +  -u T
)  =  B )
224218, 223breqtrd 4477 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  <_  B )
225206, 214, 2243jca 1176 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  e.  RR  /\  A  <_  ( x  +  -u T )  /\  ( x  +  -u T
)  <_  B )
)
226203, 1syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  e.  RR )
227203, 3syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  B  e.  RR )
228 elicc2 11601 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( x  +  -u T )  e.  ( A [,] B )  <-> 
( ( x  +  -u T )  e.  RR  /\  A  <_  ( x  +  -u T )  /\  ( x  +  -u T
)  <_  B )
) )
229226, 227, 228syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  e.  ( A [,] B )  <-> 
( ( x  +  -u T )  e.  RR  /\  A  <_  ( x  +  -u T )  /\  ( x  +  -u T
)  <_  B )
) )
230225, 229mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  e.  ( A [,] B ) )
231203, 230jca 532 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( ph  /\  ( x  +  -u T )  e.  ( A [,] B ) ) )
232 eleq1 2539 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  (
y  e.  ( A [,] B )  <->  ( x  +  -u T )  e.  ( A [,] B
) ) )
233232anbi2d 703 . . . . . . . . . . 11  |-  ( y  =  ( x  +  -u T )  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  ( x  +  -u T )  e.  ( A [,] B ) ) ) )
234 oveq1 6302 . . . . . . . . . . . . 13  |-  ( y  =  ( x  +  -u T )  ->  (
y  +  T )  =  ( ( x  +  -u T )  +  T ) )
235234fveq2d 5876 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  ( F `  ( y  +  T ) )  =  ( F `  (
( x  +  -u T )  +  T
) ) )
236 fveq2 5872 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  -u T )  ->  ( F `  y )  =  ( F `  ( x  +  -u T
) ) )
237235, 236eqeq12d 2489 . . . . . . . . . . 11  |-  ( y  =  ( x  +  -u T )  ->  (
( F `  (
y  +  T ) )  =  ( F `
 y )  <->  ( F `  ( ( x  +  -u T )  +  T
) )  =  ( F `  ( x  +  -u T ) ) ) )
238233, 237imbi12d 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 ) ) ) ) )
239 nfv 1683 . . . . . . . . . . . 12  |-  F/ x
( ( ph  /\  y  e.  ( A [,] B ) )  -> 
( F `  (
y  +  T ) )  =  ( F `
 y ) )
240 eleq1 2539 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
x  e.  ( A [,] B )  <->  y  e.  ( A [,] B ) ) )
241240anbi2d 703 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  y  e.  ( A [,] B ) ) ) )
242 oveq1 6302 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
x  +  T )  =  ( y  +  T ) )
243242fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( F `  ( x  +  T ) )  =  ( F `  (
y  +  T ) ) )
244 fveq2 5872 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
245243, 244eqeq12d 2489 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( y  +  T
) )  =  ( F `  y ) ) )
246241, 245imbi12d 320 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  ( A [,] B ) )  -> 
( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  y  e.  ( A [,] B ) )  -> 
( F `  (
y  +  T ) )  =  ( F `
 y ) ) ) )
247239, 246, 14chvar 1982 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  ( y  +  T
) )  =  ( F `  y ) )
248247a1i 11 . . . . . . . . . 10  |-  ( y  e.  CC  ->  (
( ph  /\  y  e.  ( A [,] B
) )  ->  ( F `  ( y  +  T ) )  =  ( F `  y
) ) )
249238, 248vtoclga 3182 . . . . . . . . 9  |-  ( ( x  +  -u T
)  e.  CC  ->  ( ( ph  /\  (
x  +  -u T
)  e.  ( A [,] B ) )  ->  ( F `  ( ( x  +  -u T )  +  T
) )  =  ( F `  ( x  +  -u T ) ) ) )
250202, 231, 249sylc 60 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( (
x  +  -u T
)  +  T ) )  =  ( F `
 ( x  +  -u T ) ) )
251199, 220negsubd 9948 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  +  -u T
)  =  ( x  -  T ) )
252251oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  +  T
)  =  ( ( x  -  T )  +  T ) )
253199, 220npcand 9946 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  -  T
)  +  T )  =  x )
254 eqidd 2468 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  =  x )
255252, 253, 2543eqtrd 2512 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  +  -u T )  +  T
)  =  x )
256255fveq2d 5876 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( (
x  +  -u T
)  +  T ) )  =  ( F `
 x ) )
257250, 256eqtr3d 2510 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  ( x  +  -u T ) )  =  ( F `  x ) )
258257adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  0  <  -u T )  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  -> 
( F `  (
x  +  -u T
) )  =  ( F `  x ) )
259 nfcv 2629 . . . . . . 7  |-  F/_ i
( ( S `  j )  +  -u T )
260 nfcv 2629 . . . . . . 7  |-  F/_ j
( ( S `  i )  +  -u T )
261 fveq2 5872 . . . . . . . 8  |-  ( j  =  i  ->  ( S `  j )  =  ( S `  i ) )
262261oveq1d 6310 . . . . . . 7  |-  ( j  =  i  ->  (
( S `  j
)  +  -u T
)  =  ( ( S `  i )  +  -u T ) )
263259, 260, 262cbvmpt 4543 . . . . . 6  |-  ( j  e.  ( 0 ... M )  |->  ( ( S `  j )  +  -u T ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( S `
 i )  + 
-u T ) )
26421adantr 465 . . . . . 6  |-  ( (
ph  /\  0  <  -u T )  ->  F : RR --> CC )
26521adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
266 ioossre 11598 . . . . . . . . . . 11  |-  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  C_  RR
267266a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  C_  RR )
268265, 267feqresmpt 5928 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  =  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) ) )
269173, 180oveq12d 6313 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  =  ( ( ( Q `  i )  +  T
) (,) ( ( Q `  ( i  +  1 ) )  +  T ) ) )
270161, 164, 165iooshift 31449 . . . . . . . . . . 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 ) } )
271269, 270eqtrd 2508 . . . . . . . . . 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 ) } )
272 mpteq1 4533 . . . . . . . . . 10  |-  ( ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) )  =  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  ->  ( 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
) ) )
273271, 272syl 16 . . . . . . . . 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
) ) )
274 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 )
275158adantr 465 . . . . . . . . . . . . 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 ) )
276270eleq2d 2537 . . . . . . . . . . . . . 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 ) } ) )
277276biimpar 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 ) ) )
278 elioore 11571 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( ( Q `  i )  +  T ) (,) ( ( Q `  ( i  +  1 ) )  +  T
) )  ->  x  e.  RR )
279278adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  x  e.  RR )
2808adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  T  e.  RR )
281279, 280resubcld 9999 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  (
x  -  T )  e.  RR )
2822813adant2 1015 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  RR )
28370, 161sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
28473adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  CC )
285283, 284pncand 9943 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  =  ( Q `  i ) )
286285eqcomd 2475 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
2872863adant3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
288170rexrd 9655 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR* )
2892883adant3 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  e.  RR* )
290179rexrd 9655 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR* )
2912903adant3 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR* )
292 simp3 998 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  e.  ( ( ( Q `  i )  +  T
) (,) ( ( Q `  ( i  +  1 ) )  +  T ) ) )
293 ioogtlb 31415 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( Q `  i )  +  T
)  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  +  T )  e.  RR*  /\  x  e.  ( ( ( Q `
 i )  +  T ) (,) (
( Q `  (
i  +  1 ) )  +  T ) ) )  ->  (
( Q `  i
)  +  T )  <  x )
294289, 291, 292, 293syl3anc 1228 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  <  x
)
2951703adant3 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
2962793adant2 1015 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  e.  RR )
2972803adant2 1015 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  T  e.  RR )
298295, 296, 297ltsub1d 10173 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( ( Q `  i )  +  T )  < 
x  <->  ( ( ( Q `  i )  +  T )  -  T )  <  (
x  -  T ) ) )
299294, 298mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  <  (
x  -  T ) )
300287, 299eqbrtrd 4473 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  <  (
x  -  T ) )
301 iooltub 31435 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) )
302289, 291, 292, 301syl3anc 1228 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  x  <  (
( Q `  (
i  +  1 ) )  +  T ) )
3031793adant3 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
304296, 303, 297ltsub1d 10173 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  < 
( ( Q `  ( i  +  1 ) )  +  T
)  <->  ( x  -  T )  <  (
( ( Q `  ( i  +  1 ) )  +  T
)  -  T ) ) )
305302, 304mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  (
( ( Q `  ( i  +  1 ) )  +  T
)  -  T ) )
30670, 164sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
307306, 284pncand 9943 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
3083073adant3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
309305, 308breqtrd 4477 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  ( Q `  ( i  +  1 ) ) )
310282, 300, 3093jca 1176 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( x  -  T )  e.  RR  /\  ( Q `
 i )  < 
( x  -  T
)  /\  ( x  -  T )  <  ( Q `  ( i  +  1 ) ) ) )
311161rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
3123113adant3 1016 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  i )  e.  RR* )
313164rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
3143133adant3 1016 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
315 elioo2 11582 . . . . . . . . . . . . . . 15  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR* )  ->  (
( x  -  T
)  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( (
x  -  T )  e.  RR  /\  ( Q `  i )  <  ( x  -  T
)  /\  ( x  -  T )  <  ( Q `  ( i  +  1 ) ) ) ) )
316312, 314, 315syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( x  -  T )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( ( x  -  T )  e.  RR  /\  ( Q `
 i )  < 
( x  -  T
)  /\  ( x  -  T )  <  ( Q `  ( i  +  1 ) ) ) ) )
317310, 316mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
318274, 275, 277, 317syl3anc 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 ) ) ) )
319 fvres 5886 . . . . . . . . . . . 12  |-  ( ( x  -  T )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( x  -  T ) )  =  ( F `  ( x  -  T
) ) )
320318, 319syl 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 ) ) )
321274, 277, 281syl2anc 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 )
32213ad2ant1 1017 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  e.  RR )
32375eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  =  ( ( A  +  T )  -  T ) )
3243233ad2ant1 1017 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  =  ( ( A  +  T
)  -  T ) )
325713ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  e.  RR )
3261rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A  e.  RR* )
327326adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
3283rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  e.  RR* )
329328adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
3305, 6, 12fourierdlem15 31745 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
331330adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
332161, 164, 168ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <_  ( Q `  ( i  +  1 ) ) )
333 lbicc2 11648 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( Q `  i )  <_  ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
334311, 313, 332, 333syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
335327, 329, 331, 158, 334fourierdlem1 31731 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( A [,] B ) )
336 iccgelb 11593 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 i )  e.  ( A [,] B
) )  ->  A  <_  ( Q `  i
) )
337327, 329, 335, 336syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  <_  ( Q `  i )
)
3381adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR )
339338, 161, 165leadd1d 10158 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A  <_ 
( Q `  i
)  <->  ( A  +  T )  <_  (
( Q `  i
)  +  T ) ) )
340337, 339mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A  +  T )  <_  (
( Q `  i
)  +  T ) )
3413403adant3 1016 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  <_  (
( Q `  i
)  +  T ) )
342325, 295, 296, 341, 294lelttrd 9751 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( A  +  T )  <  x
)
343325, 296, 297ltsub1d 10173 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( A  +  T )  < 
x  <->  ( ( A  +  T )  -  T )  <  (
x  -  T ) ) )
344342, 343mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( A  +  T )  -  T )  <  (
x  -  T ) )
345324, 344eqbrtrd 4473 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  <  (
x  -  T ) )
346322, 282, 345ltled 9744 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  A  <_  (
x  -  T ) )
34733ad2ant1 1017 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  B  e.  RR )
3481643adant3 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
349331, 163ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
350 iccleub 11592 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 ( i  +  1 ) )  e.  ( A [,] B
) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
351327, 329, 349, 350syl3anc 1228 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  <_  B
)
3523513adant3 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( Q `  ( i  +  1 ) )  <_  B
)
353282, 348, 347, 309, 352ltletrd 9753 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <  B
)
354282, 347, 353ltled 9744 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  <_  B
)
355282, 346, 3543jca 1176 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( x  -  T )  e.  RR  /\  A  <_ 
( x  -  T
)  /\  ( x  -  T )  <_  B
) )
356 elicc2 11601 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( x  -  T )  e.  ( A [,] B )  <-> 
( ( x  -  T )  e.  RR  /\  A  <_  ( x  -  T )  /\  (
x  -  T )  <_  B ) ) )
357322, 347, 356syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( ( x  -  T )  e.  ( A [,] B
)  <->  ( ( x  -  T )  e.  RR  /\  A  <_ 
( x  -  T
)  /\  ( x  -  T )  <_  B
) ) )
358355, 357mpbird 232 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  x  e.  ( (
( Q `  i
)  +  T ) (,) ( ( Q `
 ( i  +  1 ) )  +  T ) ) )  ->  ( x  -  T )  e.  ( A [,] B ) )
359274, 275, 277, 358syl3anc 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 ) )
360274, 359jca 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 ) ) )
361 eleq1 2539 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  (
y  e.  ( A [,] B )  <->  ( x  -  T )  e.  ( A [,] B ) ) )
362361anbi2d 703 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  T )  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  ( x  -  T
)  e.  ( A [,] B ) ) ) )
363 oveq1 6302 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  -  T )  ->  (
y  +  T )  =  ( ( x  -  T )  +  T ) )
364363fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  ( F `  ( y  +  T ) )  =  ( F `  (
( x  -  T
)  +  T ) ) )
365 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  -  T )  ->  ( F `  y )  =  ( F `  ( x  -  T
) ) )
366364, 365eqeq12d 2489 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  T )  ->  (
( F `  (
y  +  T ) )  =  ( F `
 y )  <->  ( F `  ( ( x  -  T )  +  T
) )  =  ( F `  ( x  -  T ) ) ) )
367362, 366imbi12d 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 ) ) ) ) )
368247a1i 11 . . . . . . . . . . . . 13  |-  ( y  e.  RR  ->  (
( ph  /\  y  e.  ( A [,] B
) )  ->  ( F `  ( y  +  T ) )  =  ( F `  y
) ) )
369367, 368vtoclga 3182 . . . . . . . . . . . 12  |-  ( ( x  -  T )  e.  RR  ->  (
( ph  /\  (
x  -  T )  e.  ( A [,] B ) )  -> 
( F `  (
( x  -  T
)  +  T ) )  =  ( F `
 ( x  -  T ) ) ) )
370321, 360, 369sylc 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 ) ) )
371277, 278syl 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 )
37270sseli 3505 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  x  e.  CC )
373372adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
37473adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
375373, 374npcand 9946 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  -  T )  +  T )  =  x )
376375fveq2d 5876 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( ( x  -  T )  +  T ) )  =  ( F `  x
) )
377274, 371, 376syl2anc 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 ) )
378320, 370, 3773eqtr2rd 2515 . . . . . . . . . 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 ) ) )
379378mpteq2dva 4539 . . . . . . . . 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 ) ) ) )
380268, 273, 3793eqtrd 2512 . . . . . . . 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 ) ) ) )
381 ioosscn 31414 . . . . . . . . . . 11  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
382381a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
383 nfcv 2629 . . . . . . . . . . 11  |-  F/_ w CC
384 nfcv 2629 . . . . . . . . . . 11  |-  F/_ x CC
385 nfv 1683 . . . . . . . . . . 11  |-  F/ x E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )
386 nfv 1683 . . . . . . . . . . 11  |-  F/ w E. y  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( y  +  T )
387 eqeq1 2471 . . . . . . . . . . . . 13  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
388387rexbidv 2978 . . . . . . . . . . . 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 ) ) )
389 nfv 1683 . . . . . . . . . . . . . 14  |-  F/ y  x  =  ( z  +  T )
390 nfv 1683 . . . . . . . . . . . . . 14  |-  F/ z  x  =  ( y  +  T )
391 oveq1 6302 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
392391eqeq2d 2481 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
393389, 390, 392cbvrex 3090 . . . . . . . . . . . . 13  |-  ( E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) )
394393a1i 11 . . . . . . . . . . . 12  |-  ( w  =  x  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) ) )
395388, 394bitrd 253 . . . . . . . . . . 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 ) ) )
396383, 384, 385, 386, 395cbvrab 3116 . . . . . . . . . 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 ) }
397 eqid 2467 . . . . . . . . . 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 ) ) )
398382, 284, 396, 23, 397cncfshift 31535 . . . . . . . . 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 ) )
399397a1i 11 . . . . . . . . . 10  |-  ( (
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 ) ) )  =  ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
x  -  T ) ) ) )
400271eqcomd 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  =  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
401400oveq1d 6310 . . . . . . . . . 10  |-  ( (
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 ) )
402399, 401eleq12d 2549 . . . . . . . . 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 )  <->  ( 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 ) ) )
403398, 402mpbid 210 . . . . . . . 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 ) )
404380, 403eqeltrd 2555 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )