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

Theorem fourierdlem81 31859
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 31780 . . . . . . . . . 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 16 . . . . . . . . 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 210 . . . . . . . 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 463 . . . . . . 7  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
87simpld 459 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
98simpld 459 . . . . 5  |-  ( ph  ->  ( Q `  0
)  =  A )
109eqcomd 2451 . . . 4  |-  ( ph  ->  A  =  ( Q `
 0 ) )
118simprd 463 . . . . 5  |-  ( ph  ->  ( Q `  M
)  =  B )
1211eqcomd 2451 . . . 4  |-  ( ph  ->  B  =  ( Q `
 M ) )
1310, 12oveq12d 6299 . . 3  |-  ( ph  ->  ( A [,] B
)  =  ( ( Q `  0 ) [,] ( Q `  M ) ) )
1413itgeq1d 31645 . 2  |-  ( ph  ->  S. ( A [,] B ) ( F `
 x )  _d x  =  S. ( ( Q `  0
) [,] ( Q `
 M ) ) ( F `  x
)  _d x )
15 0zd 10883 . . 3  |-  ( ph  ->  0  e.  ZZ )
16 nnuz 11126 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
17 0p1e1 10654 . . . . . 6  |-  ( 0  +  1 )  =  1
1817fveq2i 5859 . . . . 5  |-  ( ZZ>= `  ( 0  +  1 ) )  =  (
ZZ>= `  1 )
1916, 18eqtr4i 2475 . . . 4  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
202, 19syl6eleq 2541 . . 3  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 0  +  1 ) ) )
216simpld 459 . . . 4  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
22 reex 9586 . . . . . 6  |-  RR  e.  _V
2322a1i 11 . . . . 5  |-  ( ph  ->  RR  e.  _V )
24 ovex 6309 . . . . . 6  |-  ( 0 ... M )  e. 
_V
2524a1i 11 . . . . 5  |-  ( ph  ->  ( 0 ... M
)  e.  _V )
26 elmapg 7435 . . . . 5  |-  ( ( RR  e.  _V  /\  ( 0 ... M
)  e.  _V )  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
Q : ( 0 ... M ) --> RR ) )
2723, 25, 26syl2anc 661 . . . 4  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
Q : ( 0 ... M ) --> RR ) )
2821, 27mpbid 210 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
297simprd 463 . . . 4  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
3029r19.21bi 2812 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
31 fourierdlem81.f . . . . 5  |-  ( ph  ->  F : RR --> CC )
3231adantr 465 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  F : RR --> CC )
33 fourierdlem81.a . . . . . . 7  |-  ( ph  ->  A  e.  RR )
349, 33eqeltrd 2531 . . . . . 6  |-  ( ph  ->  ( Q `  0
)  e.  RR )
35 fourierdlem81.b . . . . . . 7  |-  ( ph  ->  B  e.  RR )
3611, 35eqeltrd 2531 . . . . . 6  |-  ( ph  ->  ( Q `  M
)  e.  RR )
3734, 36iccssred 31475 . . . . 5  |-  ( ph  ->  ( ( Q ` 
0 ) [,] ( Q `  M )
)  C_  RR )
3837sselda 3489 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  x  e.  RR )
3932, 38ffvelrnd 6017 . . 3  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( F `  x )  e.  CC )
4028adantr 465 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
41 elfzofz 11824 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
4241adantl 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
4340, 42ffvelrnd 6017 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
44 fzofzp1 11890 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
4544adantl 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
4640, 45ffvelrnd 6017 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
4731feqmptd 5911 . . . . . . . 8  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
4847reseq1d 5262 . . . . . . 7  |-  ( ph  ->  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( x  e.  RR  |->  ( F `  x ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
4948adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( x  e.  RR  |->  ( F `  x ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
50 ioossre 11596 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
5150a1i 11 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
5251resmptd 5315 . . . . . 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 ) ) )
5349, 52eqtr2d 2485 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
54 fourierdlem81.cncf . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
55 fourierdlem81.l . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
56 fourierdlem81.r . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
5743, 46, 54, 55, 56iblcncfioo 31667 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  L^1 )
5853, 57eqeltrd 2531 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
5931ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> CC )
6043, 46iccssred 31475 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  RR )
6160sselda 3489 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
6259, 61ffvelrnd 6017 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
6343, 46, 58, 62ibliooicc 31660 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
6415, 20, 28, 30, 39, 63itgspltprt 31668 . 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 )
65 fourierdlem81.s . . . . . . . 8  |-  S  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  +  T
) )
6665a1i 11 . . . . . . 7  |-  ( ph  ->  S  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) ) )
67 fveq2 5856 . . . . . . . . 9  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
6867oveq1d 6296 . . . . . . . 8  |-  ( i  =  0  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
6968adantl 466 . . . . . . 7  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
702nnnn0d 10859 . . . . . . . . 9  |-  ( ph  ->  M  e.  NN0 )
71 nn0uz 11125 . . . . . . . . 9  |-  NN0  =  ( ZZ>= `  0 )
7270, 71syl6eleq 2541 . . . . . . . 8  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
73 eluzfz1 11703 . . . . . . . 8  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
7472, 73syl 16 . . . . . . 7  |-  ( ph  ->  0  e.  ( 0 ... M ) )
75 fourierdlem81.t . . . . . . . . 9  |-  ( ph  ->  T  e.  RR+ )
7675rpred 11266 . . . . . . . 8  |-  ( ph  ->  T  e.  RR )
7734, 76readdcld 9626 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  e.  RR )
7866, 69, 74, 77fvmptd 5946 . . . . . 6  |-  ( ph  ->  ( S `  0
)  =  ( ( Q `  0 )  +  T ) )
799oveq1d 6296 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  =  ( A  +  T ) )
8078, 79eqtr2d 2485 . . . . 5  |-  ( ph  ->  ( A  +  T
)  =  ( S `
 0 ) )
81 fveq2 5856 . . . . . . . . 9  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
8281oveq1d 6296 . . . . . . . 8  |-  ( i  =  M  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
8382adantl 466 . . . . . . 7  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
84 eluzfz2 11704 . . . . . . . 8  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
8572, 84syl 16 . . . . . . 7  |-  ( ph  ->  M  e.  ( 0 ... M ) )
8636, 76readdcld 9626 . . . . . . 7  |-  ( ph  ->  ( ( Q `  M )  +  T
)  e.  RR )
8766, 83, 85, 86fvmptd 5946 . . . . . 6  |-  ( ph  ->  ( S `  M
)  =  ( ( Q `  M )  +  T ) )
8811oveq1d 6296 . . . . . 6  |-  ( ph  ->  ( ( Q `  M )  +  T
)  =  ( B  +  T ) )
8987, 88eqtr2d 2485 . . . . 5  |-  ( ph  ->  ( B  +  T
)  =  ( S `
 M ) )
9080, 89oveq12d 6299 . . . 4  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  =  ( ( S `  0 ) [,] ( S `  M ) ) )
9190itgeq1d 31645 . . 3  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( ( S `  0
) [,] ( S `
 M ) ) ( F `  x
)  _d x )
9228ffvelrnda 6016 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
9376adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  T  e.  RR )
9492, 93readdcld 9626 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  +  T )  e.  RR )
9594, 65fmptd 6040 . . . 4  |-  ( ph  ->  S : ( 0 ... M ) --> RR )
9676adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  RR )
9743, 46, 96, 30ltadd1dd 10170 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) )
9841, 94sylan2 474 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
9965fvmpt2 5948 . . . . . 6  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  +  T
)  e.  RR )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
10042, 98, 99syl2anc 661 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
101 fveq2 5856 . . . . . . . . . 10  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
102101oveq1d 6296 . . . . . . . . 9  |-  ( i  =  j  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 j )  +  T ) )
103102cbvmptv 4528 . . . . . . . 8  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  +  T ) )
10465, 103eqtri 2472 . . . . . . 7  |-  S  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  +  T
) )
105104a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  +  T ) ) )
106 fveq2 5856 . . . . . . . 8  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
107106oveq1d 6296 . . . . . . 7  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
108107adantl 466 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
10946, 96readdcld 9626 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
110105, 108, 45, 109fvmptd 5946 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  +  T ) )
11197, 100, 1103brtr4d 4467 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  <  ( S `  ( i  +  1 ) ) )
11231adantr 465 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  F : RR --> CC )
11378, 77eqeltrd 2531 . . . . . . . 8  |-  ( ph  ->  ( S `  0
)  e.  RR )
114113adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( S `  0 )  e.  RR )
11587, 86eqeltrd 2531 . . . . . . . 8  |-  ( ph  ->  ( S `  M
)  e.  RR )
116115adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( S `  M )  e.  RR )
117114, 116iccssred 31475 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  (
( S `  0
) [,] ( S `
 M ) ) 
C_  RR )
118 simpr 461 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )
119117, 118sseldd 3490 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  x  e.  RR )
120112, 119ffvelrnd 6017 . . . 4  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( F `  x )  e.  CC )
121100, 98eqeltrd 2531 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  e.  RR )
122110, 109eqeltrd 2531 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
123 ioosscn 31463 . . . . . . . . 9  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
124123a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
125 eqeq1 2447 . . . . . . . . . . 11  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
126125rexbidv 2954 . . . . . . . . . 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 ) ) )
127 oveq1 6288 . . . . . . . . . . . 12  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
128127eqeq2d 2457 . . . . . . . . . . 11  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
129128cbvrexv 3071 . . . . . . . . . 10  |-  ( E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) )
130126, 129syl6bb 261 . . . . . . . . 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 ) ) )
131130cbvrabv 3094 . . . . . . . 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 ) }
132 fdm 5725 . . . . . . . . . . . 12  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
13331, 132syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  RR )
134133feq2d 5708 . . . . . . . . . 10  |-  ( ph  ->  ( F : dom  F --> CC  <->  F : RR --> CC ) )
13531, 134mpbird 232 . . . . . . . . 9  |-  ( ph  ->  F : dom  F --> CC )
136135adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : dom  F --> CC )
137 elioore 11569 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  RR )
138137adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  RR )
13976adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
140138, 139readdcld 9626 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  e.  RR )
141140adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  e.  RR )
1421413adant3 1017 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  (
z  +  T )  e.  RR )
143 simp3 999 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  w  =  ( z  +  T ) )
1441333ad2ant1 1018 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  dom  F  =  RR )
1451443adant1r 1222 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  dom  F  =  RR )
146142, 143, 1453eltr4d 2546 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  w  e.  dom  F )
1471463exp 1196 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( w  =  ( z  +  T )  ->  w  e.  dom  F ) ) )
148147adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  w  e.  CC )  ->  (
z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  -> 
( w  =  ( z  +  T )  ->  w  e.  dom  F ) ) )
149148rexlimdv 2933 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  w  e.  CC )  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  ->  w  e.  dom  F ) )
150149ralrimiva 2857 . . . . . . . . 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 ) )
151 rabss 3562 . . . . . . . . 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 ) )
152150, 151sylibr 212 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  C_  dom  F )
153 simpll 753 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
15433rexrd 9646 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR* )
155154ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
15635rexrd 9646 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR* )
157156ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
1583, 2, 1fourierdlem15 31793 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
159158ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
160 simplr 755 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
161 ioossicc 11620 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
162161sseli 3485 . . . . . . . . . . 11  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
163162adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
164155, 157, 159, 160, 163fourierdlem1 31779 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( A [,] B
) )
165 fourierdlem81.fper . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
166153, 164, 165syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
167124, 96, 131, 136, 152, 166, 54cncfperiod 31588 . . . . . . 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 ) )
168126elrab 3243 . . . . . . . . . . . . 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 ) ) )
169168simprbi 464 . . . . . . . . . . . 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 ) )
170 simpr 461 . . . . . . . . . . . . . 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 ) )
171 nfv 1694 . . . . . . . . . . . . . . . 16  |-  F/ z ( ph  /\  i  e.  ( 0..^ M ) )
172 nfre1 2904 . . . . . . . . . . . . . . . 16  |-  F/ z E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T )
173171, 172nfan 1914 . . . . . . . . . . . . . . 15  |-  F/ z ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
174 nfv 1694 . . . . . . . . . . . . . . 15  |-  F/ z ( x  e.  RR  /\  ( S `  i
)  <  x  /\  x  <  ( S `  ( i  +  1 ) ) )
175 simp3 999 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  =  ( z  +  T ) )
1761403adant3 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
z  +  T )  e.  RR )
177175, 176eqeltrd 2531 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  e.  RR )
1781773adant1r 1222 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  e.  RR )
17943adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
180137adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  RR )
18176ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
182 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
18343rexrd 9646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
184183adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
18546rexrd 9646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
186185adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
187 elioo2 11580 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
188184, 186, 187syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
189182, 188mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  e.  RR  /\  ( Q `  i )  <  z  /\  z  <  ( Q `  (
i  +  1 ) ) ) )
190189simp2d 1010 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  z )
191179, 180, 181, 190ltadd1dd 10170 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
)  +  T )  <  ( z  +  T ) )
1921913adant3 1017 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
( Q `  i
)  +  T )  <  ( z  +  T ) )
1931003ad2ant1 1018 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  i )  =  ( ( Q `
 i )  +  T ) )
194 simp3 999 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  =  ( z  +  T ) )
195192, 193, 1943brtr4d 4467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  i )  <  x )
19646adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
197189simp3d 1011 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  <  ( Q `  (
i  +  1 ) ) )
198180, 196, 181, 197ltadd1dd 10170 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  <  ( ( Q `
 ( i  +  1 ) )  +  T ) )
1991983adant3 1017 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
z  +  T )  <  ( ( Q `
 ( i  +  1 ) )  +  T ) )
2001103ad2ant1 1018 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
201199, 194, 2003brtr4d 4467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  <  ( S `  (
i  +  1 ) ) )
202178, 195, 2013jca 1177 . . . . . . . . . . . . . . . . 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 ) ) ) )
2032023exp 1196 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
204203adantr 465 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
205173, 174, 204rexlimd 2927 . . . . . . . . . . . . . 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 ) ) ) ) )
206170, 205mpd 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 ) ) ) )
207121rexrd 9646 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  e.  RR* )
208207adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( S `  i )  e.  RR* )
209122rexrd 9646 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
210209adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
211 elioo2 11580 . . . . . . . . . . . . . 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 ) ) ) ) )
212208, 210, 211syl2anc 661 . . . . . . . . . . . . 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 ) ) ) ) )
213206, 212mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
214169, 213sylan2 474 . . . . . . . . . . 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 ) ) ) )
215 elioore 11569 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  ->  x  e.  RR )
216215recnd 9625 . . . . . . . . . . . . 13  |-  ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  ->  x  e.  CC )
217216adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  CC )
218183adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
219185adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
220215adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
22176adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
222220, 221resubcld 9994 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  RR )
223222adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  RR )
224100oveq1d 6296 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i )  -  T )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
22543recnd 9625 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
22696recnd 9625 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  CC )
227225, 226pncand 9937 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  =  ( Q `  i ) )
228224, 227eqtr2d 2485 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( S `  i
)  -  T ) )
229228adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  =  ( ( S `
 i )  -  T ) )
230121adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR )
231215adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
23276ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
233 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
234207adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR* )
235209adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
236234, 235, 211syl2anc 661 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
237233, 236mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  e.  RR  /\  ( S `  i )  <  x  /\  x  <  ( S `  (
i  +  1 ) ) ) )
238237simp2d 1010 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  <  x )
239230, 231, 232, 238ltsub1dd 10171 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( S `  i
)  -  T )  <  ( x  -  T ) )
240229, 239eqbrtrd 4457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( x  -  T
) )
241122adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
242237simp3d 1011 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  <  ( S `  (
i  +  1 ) ) )
243231, 241, 232, 242ltsub1dd 10171 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  <  ( ( S `
 ( i  +  1 ) )  -  T ) )
244110oveq1d 6296 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 ( i  +  1 ) )  -  T )  =  ( ( ( Q `  ( i  +  1 ) )  +  T
)  -  T ) )
24546recnd 9625 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
246245, 226pncand 9937 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
247244, 246eqtrd 2484 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 ( i  +  1 ) )  -  T )  =  ( Q `  ( i  +  1 ) ) )
248247adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( S `  (
i  +  1 ) )  -  T )  =  ( Q `  ( i  +  1 ) ) )
249243, 248breqtrd 4461 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  <  ( Q `  ( i  +  1 ) ) )
250218, 219, 223, 240, 249eliood 31467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
251220recnd 9625 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  CC )
252221recnd 9625 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  CC )
253251, 252npcand 9940 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( x  -  T
)  +  T )  =  x )
254253eqcomd 2451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  =  ( ( x  -  T )  +  T ) )
255254adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  =  ( ( x  -  T )  +  T ) )
256 oveq1 6288 . . . . . . . . . . . . . . 15  |-  ( z  =  ( x  -  T )  ->  (
z  +  T )  =  ( ( x  -  T )  +  T ) )
257256eqeq2d 2457 . . . . . . . . . . . . . 14  |-  ( z  =  ( x  -  T )  ->  (
x  =  ( z  +  T )  <->  x  =  ( ( x  -  T )  +  T
) ) )
258257rspcev 3196 . . . . . . . . . . . . 13  |-  ( ( ( x  -  T
)  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( (
x  -  T )  +  T ) )  ->  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T ) )
259250, 255, 258syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
260217, 259, 168sylanbrc 664 . . . . . . . . . . 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 ) } )
261214, 260impbida 832 . . . . . . . . . 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 ) ) ) ) )
262261eqrdv 2440 . . . . . . . . 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 ) ) ) )
263262reseq2d 5263 . . . . . . . 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 ) ) ) ) )
26431adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
265 ioossre 11596 . . . . . . . . . 10  |-  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  C_  RR
266265a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  C_  RR )
267264, 266feqresmpt 5912 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  =  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) ) )
268263, 267eqtrd 2484 . . . . . . 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 ) ) )
269262oveq1d 6296 . . . . . . 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 ) )
270167, 268, 2693eltr3d 2545 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  ( ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) ) -cn-> CC ) )
27150, 133syl5sseqr 3538 . . . . . . . . 9  |-  ( ph  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  dom  F )
272271adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
273 eqid 2443 . . . . . . . 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 ) }
274 simpll 753 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
275154ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
276156ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
277158ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
278 simplr 755 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
279161, 182sseldi 3487 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
280275, 276, 277, 278, 279fourierdlem1 31779 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( A [,] B
) )
281 eleq1 2515 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
x  e.  ( A [,] B )  <->  z  e.  ( A [,] B ) ) )
282281anbi2d 703 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  z  e.  ( A [,] B ) ) ) )
283 oveq1 6288 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
x  +  T )  =  ( z  +  T ) )
284283fveq2d 5860 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( F `  ( x  +  T ) )  =  ( F `  (
z  +  T ) ) )
285 fveq2 5856 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
286284, 285eqeq12d 2465 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( z  +  T
) )  =  ( F `  z ) ) )
287282, 286imbi12d 320 . . . . . . . . . 10  |-  ( x  =  z  ->  (
( ( ph  /\  x  e.  ( A [,] B ) )  -> 
( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( F `  (
z  +  T ) )  =  ( F `
 z ) ) ) )
288287, 165chvarv 2000 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( F `  ( z  +  T
) )  =  ( F `  z ) )
289274, 280, 288syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( z  +  T ) )  =  ( F `  z
) )
290136, 124, 272, 226, 273, 152, 289, 55limcperiod 31542 . . . . . . 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 ) ) )
291110eqcomd 2451 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  =  ( S `  ( i  +  1 ) ) )
292268, 291oveq12d 6299 . . . . . . 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 ) ) ) )
293290, 292eleqtrd 2533 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( x  e.  ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) lim CC  ( S `  ( i  +  1 ) ) ) )
294136, 124, 272, 226, 273, 152, 289, 56limcperiod 31542 . . . . . . 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 ) ) )
295100eqcomd 2451 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  =  ( S `  i ) )
296268, 295oveq12d 6299 . . . . . . 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 ) ) )
297294, 296eleqtrd 2533 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( x  e.  ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) lim CC  ( S `  i )
) )
298121, 122, 270, 293, 297iblcncfioo 31667 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
29931ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  F : RR --> CC )
300121adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR )
301122adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
302 simpr 461 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )
303 eliccre 31476 . . . . . . 7  |-  ( ( ( S `  i
)  e.  RR  /\  ( S `  ( i  +  1 ) )  e.  RR  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
304300, 301, 302, 303syl3anc 1229 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
305299, 304ffvelrnd 6017 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
306121, 122, 298, 305ibliooicc 31660 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
30715, 20, 95, 111, 120, 306itgspltprt 31668 . . 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 )
308 iftrue 3932 . . . . . . . . . . . 12  |-  ( x  =  ( S `  i )  ->  if ( x  =  ( S `  i ) ,  R ,  if ( x  =  ( S `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( S `  i ) (,) ( S `  (
i  +  1 ) ) ) ) `  x ) ) )  =  R )
309308adantl 466 . . . . . . . . . . 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 )
310 fourierdlem81.g . . . . . . . . . . . . . . 15  |-  G  =  ( x  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
311 iftrue 3932 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( Q `  i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  R )
312 iftrue 3932 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( Q `  i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) )  =  R )
313311, 312eqtr4d 2487 . . . . . . . . . . . . . . . . . 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 ) ) ) )
314313adantl 466 . . . . . . . . . . . . . . . . 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 ) ) ) )
315 iffalse 3935 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
316315adantr 465 . . . . . . . . . . . . . . . . . . . 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 ) ) )
317 iftrue 3932 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( Q `  ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  L )
318317adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) )  =  L )
319 iffalse 3935 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
320319adantr 465 . . . . . . . . . . . . . . . . . . . . 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
) ) )
321 iftrue 3932 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( Q `  ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  =  L )
322321adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )  =  L )
323320, 322eqtr2d 2485 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
324316, 318, 3233eqtrd 2488 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
325324adantll 713 . . . . . . . . . . . . . . . . . 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 ) ) ) )
326315ad2antlr 726 . . . . . . . . . . . . . . . . . . 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 ) ) )
327 iffalse 3935 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  x  =  ( Q `
 ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  ( F `
 x ) )
328327adantl 466 . . . . . . . . . . . . . . . . . . 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 ) )
329319ad2antlr 726 . . . . . . . . . . . . . . . . . . . 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 ) ) )
330 iffalse 3935 . . . . . . . . . . . . . . . . . . . . 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 ) )
331330adantl 466 . . . . . . . . . . . . . . . . . . . 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 ) )
332183ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  e.  RR* )
333185ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 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* )
33461ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  x  e.  RR )
33543ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  e.  RR )
33661adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  x  e.  RR )
337183ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  e.  RR* )
338185ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
339 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
340 iccgelb 11591 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
341337, 338, 339, 340syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  <_  x
)
342 neqne 31388 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  =  ( Q `
 i )  ->  x  =/=  ( Q `  i ) )
343342adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  x  =/=  ( Q `  i ) )
344335, 336, 341, 343leneltd 31443 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  ->  ( Q `  i )  <  x
)
345344adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  <  x )
34646ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 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 )
347183adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
348185adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
349 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
350 iccleub 11590 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
351347, 348, 349, 350syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
352351ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  x  <_  ( Q `  ( i  +  1 ) ) )
353 neqne 31388 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  =  ( Q `
 ( i  +  1 ) )  ->  x  =/=  ( Q `  ( i  +  1 ) ) )
354353necomd 2714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  x  =  ( Q `
 ( i  +  1 ) )  -> 
( Q `  (
i  +  1 ) )  =/=  x )
355354adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  =/=  x )
356334, 346, 352, 355leneltd 31443 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  /\  -.  x  =  ( Q `  i )
)  /\  -.  x  =  ( Q `  ( i  +  1 ) ) )  ->  x  <  ( Q `  ( i  +  1 ) ) )
357332, 333, 334, 345, 356eliood 31467 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
358 fvres 5870 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
359357, 358syl 16 . . . . . . . . . . . . . . . . . . . 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 ) )
360329, 331, 3593eqtrrd 2489 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M )