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

Theorem fourierdlem93 31823
Description: Integral by substitution (the domain is shifted by  X) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem93.1  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem93.2  |-  H  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  -  X
) )
fourierdlem93.3  |-  ( ph  ->  M  e.  NN )
fourierdlem93.4  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem93.5  |-  ( ph  ->  X  e.  RR )
fourierdlem93.6  |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )
fourierdlem93.7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem93.8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem93.9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
Assertion
Ref Expression
fourierdlem93  |-  ( ph  ->  S. ( -u pi [,] pi ) ( F `
 t )  _d t  =  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( F `  ( X  +  s
) )  _d s )
Distinct variable groups:    i, F, s, t    i, H, s, t    t, L    i, M, m, p    M, s, t    Q, i, p    Q, s, t    t, R    i, X, s, t    ph, i,
s, t
Allowed substitution hints:    ph( m, p)    P( t, i, m, s, p)    Q( m)    R( i, m, s, p)    F( m, p)    H( m, p)    L( i, m, s, p)    X( m, p)

Proof of Theorem fourierdlem93
Dummy variables  r  x  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem93.4 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( P `
 M ) )
2 fourierdlem93.3 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
3 fourierdlem93.1 . . . . . . . . . . . . 13  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
43fourierdlem2 31732 . . . . . . . . . . . 12  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
52, 4syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
61, 5mpbid 210 . . . . . . . . . 10  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
76simprd 463 . . . . . . . . 9  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
87simpld 459 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
0 )  =  -u pi  /\  ( Q `  M )  =  pi ) )
98simpld 459 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
108simprd 463 . . . . . . 7  |-  ( ph  ->  ( Q `  M
)  =  pi )
117simprd 463 . . . . . . 7  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
129, 10, 113jca 1176 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  =  -u pi  /\  ( Q `  M )  =  pi 
/\  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) ) )
1312simp1d 1008 . . . . 5  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
1413eqcomd 2475 . . . 4  |-  ( ph  -> 
-u pi  =  ( Q `  0 ) )
1512simp2d 1009 . . . . 5  |-  ( ph  ->  ( Q `  M
)  =  pi )
1615eqcomd 2475 . . . 4  |-  ( ph  ->  pi  =  ( Q `
 M ) )
1714, 16oveq12d 6313 . . 3  |-  ( ph  ->  ( -u pi [,] pi )  =  (
( Q `  0
) [,] ( Q `
 M ) ) )
18 itgeq1 22047 . . 3  |-  ( (
-u pi [,] pi )  =  ( ( Q `  0 ) [,] ( Q `  M
) )  ->  S. ( -u pi [,] pi ) ( F `  t )  _d t  =  S. ( ( Q `  0 ) [,] ( Q `  M ) ) ( F `  t )  _d t )
1917, 18syl 16 . 2  |-  ( ph  ->  S. ( -u pi [,] pi ) ( F `
 t )  _d t  =  S. ( ( Q `  0
) [,] ( Q `
 M ) ) ( F `  t
)  _d t )
20 0z 10887 . . . 4  |-  0  e.  ZZ
2120a1i 11 . . 3  |-  ( ph  ->  0  e.  ZZ )
22 nnuz 11129 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
232, 22syl6eleq 2565 . . . 4  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
24 1e0p1 11016 . . . . . 6  |-  1  =  ( 0  +  1 )
2524a1i 11 . . . . 5  |-  ( ph  ->  1  =  ( 0  +  1 ) )
2625fveq2d 5876 . . . 4  |-  ( ph  ->  ( ZZ>= `  1 )  =  ( ZZ>= `  (
0  +  1 ) ) )
2723, 26eleqtrd 2557 . . 3  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 0  +  1 ) ) )
283, 2, 1fourierdlem15 31745 . . . . 5  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
29 pire 22718 . . . . . . . . 9  |-  pi  e.  RR
3029renegcli 9892 . . . . . . . 8  |-  -u pi  e.  RR
3130, 29pm3.2i 455 . . . . . . 7  |-  ( -u pi  e.  RR  /\  pi  e.  RR )
32 iccssre 11618 . . . . . . 7  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
3331, 32ax-mp 5 . . . . . 6  |-  ( -u pi [,] pi )  C_  RR
3433a1i 11 . . . . 5  |-  ( ph  ->  ( -u pi [,] pi )  C_  RR )
3528, 34jca 532 . . . 4  |-  ( ph  ->  ( Q : ( 0 ... M ) --> ( -u pi [,] pi )  /\  ( -u pi [,] pi ) 
C_  RR ) )
36 fss 5745 . . . 4  |-  ( ( Q : ( 0 ... M ) --> (
-u pi [,] pi )  /\  ( -u pi [,] pi )  C_  RR )  ->  Q : ( 0 ... M ) --> RR )
3735, 36syl 16 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
3811r19.21bi 2836 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
39 fourierdlem93.6 . . . . . 6  |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )
4039adantr 465 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  F : ( -u pi [,] pi ) --> CC )
41 simpr 461 . . . . . 6  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )
4217eqcomd 2475 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 ) [,] ( Q `  M )
)  =  ( -u pi [,] pi ) )
4342adantr 465 . . . . . 6  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  (
( Q `  0
) [,] ( Q `
 M ) )  =  ( -u pi [,] pi ) )
4441, 43eleqtrd 2557 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  t  e.  ( -u pi [,] pi ) )
4540, 44jca 532 . . . 4  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( F : ( -u pi [,] pi ) --> CC  /\  t  e.  ( -u pi [,] pi ) ) )
46 ffvelrn 6030 . . . 4  |-  ( ( F : ( -u pi [,] pi ) --> CC 
/\  t  e.  (
-u pi [,] pi ) )  ->  ( F `  t )  e.  CC )
4745, 46syl 16 . . 3  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( F `  t )  e.  CC )
48 iooinlbub 31421 . . . . . . 7  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  i^i  { ( Q `
 i ) ,  ( Q `  (
i  +  1 ) ) } )  =  (/)
4948a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  i^i 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  =  (/) )
5049fveq2d 5876 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol* `  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  i^i  {
( Q `  i
) ,  ( Q `
 ( i  +  1 ) ) } ) )  =  ( vol* `  (/) ) )
51 ovol0 21772 . . . . . 6  |-  ( vol* `  (/) )  =  0
5251a1i 11 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol* `  (/) )  =  0 )
5350, 52eqtrd 2508 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol* `  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  i^i  {
( Q `  i
) ,  ( Q `
 ( i  +  1 ) ) } ) )  =  0 )
5437adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
55 elfzofz 11823 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
5655adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
5754, 56jca 532 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q :
( 0 ... M
) --> RR  /\  i  e.  ( 0 ... M
) ) )
58 ffvelrn 6030 . . . . . . . . 9  |-  ( ( Q : ( 0 ... M ) --> RR 
/\  i  e.  ( 0 ... M ) )  ->  ( Q `  i )  e.  RR )
5957, 58syl 16 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
6059rexrd 9655 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
61 fzofzp1 11889 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
6261adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
6354, 62jca 532 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q :
( 0 ... M
) --> RR  /\  (
i  +  1 )  e.  ( 0 ... M ) ) )
64 ffvelrn 6030 . . . . . . . . 9  |-  ( ( Q : ( 0 ... M ) --> RR 
/\  ( i  +  1 )  e.  ( 0 ... M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
6563, 64syl 16 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
6665rexrd 9655 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
6759, 65, 38ltled 9744 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <_  ( Q `  ( i  +  1 ) ) )
6860, 66, 673jca 1176 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  e. 
RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( Q `  i
)  <_  ( Q `  ( i  +  1 ) ) ) )
69 prunioo 11661 . . . . . 6  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( Q `  i )  <_  ( Q `  (
i  +  1 ) ) )  ->  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  =  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) )
7068, 69syl 16 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  =  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
7170eqcomd 2475 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  =  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } ) )
7239ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : ( -u pi [,] pi ) --> CC )
7330rexri 9658 . . . . . . . 8  |-  -u pi  e.  RR*
7473a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  -u pi  e.  RR* )
7529rexri 9658 . . . . . . . 8  |-  pi  e.  RR*
7675a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  pi  e.  RR* )
7728ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
78 simplr 754 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
79 simpr 461 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
8074, 76, 77, 78, 79fourierdlem1 31731 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  ( -u pi [,] pi ) )
8172, 80jca 532 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F : ( -u pi [,] pi ) --> CC  /\  t  e.  ( -u pi [,] pi ) ) )
8281, 46syl 16 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  t )  e.  CC )
8339feqmptd 5927 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( t  e.  ( -u pi [,] pi )  |->  ( F `
 t ) ) )
8483adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F  =  ( t  e.  ( -u pi [,] pi )  |->  ( F `  t ) ) )
8584reseq1d 5278 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( t  e.  (
-u pi [,] pi )  |->  ( F `  t ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
86 ioossicc 11622 . . . . . . . . . . 11  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
8786a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
8880ralrimiva 2881 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. t  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) t  e.  ( -u pi [,] pi ) )
89 dfss3 3499 . . . . . . . . . . 11  |-  ( ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  <->  A. t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) t  e.  (
-u pi [,] pi ) )
9088, 89sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
9187, 90sstrd 3519 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
92 resmpt 5329 . . . . . . . . 9  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  ->  (
( t  e.  (
-u pi [,] pi )  |->  ( F `  t ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) )
9391, 92syl 16 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  ( -u pi [,] pi )  |->  ( F `
 t ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) )
94 eqidd 2468 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  =  ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  t
) ) )
9585, 93, 943eqtrd 2512 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) )
9695eqcomd 2475 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
97 fourierdlem93.7 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
9896, 97eqeltrd 2555 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
99 fourierdlem93.9 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
10095oveq1d 6310 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
10199, 100eleqtrd 2557 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  t
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
102 fourierdlem93.8 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
10395oveq1d 6310 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =  ( ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) lim CC  ( Q `
 i ) ) )
104102, 103eleqtrd 2557 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  t
) ) lim CC  ( Q `  i )
) )
10559, 65, 98, 101, 104iblcncfioo 31619 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  L^1 )
10659, 65jca 532 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  e.  RR  /\  ( Q `
 ( i  +  1 ) )  e.  RR ) )
107 prssg 4188 . . . . . . . 8  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR )  -> 
( ( ( Q `
 i )  e.  RR  /\  ( Q `
 ( i  +  1 ) )  e.  RR )  <->  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  C_  RR ) )
108106, 107syl 16 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR )  <->  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  C_  RR ) )
109106, 108mpbid 210 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { ( Q `
 i ) ,  ( Q `  (
i  +  1 ) ) }  C_  RR )
110 prfi 7807 . . . . . . . . 9  |-  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  e.  Fin
111110a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { ( Q `
 i ) ,  ( Q `  (
i  +  1 ) ) }  e.  Fin )
112111, 109jca 532 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  e.  Fin  /\  { ( Q `
 i ) ,  ( Q `  (
i  +  1 ) ) }  C_  RR ) )
113 ovolfi 21773 . . . . . . 7  |-  ( ( { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  e.  Fin  /\  { ( Q `  i
) ,  ( Q `
 ( i  +  1 ) ) } 
C_  RR )  -> 
( vol* `  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  =  0 )
114112, 113syl 16 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol* `  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  =  0 )
11539ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  ->  F : ( -u pi [,] pi ) --> CC )
116 simpl 457 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  ->  ( ph  /\  i  e.  ( 0..^ M ) ) )
117 lbicc2 11648 . . . . . . . . . . . . . . 15  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( Q `  i )  <_  ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
11868, 117syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
119 ubicc2 11649 . . . . . . . . . . . . . . 15  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( Q `  i )  <_  ( Q `  (
i  +  1 ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) )
12068, 119syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
121118, 120jca 532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  /\  ( Q `
 ( i  +  1 ) )  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) )
122 prssi 4189 . . . . . . . . . . . . 13  |-  ( ( ( Q `  i
)  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  /\  ( Q `  ( i  +  1 ) )  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) )  ->  { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  C_  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )
123121, 122syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { ( Q `
 i ) ,  ( Q `  (
i  +  1 ) ) }  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
124123sseld 3508 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  ->  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) )
125124imp 429 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  ->  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
126116, 125jca 532 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) )
127126, 80syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  ->  t  e.  ( -u pi [,] pi ) )
128115, 127jca 532 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  ->  ( F : ( -u pi [,] pi ) --> CC  /\  t  e.  ( -u pi [,] pi ) ) )
129128, 46syl 16 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) } )  ->  ( F `  t )  e.  CC )
130109, 114, 129itgvol0 31609 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  { ( Q `
 i ) ,  ( Q `  (
i  +  1 ) ) }  |->  ( F `
 t ) )  e.  L^1  /\  S. { ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  ( F `  t )  _d t  =  0 ) )
131130simpld 459 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e. 
{ ( Q `  i ) ,  ( Q `  ( i  +  1 ) ) }  |->  ( F `  t ) )  e.  L^1 )
13253, 71, 82, 105, 131iblsplit 31607 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  L^1 )
13321, 27, 37, 38, 47, 132itgspltprt 31620 . 2  |-  ( ph  ->  S. ( ( Q `
 0 ) [,] ( Q `  M
) ) ( F `
 t )  _d t  =  sum_ i  e.  ( 0..^ M ) S. ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) ( F `
 t )  _d t )
134 fvres 5886 . . . . . . . 8  |-  ( t  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  t )  =  ( F `  t ) )
135134eqcomd 2475 . . . . . . 7  |-  ( t  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  ( F `  t )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  t
) )
136135adantl 466 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  t )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  t
) )
137136itgeq2dv 22056 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S. ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ( F `  t )  _d t  =  S. ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  t
)  _d t )
138 eqid 2467 . . . . . 6  |-  ( x  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  |->  if ( x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) ) )  =  ( x  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  |->  if ( x  =  ( Q `
 i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) ) ) )
13939adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : (
-u pi [,] pi )
--> CC )
140 fssres 5757 . . . . . . 7  |-  ( ( F : ( -u pi [,] pi ) --> CC 
/\  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )  ->  ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
141139, 90, 140syl2anc 661 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
142 resabs1 5308 . . . . . . . 8  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
14387, 142syl 16 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
144143, 97eqeltrd 2555 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
145143oveq1d 6310 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
146145eqcomd 2475 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
14759, 65, 38, 141limcicciooub 31502 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
148146, 147eqtrd 2508 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
14999, 148eleqtrd 2557 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
150143eqcomd 2475 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
151150oveq1d 6310 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =  ( ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )
15259, 65, 38, 141limciccioolb 31486 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )
153 eqidd 2468 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )
154151, 152, 1533eqtrd 2512 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )
155102, 154eleqtrd 2557 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
156 fourierdlem93.5 . . . . . . 7  |-  ( ph  ->  X  e.  RR )
157156adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
158138, 59, 65, 38, 141, 144, 149, 155, 157fourierdlem82 31812 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S. ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  t )  _d t  =  S. ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  ( X  +  t )
)  _d t )
159157adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  X  e.  RR )
16059adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  i )  e.  RR )
161160, 159resubcld 9999 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  i
)  -  X )  e.  RR )
16265adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
163162, 159resubcld 9999 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  X )  e.  RR )
164 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )
165 eliccre 31427 . . . . . . . . . . 11  |-  ( ( ( ( Q `  i )  -  X
)  e.  RR  /\  ( ( Q `  ( i  +  1 ) )  -  X
)  e.  RR  /\  t  e.  ( (
( Q `  i
)  -  X ) [,] ( ( Q `
 ( i  +  1 ) )  -  X ) ) )  ->  t  e.  RR )
166161, 163, 164, 165syl3anc 1228 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  e.  RR )
167159, 166readdcld 9635 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( X  +  t )  e.  RR )
168 elicc2 11601 . . . . . . . . . . . . 13  |-  ( ( ( ( Q `  i )  -  X
)  e.  RR  /\  ( ( Q `  ( i  +  1 ) )  -  X
)  e.  RR )  ->  ( t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) )  <->  ( t  e.  RR  /\  ( ( Q `  i )  -  X )  <_ 
t  /\  t  <_  ( ( Q `  (
i  +  1 ) )  -  X ) ) ) )
169161, 163, 168syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
t  e.  ( ( ( Q `  i
)  -  X ) [,] ( ( Q `
 ( i  +  1 ) )  -  X ) )  <->  ( t  e.  RR  /\  ( ( Q `  i )  -  X )  <_ 
t  /\  t  <_  ( ( Q `  (
i  +  1 ) )  -  X ) ) ) )
170164, 169mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
t  e.  RR  /\  ( ( Q `  i )  -  X
)  <_  t  /\  t  <_  ( ( Q `
 ( i  +  1 ) )  -  X ) ) )
171170simp2d 1009 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  i
)  -  X )  <_  t )
172 lesubadd2 10037 . . . . . . . . . . 11  |-  ( ( ( Q `  i
)  e.  RR  /\  X  e.  RR  /\  t  e.  RR )  ->  (
( ( Q `  i )  -  X
)  <_  t  <->  ( Q `  i )  <_  ( X  +  t )
) )
173160, 159, 166, 172syl3anc 1228 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( ( Q `  i )  -  X
)  <_  t  <->  ( Q `  i )  <_  ( X  +  t )
) )
174171, 173mpbid 210 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  i )  <_  ( X  +  t ) )
175170simp3d 1010 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  <_  ( ( Q `  ( i  +  1 ) )  -  X
) )
176 leaddsub2 10041 . . . . . . . . . . 11  |-  ( ( X  e.  RR  /\  t  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR )  -> 
( ( X  +  t )  <_  ( Q `  ( i  +  1 ) )  <-> 
t  <_  ( ( Q `  ( i  +  1 ) )  -  X ) ) )
177159, 166, 162, 176syl3anc 1228 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( X  +  t )  <_  ( Q `  ( i  +  1 ) )  <->  t  <_  ( ( Q `  (
i  +  1 ) )  -  X ) ) )
178175, 177mpbird 232 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( X  +  t )  <_  ( Q `  (
i  +  1 ) ) )
179167, 174, 1783jca 1176 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( X  +  t )  e.  RR  /\  ( Q `  i )  <_  ( X  +  t )  /\  ( X  +  t )  <_  ( Q `  (
i  +  1 ) ) ) )
180 elicc2 11601 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) )
181160, 162, 180syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( X  +  t )  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  <->  ( ( X  +  t )  e.  RR  /\  ( Q `
 i )  <_ 
( X  +  t )  /\  ( X  +  t )  <_ 
( Q `  (
i  +  1 ) ) ) ) )
182179, 181mpbird 232 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( X  +  t )  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
183 fvres 5886 . . . . . . 7  |-  ( ( X  +  t )  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  =  ( F `  ( X  +  t
) ) )
184182, 183syl 16 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  =  ( F `  ( X  +  t
) ) )
185184itgeq2dv 22056 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S. ( ( ( Q `  i
)  -  X ) [,] ( ( Q `
 ( i  +  1 ) )  -  X ) ) ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  _d t  =  S. ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) ( F `  ( X  +  t
) )  _d t )
186137, 158, 1853eqtrd 2512 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  S. ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ( F `  t )  _d t  =  S. ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) ( F `  ( X  +  t
) )  _d t )
187186sumeq2dv 13505 . . 3  |-  ( ph  -> 
sum_ i  e.  ( 0..^ M ) S. ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ( F `  t )  _d t  =  sum_ i  e.  ( 0..^ M ) S. ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) ( F `  ( X  +  t
) )  _d t )
188 oveq2 6303 . . . . . . 7  |-  ( s  =  t  ->  ( X  +  s )  =  ( X  +  t ) )
189188fveq2d 5876 . . . . . 6  |-  ( s  =  t  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  t
) ) )
190 nfcv 2629 . . . . . 6  |-  F/_ t
( F `  ( X  +  s )
)
191 nfcv 2629 . . . . . 6  |-  F/_ s
( F `  ( X  +  t )
)
192189, 190, 191cbvitg 22050 . . . . 5  |-  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( F `  ( X  +  s
) )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( F `  ( X  +  t )
)  _d t
193192a1i 11 . . . 4  |-  ( ph  ->  S. ( ( -u pi  -  X ) [,] ( pi  -  X
) ) ( F `
 ( X  +  s ) )  _d s  =  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( F `  ( X  +  t
) )  _d t )
194 fourierdlem93.2 . . . . . . . . 9  |-  H  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  -  X
) )
195194a1i 11 . . . . . . . 8  |-  ( ph  ->  H  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) ) )
196 fveq2 5872 . . . . . . . . . 10  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
197196oveq1d 6310 . . . . . . . . 9  |-  ( i  =  0  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
198197adantl 466 . . . . . . . 8  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
1992nnzd 10977 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ZZ )
20021, 199, 213jca 1176 . . . . . . . . . 10  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )
)
201 0re 9608 . . . . . . . . . . . . 13  |-  0  e.  RR
202201leidi 10099 . . . . . . . . . . . 12  |-  0  <_  0
203202a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  0 )
204201a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  0  e.  RR )
2052nnred 10563 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  RR )
2062nngt0d 10591 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  M )
207204, 205, 206ltled 9744 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  M )
208203, 207jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( 0  <_  0  /\  0  <_  M ) )
209200, 208jca 532 . . . . . . . . 9  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
210 elfz2 11691 . . . . . . . . 9  |-  ( 0  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
211209, 210sylibr 212 . . . . . . . 8  |-  ( ph  ->  0  e.  ( 0 ... M ) )
2129, 30syl6eqel 2563 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  e.  RR )
213212, 156resubcld 9999 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
0 )  -  X
)  e.  RR )
214195, 198, 211, 213fvmptd 5962 . . . . . . 7  |-  ( ph  ->  ( H `  0
)  =  ( ( Q `  0 )  -  X ) )
2159oveq1d 6310 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  -  X
)  =  ( -u pi  -  X ) )
216214, 215eqtr2d 2509 . . . . . 6  |-  ( ph  ->  ( -u pi  -  X )  =  ( H `  0 ) )
217 fveq2 5872 . . . . . . . . . 10  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
218217oveq1d 6310 . . . . . . . . 9  |-  ( i  =  M  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 M )  -  X ) )
219218adantl 466 . . . . . . . 8  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 M )  -  X ) )
22021, 199, 1993jca 1176 . . . . . . . . . 10  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  M  e.  ZZ )
)
221205leidd 10131 . . . . . . . . . . 11  |-  ( ph  ->  M  <_  M )
222207, 221jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( 0  <_  M  /\  M  <_  M ) )
223220, 222jca 532 . . . . . . . . 9  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  M  e.  ZZ )  /\  (
0  <_  M  /\  M  <_  M ) ) )
224 elfz2 11691 . . . . . . . . 9  |-  ( M  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  M  e.  ZZ )  /\  (
0  <_  M  /\  M  <_  M ) ) )
225223, 224sylibr 212 . . . . . . . 8  |-  ( ph  ->  M  e.  ( 0 ... M ) )
22610, 29syl6eqel 2563 . . . . . . . . 9  |-  ( ph  ->  ( Q `  M
)  e.  RR )
227226, 156resubcld 9999 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  M )  -  X
)  e.  RR )
228195, 219, 225, 227fvmptd 5962 . . . . . . 7  |-  ( ph  ->  ( H `  M
)  =  ( ( Q `  M )  -  X ) )
22910oveq1d 6310 . . . . . . 7  |-  ( ph  ->  ( ( Q `  M )  -  X
)  =  ( pi 
-  X ) )
230228, 229eqtr2d 2509 . . . . . 6  |-  ( ph  ->  ( pi  -  X
)  =  ( H `
 M ) )
231216, 230oveq12d 6313 . . . . 5  |-  ( ph  ->  ( ( -u pi  -  X ) [,] (
pi  -  X )
)  =  ( ( H `  0 ) [,] ( H `  M ) ) )
232 itgeq1 22047 . . . . 5  |-  ( ( ( -u pi  -  X ) [,] (
pi  -  X )
)  =  ( ( H `  0 ) [,] ( H `  M ) )  ->  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( F `  ( X  +  t
) )  _d t  =  S. ( ( H `  0 ) [,] ( H `  M ) ) ( F `  ( X  +  t ) )  _d t )
233231, 232syl 16 . . . 4  |-  ( ph  ->  S. ( ( -u pi  -  X ) [,] ( pi  -  X
) ) ( F `
 ( X  +  t ) )  _d t  =  S. ( ( H `  0
) [,] ( H `
 M ) ) ( F `  ( X  +  t )
)  _d t )
23437, 58sylan 471 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
235156adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
236234, 235resubcld 9999 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  -  X )  e.  RR )
237236ralrimiva 2881 . . . . . . 7  |-  ( ph  ->  A. i  e.  ( 0 ... M ) ( ( Q `  i )  -  X
)  e.  RR )
238194fmpt 6053 . . . . . . 7  |-  ( A. i  e.  ( 0 ... M ) ( ( Q `  i
)  -  X )  e.  RR  <->  H :
( 0 ... M
) --> RR )
239237, 238sylib 196 . . . . . 6  |-  ( ph  ->  H : ( 0 ... M ) --> RR )
24059, 65, 157ltsub1d 10173 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  < 
( Q `  (
i  +  1 ) )  <->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) ) )
24138, 240mpbid 210 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) )
24256, 236syldan 470 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  e.  RR )
243194fvmpt2 5964 . . . . . . . 8  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  -  X
)  e.  RR )  ->  ( H `  i )  =  ( ( Q `  i
)  -  X ) )
24456, 242, 243syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  =  ( ( Q `  i
)  -  X ) )
245 nfcv 2629 . . . . . . . . . . 11  |-  F/_ j
( ( Q `  i )  -  X
)
246 nfcv 2629 . . . . . . . . . . 11  |-  F/_ i
( ( Q `  j )  -  X
)
247 fveq2 5872 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
248247oveq1d 6310 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 j )  -  X ) )
249245, 246, 248cbvmpt 4543 . . . . . . . . . 10  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  -  X ) )
250194, 249eqtri 2496 . . . . . . . . 9  |-  H  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  -  X
) )
251250a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  H  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  -  X ) ) )
252 fveq2 5872 . . . . . . . . . 10  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
253252oveq1d 6310 . . . . . . . . 9  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
254253adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
25565, 157resubcld 9999 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  X )  e.  RR )
256251, 254, 62, 255fvmptd 5962 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  -  X ) )
257241, 244, 2563brtr4d 4483 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  <  ( H `  ( i  +  1 ) ) )
258 ffun 5739 . . . . . . . . . 10  |-  ( F : ( -u pi [,] pi ) --> CC  ->  Fun 
F )
25939, 258syl 16 . . . . . . . . 9  |-  ( ph  ->  Fun  F )
260259adantr 465 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  Fun  F )
261156adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  X  e.  RR )
262214, 213eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( H `  0
)  e.  RR )
263262adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  0 )  e.  RR )
264228, 227eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( H `  M
)  e.  RR )
265264adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  M )  e.  RR )
266 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )
267 eliccre 31427 . . . . . . . . . . . . 13  |-  ( ( ( H `  0
)  e.  RR  /\  ( H `  M )  e.  RR  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  RR )
268263, 265, 266, 267syl3anc 1228 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  RR )
269261, 268readdcld 9635 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  RR )
270 elicc2 11601 . . . . . . . . . . . . . . . 16  |-  ( ( ( H `  0
)  e.  RR  /\  ( H `  M )  e.  RR )  -> 
( t  e.  ( ( H `  0
) [,] ( H `
 M ) )  <-> 
( t  e.  RR  /\  ( H `  0
)  <_  t  /\  t  <_  ( H `  M ) ) ) )
271263, 265, 270syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
t  e.  ( ( H `  0 ) [,] ( H `  M ) )  <->  ( t  e.  RR  /\  ( H `
 0 )  <_ 
t  /\  t  <_  ( H `  M ) ) ) )
272266, 271mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
t  e.  RR  /\  ( H `  0 )  <_  t  /\  t  <_  ( H `  M
) ) )
273272simp2d 1009 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  0 )  <_  t )
274263, 268, 2613jca 1176 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
( H `  0
)  e.  RR  /\  t  e.  RR  /\  X  e.  RR ) )
275 leadd2 10033 . . . . . . . . . . . . . 14  |-  ( ( ( H `  0
)  e.  RR  /\  t  e.  RR  /\  X  e.  RR )  ->  (
( H `  0
)  <_  t  <->  ( X  +  ( H ` 
0 ) )  <_ 
( X  +  t ) ) )
276274, 275syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
( H `  0
)  <_  t  <->  ( X  +  ( H ` 
0 ) )  <_ 
( X  +  t ) ) )
277273, 276mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  ( H `  0 ) )  <_  ( X  +  t ) )
278196adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  = 
0 )  ->  ( Q `  i )  =  ( Q ` 
0 ) )
279278oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
280195, 279, 211, 213fvmptd 5962 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( H `  0
)  =  ( ( Q `  0 )  -  X ) )
281280oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  +  ( H `  0 ) )  =  ( X  +  ( ( Q `
 0 )  -  X ) ) )
282 ax-resscn 9561 . . . . . . . . . . . . . . . . 17  |-  RR  C_  CC
283282, 156sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  CC )
284282, 212sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  0
)  e.  CC )
285 pncan3 9840 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  CC  /\  ( Q `  0 )  e.  CC )  -> 
( X  +  ( ( Q `  0
)  -  X ) )  =  ( Q `
 0 ) )
286283, 284, 285syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  +  ( ( Q `  0
)  -  X ) )  =  ( Q `
 0 ) )
287281, 286, 93eqtrrd 2513 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u pi  =  ( X  +  ( H `
 0 ) ) )
288287adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  =  ( X  +  ( H `  0 ) ) )
289288breq1d 4463 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( -u pi  <_  ( X  +  t )  <->  ( X  +  ( H ` 
0 ) )  <_ 
( X  +  t ) ) )
290277, 289mpbird 232 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  <_  ( X  +  t ) )
291272simp3d 1010 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  <_  ( H `  M
) )
292 leadd2 10033 . . . . . . . . . . . . . 14  |-  ( ( t  e.  RR  /\  ( H `  M )  e.  RR  /\  X  e.  RR )  ->  (
t  <_  ( H `  M )  <->  ( X  +  t )  <_ 
( X  +  ( H `  M ) ) ) )
293268, 265, 261, 292syl3anc 1228 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
t  <_  ( H `  M )  <->  ( X  +  t )  <_ 
( X  +  ( H `  M ) ) ) )
294291, 293mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  <_  ( X  +  ( H `  M ) ) )
295228oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  +  ( H `  M ) )  =  ( X  +  ( ( Q `
 M )  -  X ) ) )
296282, 226sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  M
)  e.  CC )
297 pncan3 9840 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  CC  /\  ( Q `  M )  e.  CC )  -> 
( X  +  ( ( Q `  M
)  -  X ) )  =  ( Q `
 M ) )
298283, 296, 297syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  +  ( ( Q `  M
)  -  X ) )  =  ( Q `
 M ) )
299295, 298, 103eqtrrd 2513 . . . . . . . . . . . . . 14  |-  ( ph  ->  pi  =  ( X  +  ( H `  M ) ) )
300299adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  pi  =  ( X  +  ( H `  M ) ) )
301300breq2d 4465 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
( X  +  t )  <_  pi  <->  ( X  +  t )  <_ 
( X  +  ( H `  M ) ) ) )
302294, 301mpbird 232 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  <_  pi )
303269, 290, 3023jca 1176 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
( X  +  t )  e.  RR  /\  -u pi  <_  ( X  +  t )  /\  ( X  +  t
)  <_  pi )
)
30430a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  e.  RR )
30529a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  pi  e.  RR )
306 elicc2 11601 . . . . . . . . . . 11  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( ( X  +  t )  e.  ( -u pi [,] pi )  <->  ( ( X  +  t )  e.  RR  /\  -u pi  <_  ( X  +  t )  /\  ( X  +  t )  <_  pi ) ) )
307304, 305, 306syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
( X  +  t )  e.  ( -u pi [,] pi )  <->  ( ( X  +  t )  e.  RR  /\  -u pi  <_  ( X  +  t )  /\  ( X  +  t )  <_  pi ) ) )
308303, 307mpbird 232 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  ( -u pi [,] pi ) )
309 fdm 5741 . . . . . . . . . . . 12  |-  ( F : ( -u pi [,] pi ) --> CC  ->  dom 
F  =  ( -u pi [,] pi ) )
31039, 309syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  (
-u pi [,] pi ) )
311310eqcomd 2475 . . . . . . . . . 10  |-  ( ph  ->  ( -u pi [,] pi )  =  dom  F )
312311adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( -u pi [,] pi )  =  dom  F )
313308, 312eleqtrd 2557 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  dom  F )
314 fvelrn 6025 . . . . . . . 8  |-  ( ( Fun  F  /\  ( X  +  t )  e.  dom  F )  -> 
( F `  ( X  +  t )
)  e.  ran  F
)
315260, 313, 314syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( F `  ( X  +  t ) )  e.  ran  F )
316 frn 5743 . . . . . . . . . 10  |-  ( F : ( -u pi [,] pi ) --> CC  ->  ran 
F  C_  CC )
31739, 316syl 16 . . . . . . . . 9  |-  ( ph  ->  ran  F  C_  CC )
318317adantr 465 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ran  F 
C_  CC )
319318sseld 3508 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
( F `  ( X  +  t )
)  e.  ran  F  ->  ( F `  ( X  +  t )
)  e.  CC ) )
320315, 319mpd 15 . . . . . 6  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( F `  ( X  +  t ) )  e.  CC )
321244, 242eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  e.  RR )
322256, 255eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  e.  RR )
323 fssres 5757 . . . . . . . . . . . 12  |-  ( ( F : ( -u pi [,] pi ) --> CC 
/\  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
324139, 91, 323syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
32560adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
32666adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
327157adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
328 elioore 11571 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  ->  t  e.  RR )
329328adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
330327, 329readdcld 9635 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  e.  RR )
331330rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  e.  RR* )
332325, 326, 3313jca 1176 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( X  +  t )  e.  RR* ) )
333 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )
334321adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  e.  RR )
335334rexrd 9655 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  e.  RR* )
336322rexrd 9655 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  e.  RR* )
337336adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  ( i  +  1 ) )  e.  RR* )
338 elioo2 11582 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( H `  i
)  e.  RR*  /\  ( H `  ( i  +  1 ) )  e.  RR* )  ->  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  <->  ( t  e.  RR  /\  ( H `
 i )  < 
t  /\  t  <  ( H `  ( i  +  1 ) ) ) ) )
339335, 337, 338syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  <->  ( t  e.  RR  /\  ( H `
 i )  < 
t  /\  t  <  ( H `  ( i  +  1 ) ) ) ) )
340333, 339mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
t  e.  RR  /\  ( H `  i )  <  t  /\  t  <  ( H `  (
i  +  1 ) ) ) )
341340simp2d 1009 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  <  t )
342334, 329, 327ltadd2d 9749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( H `  i
)  <  t  <->  ( X  +  ( H `  i ) )  < 
( X  +  t ) ) )
343341, 342mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  ( H `  i ) )  < 
( X  +  t ) )
344244oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  i ) )  =  ( X  +  ( ( Q `
 i )  -  X ) ) )
345283adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
346282, 59sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
347 pncan3 9840 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( X  e.  CC  /\  ( Q `  i )  e.  CC )  -> 
( X  +  ( ( Q `  i
)  -  X ) )  =  ( Q `
 i ) )
348345, 346, 347syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( Q `  i )  -  X
) )  =  ( Q `  i ) )
349 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( Q `  i ) )
350344, 348, 3493eqtrrd 2513 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( X  +  ( H `
 i ) ) )
351350adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  =  ( X  +  ( H `  i ) ) )
352351breq1d 4463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
)  <  ( X  +  t )  <->  ( X  +  ( H `  i ) )  < 
( X  +  t ) ) )
353343, 352mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( X  +  t ) )
354340simp3d 1010 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  <  ( H `  (
i  +  1 ) ) )
355322adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  ( i  +  1 ) )  e.  RR )
356329, 355, 327ltadd2d 9749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
t  <  ( H `  ( i  +  1 ) )  <->  ( X  +  t )  < 
( X  +  ( H `  ( i  +  1 ) ) ) ) )
357354, 356mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  <  ( X  +  ( H `  ( i  +  1 ) ) ) )
358256oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( X  +  ( ( Q `
 ( i  +  1 ) )  -  X ) ) )
359282, 65sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
360 pncan3 9840 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( X  e.  CC  /\  ( Q `  ( i  +  1 ) )  e.  CC )  -> 
( X  +  ( ( Q `  (
i  +  1 ) )  -  X ) )  =  ( Q `
 ( i  +  1 ) ) )
361345, 359, 360syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( Q `  ( i  +  1 ) )  -  X
) )  =  ( Q `  ( i  +  1 ) ) )
362 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
363358, 361, 3623eqtrd 2512 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( Q `
 ( i  +  1 ) ) )
364363adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( Q `  (
i  +  1 ) ) )
365364breq2d 4465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( X  +  t )  <  ( X  +  ( H `  ( i  +  1 ) ) )  <->  ( X  +  t )  < 
( Q `  (
i  +  1 ) ) ) )
366357, 365mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  <  ( Q `  (
i  +  1 ) ) )
367353, 366jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
)  <  ( X  +  t )  /\  ( X  +  t
)  <  ( Q `  ( i  +  1 ) ) ) )
368332, 367jca 532 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( ( Q `  i )  e.  RR*  /\  ( Q `  (
i  +  1 ) )  e.  RR*  /\  ( X  +  t )  e.  RR* )  /\  (
( Q `  i
)  <  ( X  +  t )  /\  ( X  +  t
)  <  ( Q `  ( i  +  1 ) ) ) ) )
369 elioo3g 11570 . . . . . . . . . . . . . 14  |-  ( ( X  +  t )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  <->  ( (
( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( X  +  t )  e.  RR* )  /\  (
( Q `  i
)  <  ( X  +  t )  /\  ( X  +  t
)  <  ( Q `  ( i  +  1 ) ) ) ) )
370368, 369sylibr 212 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
371370ralrimiva 2881 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) ( X  +  t )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
372 eqid 2467 . . . . . . . . . . . . 13  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) )  =  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) )
373372fmpt 6053 . . . . . . . . . . . 12  |-  ( A. t  e.  ( ( H `  i ) (,) ( H `  (
i  +  1 ) ) ) ( X  +  t )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) : ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) --> ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
374371, 373sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) : ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) --> ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
375 fcompt 6068 . . . . . . . . . . 11  |-  ( ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC 
/\  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 )