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

Theorem fourierdlem81 31811
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 31732 . . . . . . . . . 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 2475 . . . 4  |-  ( ph  ->  A  =  ( Q `
 0 ) )
118simprd 463 . . . . 5  |-  ( ph  ->  ( Q `  M
)  =  B )
1211eqcomd 2475 . . . 4  |-  ( ph  ->  B  =  ( Q `
 M ) )
1310, 12oveq12d 6313 . . 3  |-  ( ph  ->  ( A [,] B
)  =  ( ( Q `  0 ) [,] ( Q `  M ) ) )
14 itgeq1 22047 . . 3  |-  ( ( A [,] B )  =  ( ( Q `
 0 ) [,] ( Q `  M
) )  ->  S. ( A [,] B ) ( F `  x
)  _d x  =  S. ( ( Q `
 0 ) [,] ( Q `  M
) ) ( F `
 x )  _d x )
1513, 14syl 16 . 2  |-  ( ph  ->  S. ( A [,] B ) ( F `
 x )  _d x  =  S. ( ( Q `  0
) [,] ( Q `
 M ) ) ( F `  x
)  _d x )
16 0z 10887 . . . 4  |-  0  e.  ZZ
1716a1i 11 . . 3  |-  ( ph  ->  0  e.  ZZ )
18 0p1e1 10659 . . . . . . 7  |-  ( 0  +  1 )  =  1
1918fveq2i 5875 . . . . . 6  |-  ( ZZ>= `  ( 0  +  1 ) )  =  (
ZZ>= `  1 )
20 nnuz 11129 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
2120eqcomi 2480 . . . . . 6  |-  ( ZZ>= ` 
1 )  =  NN
2219, 21eqtr2i 2497 . . . . 5  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
2322a1i 11 . . . 4  |-  ( ph  ->  NN  =  ( ZZ>= `  ( 0  +  1 ) ) )
242, 23eleqtrd 2557 . . 3  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 0  +  1 ) ) )
256simpld 459 . . . 4  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
26 reex 9595 . . . . . 6  |-  RR  e.  _V
2726a1i 11 . . . . 5  |-  ( ph  ->  RR  e.  _V )
28 ovex 6320 . . . . . 6  |-  ( 0 ... M )  e. 
_V
2928a1i 11 . . . . 5  |-  ( ph  ->  ( 0 ... M
)  e.  _V )
30 elmapg 7445 . . . . 5  |-  ( ( RR  e.  _V  /\  ( 0 ... M
)  e.  _V )  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
Q : ( 0 ... M ) --> RR ) )
3127, 29, 30syl2anc 661 . . . 4  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
Q : ( 0 ... M ) --> RR ) )
3225, 31mpbid 210 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
337simprd 463 . . . 4  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
3433r19.21bi 2836 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
35 fourierdlem81.f . . . . 5  |-  ( ph  ->  F : RR --> CC )
3635adantr 465 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  F : RR --> CC )
37 fourierdlem81.a . . . . . . . 8  |-  ( ph  ->  A  e.  RR )
389, 37eqeltrd 2555 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  e.  RR )
39 fourierdlem81.b . . . . . . . 8  |-  ( ph  ->  B  e.  RR )
4011, 39eqeltrd 2555 . . . . . . 7  |-  ( ph  ->  ( Q `  M
)  e.  RR )
41 iccssre 11618 . . . . . . 7  |-  ( ( ( Q `  0
)  e.  RR  /\  ( Q `  M )  e.  RR )  -> 
( ( Q ` 
0 ) [,] ( Q `  M )
)  C_  RR )
4238, 40, 41syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 ) [,] ( Q `  M )
)  C_  RR )
4342adantr 465 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  (
( Q `  0
) [,] ( Q `
 M ) ) 
C_  RR )
44 simpr 461 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )
4543, 44sseldd 3510 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  x  e.  RR )
4636, 45ffvelrnd 6033 . . 3  |-  ( (
ph  /\  x  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( F `  x )  e.  CC )
4732adantr 465 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
48 elfzofz 11823 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
4948adantl 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
5047, 49ffvelrnd 6033 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
51 fzofzp1 11889 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
5251adantl 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
5347, 52ffvelrnd 6033 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
5435feqmptd 5927 . . . . . . . 8  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
5554reseq1d 5278 . . . . . . 7  |-  ( ph  ->  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( x  e.  RR  |->  ( F `  x ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
5655adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( x  e.  RR  |->  ( F `  x ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
57 ioossre 11598 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
5857a1i 11 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
59 resmpt 5329 . . . . . . 7  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  RR  ->  ( ( x  e.  RR  |->  ( F `  x ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) )
6058, 59syl 16 . . . . . 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 ) ) )
61 eqidd 2468 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  =  ( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) )
6256, 60, 613eqtrrd 2513 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
63 fourierdlem81.cncf . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
64 fourierdlem81.l . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
65 fourierdlem81.r . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
6650, 53, 63, 64, 65iblcncfioo 31619 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  L^1 )
6762, 66eqeltrd 2555 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
6835ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> CC )
69 iccssre 11618 . . . . . . 7  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR )  -> 
( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  C_  RR )
7050, 53, 69syl2anc 661 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  RR )
7170sselda 3509 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
7268, 71ffvelrnd 6033 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
7350, 53, 67, 72ibliooicc 31612 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
7417, 24, 32, 34, 46, 73itgspltprt 31620 . 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 )
75 fourierdlem81.s . . . . . . . 8  |-  S  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  +  T
) )
7675a1i 11 . . . . . . 7  |-  ( ph  ->  S  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) ) )
77 fveq2 5872 . . . . . . . . 9  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
7877oveq1d 6310 . . . . . . . 8  |-  ( i  =  0  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
7978adantl 466 . . . . . . 7  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 0 )  +  T ) )
802nnnn0d 10864 . . . . . . . . 9  |-  ( ph  ->  M  e.  NN0 )
81 nn0uz 11128 . . . . . . . . . 10  |-  NN0  =  ( ZZ>= `  0 )
8281a1i 11 . . . . . . . . 9  |-  ( ph  ->  NN0  =  ( ZZ>= ` 
0 ) )
8380, 82eleqtrd 2557 . . . . . . . 8  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
84 eluzfz1 11705 . . . . . . . 8  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
8583, 84syl 16 . . . . . . 7  |-  ( ph  ->  0  e.  ( 0 ... M ) )
86 fourierdlem81.t . . . . . . . . 9  |-  ( ph  ->  T  e.  RR+ )
8786rpred 11268 . . . . . . . 8  |-  ( ph  ->  T  e.  RR )
8838, 87readdcld 9635 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  e.  RR )
8976, 79, 85, 88fvmptd 5962 . . . . . 6  |-  ( ph  ->  ( S `  0
)  =  ( ( Q `  0 )  +  T ) )
909oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  +  T
)  =  ( A  +  T ) )
9189, 90eqtr2d 2509 . . . . 5  |-  ( ph  ->  ( A  +  T
)  =  ( S `
 0 ) )
92 fveq2 5872 . . . . . . . . 9  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
93 eqidd 2468 . . . . . . . . 9  |-  ( i  =  M  ->  T  =  T )
9492, 93oveq12d 6313 . . . . . . . 8  |-  ( i  =  M  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
9594adantl 466 . . . . . . 7  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 M )  +  T ) )
96 eluzfz2 11706 . . . . . . . 8  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
9783, 96syl 16 . . . . . . 7  |-  ( ph  ->  M  e.  ( 0 ... M ) )
9840, 87readdcld 9635 . . . . . . 7  |-  ( ph  ->  ( ( Q `  M )  +  T
)  e.  RR )
9976, 95, 97, 98fvmptd 5962 . . . . . 6  |-  ( ph  ->  ( S `  M
)  =  ( ( Q `  M )  +  T ) )
10011oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( ( Q `  M )  +  T
)  =  ( B  +  T ) )
10199, 100eqtr2d 2509 . . . . 5  |-  ( ph  ->  ( B  +  T
)  =  ( S `
 M ) )
10291, 101oveq12d 6313 . . . 4  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  =  ( ( S `  0 ) [,] ( S `  M ) ) )
103 itgeq1 22047 . . . 4  |-  ( ( ( A  +  T
) [,] ( B  +  T ) )  =  ( ( S `
 0 ) [,] ( S `  M
) )  ->  S. ( ( A  +  T ) [,] ( B  +  T )
) ( F `  x )  _d x  =  S. ( ( S `  0 ) [,] ( S `  M ) ) ( F `  x )  _d x )
104102, 103syl 16 . . 3  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( ( S `  0
) [,] ( S `
 M ) ) ( F `  x
)  _d x )
10532ffvelrnda 6032 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
10687adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  T  e.  RR )
107105, 106readdcld 9635 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  +  T )  e.  RR )
108107, 75fmptd 6056 . . . 4  |-  ( ph  ->  S : ( 0 ... M ) --> RR )
10987adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  RR )
11050, 53, 109ltadd1d 10157 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  < 
( Q `  (
i  +  1 ) )  <->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) ) )
11134, 110mpbid 210 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) )
11249, 107syldan 470 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  e.  RR )
11375fvmpt2 5964 . . . . . . 7  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  +  T
)  e.  RR )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
11449, 112, 113syl2anc 661 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  =  ( ( Q `  i
)  +  T ) )
115 nfcv 2629 . . . . . . . . . 10  |-  F/_ j
( ( Q `  i )  +  T
)
116 nfcv 2629 . . . . . . . . . 10  |-  F/_ i
( ( Q `  j )  +  T
)
117 fveq2 5872 . . . . . . . . . . 11  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
118117oveq1d 6310 . . . . . . . . . 10  |-  ( i  =  j  ->  (
( Q `  i
)  +  T )  =  ( ( Q `
 j )  +  T ) )
119115, 116, 118cbvmpt 4543 . . . . . . . . 9  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  +  T ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  +  T ) )
12075, 119eqtri 2496 . . . . . . . 8  |-  S  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  +  T
) )
121120a1i 11 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  +  T ) ) )
122 fveq2 5872 . . . . . . . . 9  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
123122oveq1d 6310 . . . . . . . 8  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
124123adantl 466 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  +  T )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
12553, 109readdcld 9635 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  e.  RR )
126121, 124, 52, 125fvmptd 5962 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  +  T ) )
127114, 126breq12d 4466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i )  < 
( S `  (
i  +  1 ) )  <->  ( ( Q `
 i )  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) ) )
128111, 127mpbird 232 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  <  ( S `  ( i  +  1 ) ) )
12935adantr 465 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  F : RR --> CC )
13089, 88eqeltrd 2555 . . . . . . . 8  |-  ( ph  ->  ( S `  0
)  e.  RR )
131130adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( S `  0 )  e.  RR )
13299, 98eqeltrd 2555 . . . . . . . 8  |-  ( ph  ->  ( S `  M
)  e.  RR )
133132adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( S `  M )  e.  RR )
134 iccssre 11618 . . . . . . 7  |-  ( ( ( S `  0
)  e.  RR  /\  ( S `  M )  e.  RR )  -> 
( ( S ` 
0 ) [,] ( S `  M )
)  C_  RR )
135131, 133, 134syl2anc 661 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  (
( S `  0
) [,] ( S `
 M ) ) 
C_  RR )
136 simpr 461 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )
137135, 136sseldd 3510 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  x  e.  RR )
138129, 137ffvelrnd 6033 . . . 4  |-  ( (
ph  /\  x  e.  ( ( S ` 
0 ) [,] ( S `  M )
) )  ->  ( F `  x )  e.  CC )
139114, 112eqeltrd 2555 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  e.  RR )
140126, 125eqeltrd 2555 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
141 ioosscn 31414 . . . . . . . . 9  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
142141a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
143 nfcv 2629 . . . . . . . . 9  |-  F/_ w CC
144 nfcv 2629 . . . . . . . . 9  |-  F/_ x CC
145 nfv 1683 . . . . . . . . 9  |-  F/ x E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )
146 nfv 1683 . . . . . . . . 9  |-  F/ w E. y  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( y  +  T )
147 eqeq1 2471 . . . . . . . . . . 11  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
148147rexbidv 2978 . . . . . . . . . 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 ) ) )
149 nfv 1683 . . . . . . . . . . . 12  |-  F/ y  x  =  ( z  +  T )
150 nfv 1683 . . . . . . . . . . . 12  |-  F/ z  x  =  ( y  +  T )
151 oveq1 6302 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
152151eqeq2d 2481 . . . . . . . . . . . 12  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
153149, 150, 152cbvrex 3090 . . . . . . . . . . 11  |-  ( E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) )
154153a1i 11 . . . . . . . . . 10  |-  ( w  =  x  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T )  <->  E. y  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( y  +  T ) ) )
155148, 154bitrd 253 . . . . . . . . 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 ) ) )
156143, 144, 145, 146, 155cbvrab 3116 . . . . . . . 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 ) }
157 fdm 5741 . . . . . . . . . . . 12  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
15835, 157syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  RR )
159 feq2 5720 . . . . . . . . . . 11  |-  ( dom 
F  =  RR  ->  ( F : dom  F --> CC 
<->  F : RR --> CC ) )
160158, 159syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( F : dom  F --> CC  <->  F : RR --> CC ) )
16135, 160mpbird 232 . . . . . . . . 9  |-  ( ph  ->  F : dom  F --> CC )
162161adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : dom  F --> CC )
16357sseli 3505 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  RR )
164163adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  RR )
16587adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
166164, 165readdcld 9635 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  e.  RR )
167166adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  e.  RR )
1681673adant3 1016 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  (
z  +  T )  e.  RR )
169 simp3 998 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  w  =  ( z  +  T ) )
1701583ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  dom  F  =  RR )
1711703adant1r 1221 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  dom  F  =  RR )
172169, 171eleq12d 2549 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  (
w  e.  dom  F  <->  ( z  +  T )  e.  RR ) )
173168, 172mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  w  =  ( z  +  T
) )  ->  w  e.  dom  F )
1741733exp 1195 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( w  =  ( z  +  T )  ->  w  e.  dom  F ) ) )
175174adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  w  e.  CC )  ->  (
z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  -> 
( w  =  ( z  +  T )  ->  w  e.  dom  F ) ) )
176175rexlimdv 2957 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  w  e.  CC )  ->  ( E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T )  ->  w  e.  dom  F ) )
177176ralrimiva 2881 . . . . . . . . 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 ) )
178 rabss 3582 . . . . . . . . 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 ) )
179177, 178sylibr 212 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  C_  dom  F )
180 simpl 457 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
181180adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
18237rexrd 9655 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR* )
183181, 182syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
18439rexrd 9655 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR* )
185181, 184syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
1863, 2, 1fourierdlem15 31745 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
187181, 186syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
188 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
189188adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
190 ioossicc 11622 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
191190sseli 3505 . . . . . . . . . . 11  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
192191adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
193183, 185, 187, 189, 192fourierdlem1 31731 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( A [,] B
) )
194 fourierdlem81.fper . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
195181, 193, 194syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
196142, 109, 156, 162, 179, 195, 63cncfperiod 31540 . . . . . . 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 ) )
197 nfv 1683 . . . . . . . . . . . 12  |-  F/ x
( ph  /\  i  e.  ( 0..^ M ) )
198 simpl 457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( ph  /\  i  e.  ( 0..^ M ) ) )
199148elrab 3266 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
200199simprbi 464 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) )
201200adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  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 ) )
202198, 201jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
{ w  e.  CC  |  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) } )  ->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) ) )
203 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
204 nfv 1683 . . . . . . . . . . . . . . . . . . 19  |-  F/ z ( ph  /\  i  e.  ( 0..^ M ) )
205 nfre1 2928 . . . . . . . . . . . . . . . . . . 19  |-  F/ z E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T )
206204, 205nfan 1875 . . . . . . . . . . . . . . . . . 18  |-  F/ z ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
207 nfv 1683 . . . . . . . . . . . . . . . . . 18  |-  F/ z ( x  e.  RR  /\  ( S `  i
)  <  x  /\  x  <  ( S `  ( i  +  1 ) ) )
208 simp3 998 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  =  ( z  +  T ) )
2091663adant3 1016 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
z  +  T )  e.  RR )
210208, 209eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  e.  RR )
2112103adant1r 1221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  e.  RR )
212 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
21350rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
214213adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
21553rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
216215adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
217 elioo2 11582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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 ) ) ) ) )
218214, 216, 217syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 ) ) ) ) )
219212, 218mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  e.  RR  /\  ( Q `  i )  <  z  /\  z  <  ( Q `  (
i  +  1 ) ) ) )
220219simp2d 1009 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  z )
22150adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
222163adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  RR )
223109adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
224221, 222, 223ltadd1d 10157 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
)  <  z  <->  ( ( Q `  i )  +  T )  <  (
z  +  T ) ) )
225220, 224mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
)  +  T )  <  ( z  +  T ) )
2262253adant3 1016 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
( Q `  i
)  +  T )  <  ( z  +  T ) )
2271143ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  i )  =  ( ( Q `
 i )  +  T ) )
228 simp3 998 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  =  ( z  +  T ) )
229227, 228breq12d 4466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
( S `  i
)  <  x  <->  ( ( Q `  i )  +  T )  <  (
z  +  T ) ) )
230226, 229mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  i )  <  x )
231219simp3d 1010 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  <  ( Q `  (
i  +  1 ) ) )
23253adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
233222, 232, 223ltadd1d 10157 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  <  ( Q `  ( i  +  1 ) )  <->  ( z  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) ) )
234231, 233mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
z  +  T )  <  ( ( Q `
 ( i  +  1 ) )  +  T ) )
2352343adant3 1016 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
z  +  T )  <  ( ( Q `
 ( i  +  1 ) )  +  T ) )
2361263ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  ( S `  ( i  +  1 ) )  =  ( ( Q `
 ( i  +  1 ) )  +  T ) )
237228, 236breq12d 4466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  (
x  <  ( S `  ( i  +  1 ) )  <->  ( z  +  T )  <  (
( Q `  (
i  +  1 ) )  +  T ) ) )
238235, 237mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( z  +  T
) )  ->  x  <  ( S `  (
i  +  1 ) ) )
239211, 230, 2383jca 1176 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) ) )
2402393exp 1195 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) ) ) ) )
241240adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) ) ) )
242206, 207, 241rexlimd 2951 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) ) )
243203, 242mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
244139rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  i )  e.  RR* )
245244adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( S `  i )  e.  RR* )
246140rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
247246adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
248 elioo2 11582 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) ) )
249245, 247, 248syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) ) )
250243, 249mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )  ->  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
251202, 250syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
252251ex 434 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) ) )
253 elioore 11571 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  ->  x  e.  RR )
254 ax-resscn 9561 . . . . . . . . . . . . . . . . . . 19  |-  RR  C_  CC
255254sseli 3505 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  x  e.  CC )
256253, 255syl 16 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  ->  x  e.  CC )
257256adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  CC )
258253adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
25987adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
260258, 259resubcld 9999 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  RR )
261260adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  RR )
262114oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i )  -  T )  =  ( ( ( Q `  i )  +  T
)  -  T ) )
263254, 50sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
264254, 109sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  T  e.  CC )
265263, 264pncand 9943 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  T )  -  T )  =  ( Q `  i ) )
266262, 265eqtr2d 2509 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( S `  i
)  -  T ) )
267266adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  =  ( ( S `
 i )  -  T ) )
268 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
269244adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR* )
270246adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR* )
271269, 270, 248syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) ) ) )
272268, 271mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  e.  RR  /\  ( S `  i )  <  x  /\  x  <  ( S `  (
i  +  1 ) ) ) )
273272simp2d 1009 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  <  x )
274139adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR )
275253adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
276109adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  RR )
277274, 275, 276ltsub1d 10173 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( S `  i
)  <  x  <->  ( ( S `  i )  -  T )  <  (
x  -  T ) ) )
278273, 277mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( S `  i
)  -  T )  <  ( x  -  T ) )
279267, 278eqbrtrd 4473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( x  -  T
) )
280272simp3d 1010 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  <  ( S `  (
i  +  1 ) ) )
281140adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
282275, 281, 276ltsub1d 10173 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  <  ( S `  ( i  +  1 ) )  <->  ( x  -  T )  <  (
( S `  (
i  +  1 ) )  -  T ) ) )
283280, 282mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  <  ( ( S `
 ( i  +  1 ) )  -  T ) )
284126oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 ( i  +  1 ) )  -  T )  =  ( ( ( Q `  ( i  +  1 ) )  +  T
)  -  T ) )
285254, 53sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
286285, 264pncand 9943 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  ( i  +  1 ) )  +  T )  -  T )  =  ( Q `  ( i  +  1 ) ) )
287284, 286eqtrd 2508 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 ( i  +  1 ) )  -  T )  =  ( Q `  ( i  +  1 ) ) )
288287adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( S `  (
i  +  1 ) )  -  T )  =  ( Q `  ( i  +  1 ) ) )
289283, 288breqtrd 4477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  <  ( Q `  ( i  +  1 ) ) )
290261, 279, 2893jca 1176 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( x  -  T
)  e.  RR  /\  ( Q `  i )  <  ( x  -  T )  /\  (
x  -  T )  <  ( Q `  ( i  +  1 ) ) ) )
291213adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
292215adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
293 elioo2 11582 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR* )  ->  (
( x  -  T
)  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( (
x  -  T )  e.  RR  /\  ( Q `  i )  <  ( x  -  T
)  /\  ( x  -  T )  <  ( Q `  ( i  +  1 ) ) ) ) )
294291, 292, 293syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( x  -  T
)  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( (
x  -  T )  e.  RR  /\  ( Q `  i )  <  ( x  -  T
)  /\  ( x  -  T )  <  ( Q `  ( i  +  1 ) ) ) ) )
295290, 294mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  -  T )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
296258, 255syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  e.  CC )
297254, 259sseldi 3507 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  T  e.  CC )
298296, 297npcand 9946 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
( x  -  T
)  +  T )  =  x )
299298eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  =  ( ( x  -  T )  +  T ) )
300299adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  x  =  ( ( x  -  T )  +  T ) )
301 oveq1 6302 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( x  -  T )  ->  (
z  +  T )  =  ( ( x  -  T )  +  T ) )
302301eqeq2d 2481 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( x  -  T )  ->  (
x  =  ( z  +  T )  <->  x  =  ( ( x  -  T )  +  T
) ) )
303302rspcev 3219 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  -  T
)  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  /\  x  =  ( (
x  -  T )  +  T ) )  ->  E. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) x  =  ( z  +  T ) )
304295, 300, 303syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) )
305257, 304jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  ->  (
x  e.  CC  /\  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) x  =  ( z  +  T ) ) )
306305, 199sylibr 212 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) } )
307306ex 434 . . . . . . . . . . . . 13  |-  ( (
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 ) } ) )
308252, 307impbid 191 . . . . . . . . . . . 12  |-  ( (
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 ) ) ) ) )
309197, 308alrimi 1825 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. x ( x  e.  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  <->  x  e.  (
( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) ) )
310 dfcleq 2460 . . . . . . . . . . 11  |-  ( { w  e.  CC  |  E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) }  =  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  <->  A. x
( x  e.  {
w  e.  CC  |  E. z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) w  =  ( z  +  T ) }  <-> 
x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) ) )
311309, 310sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { w  e.  CC  |  E. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) w  =  ( z  +  T ) }  =  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )
312311reseq2d 5279 . . . . . . . . 9  |-  ( (
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 ) ) ) ) )
31335adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> CC )
314 ioossre 11598 . . . . . . . . . . 11  |-  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  C_  RR
315314a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) )  C_  RR )
316313, 315feqresmpt 5928 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) ) )  =  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) ) )
317312, 316eqtrd 2508 . . . . . . . 8  |-  ( (
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 ) ) )
318311oveq1d 6310 . . . . . . . 8  |-  ( (
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 ) )
319317, 318eleq12d 2549 . . . . . . 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 )  <->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  ( ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) ) -cn-> CC ) ) )
320196, 319mpbid 210 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  ( ( ( S `
 i ) (,) ( S `  (
i  +  1 ) ) ) -cn-> CC ) )
32157, 158syl5sseqr 3558 . . . . . . . . 9  |-  ( ph  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  dom  F )
322321adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
323 eqid 2467 . . . . . . . 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 ) }
324 simpll 753 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ph )
325324, 182syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
326324, 184syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
327324, 186syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
328188adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
329190, 212sseldi 3507 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
330325, 326, 327, 328, 329fourierdlem1 31731 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( A [,] B
) )
331 nfv 1683 . . . . . . . . . 10  |-  F/ x
( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( F `  (
z  +  T ) )  =  ( F `
 z ) )
332 eleq1 2539 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
x  e.  ( A [,] B )  <->  z  e.  ( A [,] B ) ) )
333332anbi2d 703 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( ph  /\  x  e.  ( A [,] B
) )  <->  ( ph  /\  z  e.  ( A [,] B ) ) ) )
334 oveq1 6302 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
x  +  T )  =  ( z  +  T ) )
335334fveq2d 5876 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( F `  ( x  +  T ) )  =  ( F `  (
z  +  T ) ) )
336 fveq2 5872 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
337335, 336eqeq12d 2489 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( z  +  T
) )  =  ( F `  z ) ) )
338333, 337imbi12d 320 . . . . . . . . . 10  |-  ( x  =  z  ->  (
( ( ph  /\  x  e.  ( A [,] B ) )  -> 
( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( F `  (
z  +  T ) )  =  ( F `
 z ) ) ) )
339331, 338, 194chvar 1982 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( F `  ( z  +  T
) )  =  ( F `  z ) )
340324, 330, 339syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( z  +  T ) )  =  ( F `  z
) )
341162, 142, 322, 264, 323, 179, 340, 64limcperiod 31493 . . . . . . 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 ) ) )
342126eqcomd 2475 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  T )  =  ( S `  ( i  +  1 ) ) )
343317, 342oveq12d 6313 . . . . . . 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 ) ) ) )
344341, 343eleqtrd 2557 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( x  e.  ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) lim CC  ( S `  ( i  +  1 ) ) ) )
345162, 142, 322, 264, 323, 179, 340, 65limcperiod 31493 . . . . . . 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 ) ) )
346114eqcomd 2475 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  T )  =  ( S `  i ) )
347317, 346oveq12d 6313 . . . . . . 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 ) ) )
348345, 347eleqtrd 2557 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( x  e.  ( ( S `  i
) (,) ( S `
 ( i  +  1 ) ) ) 
|->  ( F `  x
) ) lim CC  ( S `  i )
) )
349139, 140, 320, 344, 348iblcncfioo 31619 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) (,) ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
350313adantr 465 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  F : RR --> CC )
351139adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( S `  i )  e.  RR )
352140adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( S `  ( i  +  1 ) )  e.  RR )
353 simpr 461 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )
354 eliccre 31427 . . . . . . 7  |-  ( ( ( S `  i
)  e.  RR  /\  ( S `  ( i  +  1 ) )  e.  RR  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
355351, 352, 353, 354syl3anc 1228 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
356350, 355ffvelrnd 6033 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
357139, 140, 349, 356ibliooicc 31612 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1 ) ) )  |->  ( F `  x ) )  e.  L^1 )
35817, 24, 108, 128, 138, 357itgspltprt 31620 . . 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 )
359 fourierdlem81.g . . . . . . . . . . . . . . 15  |-  G  =  ( x  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
360359a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  G  =  ( x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) ) )
361 iftrue 3951 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( Q `  i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  R )
362 iftrue 3951 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( Q `  i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) )  =  R )
363362eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( Q `  i )  ->  R  =  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) ) )
364361, 363eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) )
365364adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) ) )
366 iffalse 3954 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  x  =  ( Q `
 i )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )  =  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )
367366adantr 465 . . . . . . . . . . . . . . . . . . 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  +  1 ) ) ,  L ,  ( F `
 x ) ) )
368 iftrue 3951 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( Q `  ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  L )
369368adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) )  =  L )
370 iffalse 3954 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  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 ) ) )
371370adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  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
) ) )
372 iftrue 3951 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( Q `  ( i  +  1 ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  =  L )
373372adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  x  =  ( Q `  i )  /\  x  =  ( Q `  ( i  +  1 ) ) )  ->  if (
x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )  =  L )
374371, 373eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  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 ) ) ) )
375367, 369, 374