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

Theorem fourierdlem81 37991
Description: The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by its period  T. In this lemma,  T is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem81.a  |-  ( ph  ->  A  e.  RR )
fourierdlem81.b  |-  ( ph  ->  B  e.  RR )
fourierdlem81.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 ) ) ) } )
fourierdlem81.m  |-  ( ph  ->  M  e.  NN )
fourierdlem81.t  |-  ( ph  ->  T  e.  RR+ )
fourierdlem81.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem81.fper  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
fourierdlem81.s  |-  S  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  +  T
) )
fourierdlem81.f  |-  ( ph  ->  F : RR --> CC )
fourierdlem81.cncf  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem81.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem81.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
fourierdlem81.g  |-  G  =  ( x  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
fourierdlem81.h  |-  H  =  ( x  e.  ( ( S `  i
) [,] ( S `
 ( i  +  1 ) ) ) 
|->  ( G `  (
x  -  T ) ) )
Assertion
Ref Expression
fourierdlem81  |-  ( 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, G    x, L    i, M, m, p    x, M    Q, i, p    x, Q    x, R    S, i, x    T, i, x    ph, i, x
Allowed substitution hints:    ph( m, p)    P( x, i, m, p)    Q( m)    R( i, m, p)    S( m, p)    T( m, p)    F( m, p)    G( i, m, p)    H( x, i, m, p)    L( i, m, p)

Proof of Theorem fourierdlem81
Dummy variables  y  w  z  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem81.q . . . . . . . . 9  |-  ( ph  ->  Q  e.  ( P `
 M ) )
2 fourierdlem81.m . . . . . . . . . 10  |-  ( ph  ->  M  e.  NN )
3 fourierdlem81.p . . . . . . . . . . 11  |-  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 ) ) ) } )
43fourierdlem2 37911 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
52, 4syl 17 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
61, 5mpbid 213 . . . . . . . 8  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
76simprd 464 . . . . . . 7  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
87simpld 460 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
98simpld 460 . . . . 5  |-  ( ph  ->  ( Q `  0
)  =  A )
109eqcomd 2430 . . . 4  |-  ( ph  ->  A  =  ( Q `
 0 ) )
118simprd 464 . . . . 5  |-  ( ph  ->  ( Q `  M
)  =  B )
1211eqcomd 2430 . . . 4  |-  ( ph  ->  B  =  ( Q `
 M ) )
1310, 12oveq12d 6323 . . 3  |-  ( ph  ->  ( A [,] B
)  =  ( ( Q `  0 ) [,] ( Q `  M ) ) )
1413itgeq1d 37773 . 2  |-  ( ph  ->  S. ( A [,] B ) ( F `
 x )  _d x  =  S. ( ( Q `  0
) [,] ( Q `
 M ) ) ( F `  x
)  _d x )
15 0zd 10956 . . 3  |-  ( ph  ->  0  e.  ZZ )
16 nnuz 11201 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
17 0p1e1 10728 . . . . . 6  |-  ( 0  +  1 )  =  1
1817fveq2i 5884 . . . . 5  |-  ( ZZ>= `  ( 0  +  1 ) )  =  (
ZZ>= `  1 )
1916, 18eqtr4i 2454 . . . 4  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
202, 19syl6eleq 2517 . . 3  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 0  +  1 ) ) )
216simpld 460 . . . 4  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
22 reex 9637 . . . . . 6  |-  RR  e.  _V
2322a1i 11 . . . . 5  |-  ( ph  ->  RR  e.  _V )
24 ovex 6333 . . . . . 6  |-  ( 0 ... M )  e. 
_V
2524a1i 11 . . . . 5  |-  ( ph  ->  ( 0 ... M
)  e.  _V )
2623, 25elmapd 7497 . . . 4  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
Q : ( 0 ... M ) --> RR ) )
2721, 26mpbid 213 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
287simprd 464 . . . 4  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
2928r19.21bi 2791 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
30 fourierdlem81.f . . . . 5  |-  ( ph  ->  F : RR --> CC )
3130adantr 466 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  F : RR --> CC )
32 fourierdlem81.a . . . . . . 7  |-  ( ph  ->  A  e.  RR )
339, 32eqeltrd 2507 . . . . . 6  |-  ( ph  ->  ( Q `  0
)  e.  RR )
34 fourierdlem81.b . . . . . . 7  |-  ( ph  ->  B  e.  RR )
3511, 34eqeltrd 2507 . . . . . 6  |-  ( ph  ->  ( Q `  M
)  e.  RR )
3633, 35iccssred 37551 . . . . 5  |-  ( ph  ->  ( ( Q ` 
0 ) [,] ( Q `  M )
)  C_  RR )
3736sselda 3464 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  x  e.  RR )
3831, 37ffvelrnd 6038 . . 3  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( F `  x )  e.  CC )
3927adantr 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
40 elfzofz 11942 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
4140adantl 467 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
4239, 41ffvelrnd 6038 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
43 fzofzp1 12014 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
4443adantl 467 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
4539, 44ffvelrnd 6038 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
4630feqmptd 5934 . . . . . . . 8  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
4746reseq1d 5123 . . . . . . 7  |-  ( ph  ->  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( x  e.  RR  |->  ( F `  x ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
4847adantr 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( x  e.  RR  |->  ( F `  x ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
49 ioossre 11703 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
5049a1i 11 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
5150resmptd 5175 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( x  e.  RR  |->  ( F `
 x ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) ) )
5248, 51eqtr2d 2464 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
53 fourierdlem81.cncf . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
54 fourierdlem81.l . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
55 fourierdlem81.r . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
5642, 45, 53, 54, 55iblcncfioo 37795 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  L^1 )
5752, 56eqeltrd 2507 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
5830ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> CC )
5942, 45iccssred 37551 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  RR )
6059sselda 3464 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
6158, 60ffvelrnd 6038 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
6242, 45, 57, 61ibliooicc 37788 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
6315, 20, 27, 29, 38, 62itgspltprt 37796 . 2  |-  ( ph  ->  S. ( ( Q `
 0 ) [,] ( Q `  M
) ) ( F `
 x )  _d x  =  sum_ i  e.  ( 0..^ M ) S. ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) ( F `
 x )  _d x )
64 fourierdlem81.s . . . . . . . 8  |-  S  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  +  T
) )
6564a1i 11 . . . . . . 7  |-  ( ph  ->  S  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) ) )
66 fveq2 5881 . . . . . . . . 9  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
6766oveq1d 6320 . . . . . . . 8  |-  ( i  =  0  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
6867adantl 467 . . . . . . 7  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
692nnnn0d 10932 . . . . . . . . 9  |-  ( ph  ->  M  e.  NN0 )
70 nn0uz 11200 . . . . . . . . 9  |-  NN0  =  ( ZZ>= `  0 )
7169, 70syl6eleq 2517 . . . . . . . 8  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
72 eluzfz1 11813 . . . . . . . 8  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
7371, 72syl 17 . . . . . . 7  |-  ( ph  ->  0  e.  ( 0 ... M ) )
74 fourierdlem81.t . . . . . . . . 9  |-  ( ph  ->  T  e.  RR+ )
7574rpred 11348 . . . . . . . 8  |-  ( ph  ->  T  e.  RR )
7633, 75readdcld 9677 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  e.  RR )
7765, 68, 73, 76fvmptd 5970 . . . . . 6  |-  ( ph  ->  ( S `  0
)  =  ( ( Q `  0 )  +  T ) )
789oveq1d 6320 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  =  ( A  +  T ) )
7977, 78eqtr2d 2464 . . . . 5  |-  ( ph  ->  ( A  +  T
)  =  ( S `
 0 ) )
80 fveq2 5881 . . . . . . . . 9  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
8180oveq1d 6320 . . . . . . . 8  |-  ( i  =  M  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
8281adantl 467 . . . . . . 7  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
83 eluzfz2 11814 . . . . . . . 8  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
8471, 83syl 17 . . . . . . 7  |-  ( ph  ->  M  e.  ( 0 ... M ) )
8535, 75readdcld 9677 . . . . . . 7  |-  ( ph  ->  ( ( Q `  M )  +  T
)  e.  RR )
8665, 82, 84, 85fvmptd 5970 . . . . . 6  |-  ( ph  ->  ( S `  M
)  =  ( ( Q `  M )  +  T ) )
8711oveq1d 6320 . . . . . 6  |-  ( ph  ->  ( ( Q `  M )  +  T
)  =  ( B  +  T ) )
8886, 87eqtr2d 2464 . . . . 5  |-  ( ph  ->  ( B  +  T
)  =  ( S `
 M ) )
8979, 88oveq12d 6323 . . . 4  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  =  ( ( S `  0 ) [,] ( S `  M ) ) )
9089itgeq1d 37773 . . 3  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( ( S `  0
) [,] ( S `
 M ) ) ( F `  x
)  _d x )
9127ffvelrnda 6037 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
9275adantr 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  T  e.  RR )
9391, 92readdcld 9677 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  +  T )  e.  RR )
9493, 64fmptd 6061 . . . 4  |-  ( ph  ->  S : ( 0 ... M ) --> RR )
9575adantr 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  RR )
9642, 45, 95, 29ltadd1dd 10231 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) )
9740, 93sylan2 476 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
9864fvmpt2 5973 . . . . . 6  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  +  T
)  e.  RR )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
9941, 97, 98syl2anc 665 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
100 fveq2 5881 . . . . . . . . . 10  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
101100oveq1d 6320 . . . . . . . . 9  |-  ( i  =  j  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 j )  +  T ) )
102101cbvmptv 4516 . . . . . . . 8  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  +  T ) )
10364, 102eqtri 2451 . . . . . . 7  |-  S  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  +  T
) )
104103a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  +  T ) ) )
105 fveq2 5881 . . . . . . . 8  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
106105oveq1d 6320 . . . . . . 7  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
107106adantl 467 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
10845, 95readdcld 9677 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
109104, 107, 44, 108fvmptd 5970 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  +  T ) )
11096, 99, 1093brtr4d 4454 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  <  ( S `  ( i  +  1 ) ) )
11130adantr 466 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  F : RR --> CC )
11277, 76eqeltrd 2507 . . . . . . . 8  |-  ( ph  ->  ( S `  0
)  e.  RR )
113112adantr 466 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( S `  0 )  e.  RR )
11486, 85eqeltrd 2507 . . . . . . . 8  |-  ( ph  ->  ( S `  M
)  e.  RR )
115114adantr 466 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( S `  M )  e.  RR )
116113, 115iccssred 37551 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  (
( S `  0
) [,] ( S `
 M ) ) 
C_  RR )
117 simpr 462 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )
118116, 117sseldd 3465 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  x  e.  RR )
119111, 118ffvelrnd 6038 . . . 4  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( F `  x )  e.  CC )
12099, 97eqeltrd 2507 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  e.  RR )
121109, 108eqeltrd 2507 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
122 ioosscn 37540 . . . . . . . . 9  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
123122a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
124 eqeq1 2426 . . . . . . . . . . 11  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
125124rexbidv 2936 . . . . . . . . . 10  |-  ( w  =  x  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  <->  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) ) )
126 oveq1 6312 . . . . . . . . . . . 12  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
127126eqeq2d 2436 . . . . . . . . . . 11  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
128127cbvrexv 3055 . . . . . . . . . 10  |-  ( E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) )
129125, 128syl6bb 264 . . . . . . . . 9  |-  ( w  =  x  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) ) )
130129cbvrabv 3079 . . . . . . . 8  |-  { 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 ) }
131 fdm 5750 . . . . . . . . . . . 12  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
13230, 131syl 17 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  RR )
133132feq2d 5733 . . . . . . . . . 10  |-  ( ph  ->  ( F : dom  F --> CC  <->  F : RR --> CC ) )
13430, 133mpbird 235 . . . . . . . . 9  |-  ( ph  ->  F : dom  F --> CC )
135134adantr 466 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : dom  F --> CC )
136 elioore 11673 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  RR )
137136adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  RR )
13875adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
139137, 138readdcld 9677 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  e.  RR )
140139adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  e.  RR )
1411403adant3 1025 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  (
z  +  T )  e.  RR )
142 simp3 1007 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  w  =  ( z  +  T ) )
1431323ad2ant1 1026 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  dom  F  =  RR )
1441433adant1r 1257 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  dom  F  =  RR )
145141, 142, 1443eltr4d 2522 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  w  e.  dom  F )
1461453exp 1204 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( w  =  ( z  +  T )  ->  w  e.  dom  F ) ) )
147146adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  w  e.  CC )  ->  (
z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  -> 
( w  =  ( z  +  T )  ->  w  e.  dom  F ) ) )
148147rexlimdv 2912 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  w  e.  CC )  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  ->  w  e.  dom  F ) )
149148ralrimiva 2836 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. w  e.  CC  ( E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  ->  w  e.  dom  F ) )
150 rabss 3538 . . . . . . . . 9  |-  ( { w  e.  CC  |  E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } 
C_  dom  F  <->  A. w  e.  CC  ( E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T )  ->  w  e.  dom  F ) )
151149, 150sylibr 215 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  C_  dom  F )
152 simpll 758 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
15332rexrd 9697 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR* )
154153ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
15534rexrd 9697 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR* )
156155ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
1573, 2, 1fourierdlem15 37924 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
158157ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
159 simplr 760 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
160 ioossicc 11727 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
161160sseli 3460 . . . . . . . . . . 11  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
162161adantl 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
163154, 156, 158, 159, 162fourierdlem1 37910 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( A [,] B
) )
164 fourierdlem81.fper . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
165152, 163, 164syl2anc 665 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
166123, 95, 130, 135, 151, 165, 53cncfperiod 37696 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  { w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  e.  ( { w  e.  CC  |  E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) }
-cn-> CC ) )
167125elrab 3228 . . . . . . . . . . . . 13  |-  ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  <->  ( x  e.  CC  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) ) )
168167simprbi 465 . . . . . . . . . . . 12  |-  ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  ->  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
169 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
170 nfv 1755 . . . . . . . . . . . . . . . 16  |-  F/ z ( ph  /\  i  e.  ( 0..^ M ) )
171 nfre1 2883 . . . . . . . . . . . . . . . 16  |-  F/ z E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T )
172170, 171nfan 1988 . . . . . . . . . . . . . . 15  |-  F/ z ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
173 nfv 1755 . . . . . . . . . . . . . . 15  |-  F/ z ( x  e.  RR  /\  ( S `  i
)  <  x  /\  x  <  ( S `  ( i  +  1 ) ) )
174 simp3 1007 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  =  ( z  +  T ) )
1751393adant3 1025 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
z  +  T )  e.  RR )
176174, 175eqeltrd 2507 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  e.  RR )
1771763adant1r 1257 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  e.  RR )
17842adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
179136adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  RR )
18075ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
181 simpr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
18242rexrd 9697 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
183182adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
18445rexrd 9697 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
185184adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
186 elioo2 11684 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR* )  ->  (
z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( z  e.  RR  /\  ( Q `
 i )  < 
z  /\  z  <  ( Q `  ( i  +  1 ) ) ) ) )
187183, 185, 186syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( z  e.  RR  /\  ( Q `
 i )  < 
z  /\  z  <  ( Q `  ( i  +  1 ) ) ) ) )
188181, 187mpbid 213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  e.  RR  /\  ( Q `  i )  <  z  /\  z  <  ( Q `  (
i  +  1 ) ) ) )
189188simp2d 1018 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  z )
190178, 179, 180, 189ltadd1dd 10231 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
)  +  T )  <  ( z  +  T ) )
1911903adant3 1025 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
( Q `  i
)  +  T )  <  ( z  +  T ) )
192993ad2ant1 1026 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  i )  =  ( ( Q `
 i )  +  T ) )
193 simp3 1007 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  =  ( z  +  T ) )
194191, 192, 1933brtr4d 4454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  i )  <  x )
19545adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
196188simp3d 1019 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  <  ( Q `  (
i  +  1 ) ) )
197179, 195, 180, 196ltadd1dd 10231 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  <  ( ( Q `
 ( i  +  1 ) )  +  T ) )
1981973adant3 1025 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
z  +  T )  <  ( ( Q `
 ( i  +  1 ) )  +  T ) )
1991093ad2ant1 1026 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
200198, 193, 1993brtr4d 4454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  <  ( S `  (
i  +  1 ) ) )
201177, 194, 2003jca 1185 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
x  e.  RR  /\  ( S `  i )  <  x  /\  x  <  ( S `  (
i  +  1 ) ) ) )
2022013exp 1204 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( x  =  ( z  +  T )  ->  (
x  e.  RR  /\  ( S `  i )  <  x  /\  x  <  ( S `  (
i  +  1 ) ) ) ) ) )
203202adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( x  =  ( z  +  T )  ->  (
x  e.  RR  /\  ( S `  i )  <  x  /\  x  <  ( S `  (
i  +  1 ) ) ) ) ) )
204172, 173, 203rexlimd 2906 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( E. z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) x  =  ( z  +  T
)  ->  ( x  e.  RR  /\  ( S `
 i )  < 
x  /\  x  <  ( S `  ( i  +  1 ) ) ) ) )
205169, 204mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( x  e.  RR  /\  ( S `
 i )  < 
x  /\  x  <  ( S `  ( i  +  1 ) ) ) )
206120rexrd 9697 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  e.  RR* )
207206adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( S `  i )  e.  RR* )
208121rexrd 9697 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
209208adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
210 elioo2 11684 . . . . . . . . . . . . . 14  |-  ( ( ( S `  i
)  e.  RR*  /\  ( S `  ( i  +  1 ) )  e.  RR* )  ->  (
x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  <->  ( x  e.  RR  /\  ( S `
 i )  < 
x  /\  x  <  ( S `  ( i  +  1 ) ) ) ) )
211207, 209, 210syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  <->  ( x  e.  RR  /\  ( S `
 i )  < 
x  /\  x  <  ( S `  ( i  +  1 ) ) ) ) )
212205, 211mpbird 235 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
213168, 212sylan2 476 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
214 elioore 11673 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  ->  x  e.  RR )
215214recnd 9676 . . . . . . . . . . . . 13  |-  ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  ->  x  e.  CC )
216215adantl 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  CC )
217182adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
218184adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
219214adantl 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
22075adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
221219, 220resubcld 10054 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  RR )
222221adantlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  RR )
22399oveq1d 6320 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i )  -  T )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
22442recnd 9676 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
22595recnd 9676 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  CC )
226224, 225pncand 9994 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  =  ( Q `  i ) )
227223, 226eqtr2d 2464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( S `  i
)  -  T ) )
228227adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  =  ( ( S `
 i )  -  T ) )
229120adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR )
230214adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
23175ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
232 simpr 462 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
233206adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR* )
234208adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
235233, 234, 210syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  <->  ( x  e.  RR  /\  ( S `
 i )  < 
x  /\  x  <  ( S `  ( i  +  1 ) ) ) ) )
236232, 235mpbid 213 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  e.  RR  /\  ( S `  i )  <  x  /\  x  <  ( S `  (
i  +  1 ) ) ) )
237236simp2d 1018 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  <  x )
238229, 230, 231, 237ltsub1dd 10232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( S `  i
)  -  T )  <  ( x  -  T ) )
239228, 238eqbrtrd 4444 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( x  -  T
) )
240121adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
241236simp3d 1019 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  <  ( S `  (
i  +  1 ) ) )
242230, 240, 231, 241ltsub1dd 10232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  <  ( ( S `
 ( i  +  1 ) )  -  T ) )
243109oveq1d 6320 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 ( i  +  1 ) )  -  T )  =  ( ( ( Q `  ( i  +  1 ) )  +  T
)  -  T ) )
24445recnd 9676 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
245244, 225pncand 9994 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
246243, 245eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 ( i  +  1 ) )  -  T )  =  ( Q `  ( i  +  1 ) ) )
247246adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( S `  (
i  +  1 ) )  -  T )  =  ( Q `  ( i  +  1 ) ) )
248242, 247breqtrd 4448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  <  ( Q `  ( i  +  1 ) ) )
249217, 218, 222, 239, 248eliood 37544 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
250219recnd 9676 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  CC )
251220recnd 9676 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  CC )
252250, 251npcand 9997 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( x  -  T
)  +  T )  =  x )
253252eqcomd 2430 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  =  ( ( x  -  T )  +  T ) )
254253adantlr 719 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  =  ( ( x  -  T )  +  T ) )
255 oveq1 6312 . . . . . . . . . . . . . . 15  |-  ( z  =  ( x  -  T )  ->  (
z  +  T )  =  ( ( x  -  T )  +  T ) )
256255eqeq2d 2436 . . . . . . . . . . . . . 14  |-  ( z  =  ( x  -  T )  ->  (
x  =  ( z  +  T )  <->  x  =  ( ( x  -  T )  +  T
) ) )
257256rspcev 3182 . . . . . . . . . . . . 13  |-  ( ( ( x  -  T
)  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( (
x  -  T )  +  T ) )  ->  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T ) )
258249, 254, 257syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
259216, 258, 167sylanbrc 668 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )
260213, 259impbida 840 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) }  <-> 
x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) ) )
261260eqrdv 2419 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  =  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
262261reseq2d 5124 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  { w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  =  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) ) )
26330adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
264 ioossre 11703 . . . . . . . . . 10  |-  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  C_  RR
265264a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  C_  RR )
266263, 265feqresmpt 5935 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  =  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) ) )
267262, 266eqtrd 2463 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  { w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  =  ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  |->  ( F `
 x ) ) )
268261oveq1d 6320 . . . . . . 7  |-  ( (
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 ) )
269166, 267, 2683eltr3d 2521 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  ( ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) ) -cn-> CC ) )
27049, 132syl5sseqr 3513 . . . . . . . . 9  |-  ( ph  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  dom  F )
271270adantr 466 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
272 eqid 2422 . . . . . . . 8  |-  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  =  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }
273 simpll 758 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
274153ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
275155ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
276157ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
277 simplr 760 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
278160, 181sseldi 3462 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
279274, 275, 276, 277, 278fourierdlem1 37910 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( A [,] B
) )
280 eleq1 2495 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
x  e.  ( A [,] B )  <->  z  e.  ( A [,] B ) ) )
281280anbi2d 708 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  z  e.  ( A [,] B ) ) ) )
282 oveq1 6312 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
x  +  T )  =  ( z  +  T ) )
283282fveq2d 5885 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( F `  ( x  +  T ) )  =  ( F `  (
z  +  T ) ) )
284 fveq2 5881 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
285283, 284eqeq12d 2444 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( z  +  T
) )  =  ( F `  z ) ) )
286281, 285imbi12d 321 . . . . . . . . . 10  |-  ( x  =  z  ->  (
( ( ph  /\  x  e.  ( A [,] B ) )  -> 
( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( F `  (
z  +  T ) )  =  ( F `
 z ) ) ) )
287286, 164chvarv 2072 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( F `  ( z  +  T
) )  =  ( F `  z ) )
288273, 279, 287syl2anc 665 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( z  +  T ) )  =  ( F `  z
) )
289135, 123, 271, 225, 272, 151, 288, 54limcperiod 37648 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) } ) lim CC  (
( Q `  (
i  +  1 ) )  +  T ) ) )
290109eqcomd 2430 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  =  ( S `  ( i  +  1 ) ) )
291267, 290oveq12d 6323 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  { w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } ) lim CC  ( ( Q `  ( i  +  1 ) )  +  T ) )  =  ( ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  |->  ( F `
 x ) ) lim
CC  ( S `  ( i  +  1 ) ) ) )
292289, 291eleqtrd 2509 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( x  e.  ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) lim CC  ( S `  ( i  +  1 ) ) ) )
293135, 123, 271, 225, 272, 151, 288, 55limcperiod 37648 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) } ) lim CC  (
( Q `  i
)  +  T ) ) )
29499eqcomd 2430 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  =  ( S `  i ) )
295267, 294oveq12d 6323 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  { w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } ) lim CC  ( ( Q `  i )  +  T ) )  =  ( ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  |->  ( F `
 x ) ) lim
CC  ( S `  i ) ) )
296293, 295eleqtrd 2509 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( x  e.  ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) lim CC  ( S `  i )
) )
297120, 121, 269, 292, 296iblcncfioo 37795 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
29830ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  F : RR --> CC )
299120adantr 466 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR )
300121adantr 466 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
301 simpr 462 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )
302 eliccre 37552 . . . . . . 7  |-  ( ( ( S `  i
)  e.  RR  /\  ( S `  ( i  +  1 ) )  e.  RR  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
303299, 300, 301, 302syl3anc 1264 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
304298, 303ffvelrnd 6038 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
305120, 121, 297, 304ibliooicc 37788 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
30615, 20, 94, 110, 119, 305itgspltprt 37796 . . 3  |-  ( ph  ->  S. ( ( S `
 0 ) [,] ( S `  M
) ) ( F `
 x )  _d x  =  sum_ i  e.  ( 0..^ M ) S. ( ( S `
 i ) [,] ( S `  (
i  +  1 ) ) ) ( F `
 x )  _d x )
307 iftrue 3917 . . . . . . . . . . . 12  |-  ( x  =  ( S `  i )  ->  if ( x  =  ( S `  i ) ,  R ,  if ( x  =  ( S `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( S `  i ) (,) ( S `  (
i  +  1 ) ) ) ) `  x ) ) )  =  R )
308307adantl 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  =  ( S `  i
) )  ->  if ( x  =  ( S `  i ) ,  R ,  if ( x  =  ( S `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( S `  i ) (,) ( S `  (
i  +  1 ) ) ) ) `  x ) ) )  =  R )
309 fourierdlem81.g . . . . . . . . . . . . . . 15  |-  G  =  ( x  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
310 iftrue 3917 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( Q `  i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  R )
311 iftrue 3917 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( Q `  i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) )  =  R )
312310, 311eqtr4d 2466 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( Q `  i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  if ( x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) ) )
313312adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  x  =  ( Q `  i ) )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )  =  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) ) )
314 iffalse 3920 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  x  =  ( Q `
 i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )  =  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )
315314adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
316 iftrue 3917 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( Q `  ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  L )
317316adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) )  =  L )
318 iffalse 3920 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  x  =  ( Q `
 i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) )  =  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) )
319318adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) )  =  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
) ) )
320 iftrue 3917 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( Q `  ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  =  L )
321320adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )  =  L )
322319, 321eqtr2d 2464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  L  =  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) ) )
323315, 317, 3223eqtrd 2467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  if ( x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) ) )
324323adantll 718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  if ( x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) ) )
325314ad2antlr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )  =  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )
326 iffalse 3920 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  x  =  ( Q `
 ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  ( F `
 x ) )
327326adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  ( F `
 x ) )
328318ad2antlr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) )  =  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) )
329 iffalse 3920 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  x  =  ( Q `
 ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )
330329adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )
331182ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  e.  RR* )
332184ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
33360ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  x  e.  RR )
33442ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  e.  RR )
33560adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  x  e.  RR )
336182ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  e.  RR* )
337184ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
338 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
339 iccgelb 11698 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
340336, 337, 338, 339syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  <_  x
)
341 neqne 37347 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  =  ( Q `
 i )  ->  x  =/=  ( Q `  i ) )
342341adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  x  =/=  ( Q `  i ) )
343334, 335, 340, 342leneltd 9796 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  <  x
)
344343adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  <  x )
34545ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
346182adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
347184adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
348 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
349 iccleub 11697 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
350346, 347, 348, 349syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
351350ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  x  <_  ( Q `  ( i  +  1 ) ) )
352 neqne 37347 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  =  ( Q `
 ( i  +  1 ) )  ->  x  =/=  ( Q `  ( i  +  1 ) ) )
353352necomd 2691 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  x  =  ( Q `
 ( i  +  1 ) )  -> 
( Q `  (
i  +  1 ) )  =/=  x )
354353adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  =/=  x )
355333, 345, 351, 354leneltd 9796 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  x  <  ( Q `  ( i  +  1 ) ) )
356331, 332, 333, 344, 355eliood 37544 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
357 fvres 5895 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
358356, 357syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
)  =  ( F `
 x ) )
359328, 330, 3583eqtrrd 2468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
(