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

Theorem fourierdlem93 37850
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 . . . . . . . 8  |-  ( ph  ->  Q  e.  ( P `
 M ) )
2 fourierdlem93.3 . . . . . . . . 9  |-  ( ph  ->  M  e.  NN )
3 fourierdlem93.1 . . . . . . . . . 10  |-  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 37758 . . . . . . . . 9  |-  ( 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 17 . . . . . . . 8  |-  ( 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 213 . . . . . . 7  |-  ( 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 464 . . . . . 6  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
87simplld 759 . . . . 5  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
98eqcomd 2428 . . . 4  |-  ( ph  -> 
-u pi  =  ( Q `  0 ) )
107simplrd 761 . . . . 5  |-  ( ph  ->  ( Q `  M
)  =  pi )
1110eqcomd 2428 . . . 4  |-  ( ph  ->  pi  =  ( Q `
 M ) )
129, 11oveq12d 6315 . . 3  |-  ( ph  ->  ( -u pi [,] pi )  =  (
( Q `  0
) [,] ( Q `
 M ) ) )
1312itgeq1d 37620 . 2  |-  ( ph  ->  S. ( -u pi [,] pi ) ( F `
 t )  _d t  =  S. ( ( Q `  0
) [,] ( Q `
 M ) ) ( F `  t
)  _d t )
14 0zd 10945 . . 3  |-  ( ph  ->  0  e.  ZZ )
15 nnuz 11190 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
162, 15syl6eleq 2518 . . . 4  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
17 1e0p1 11075 . . . . . 6  |-  1  =  ( 0  +  1 )
1817a1i 11 . . . . 5  |-  ( ph  ->  1  =  ( 0  +  1 ) )
1918fveq2d 5877 . . . 4  |-  ( ph  ->  ( ZZ>= `  1 )  =  ( ZZ>= `  (
0  +  1 ) ) )
2016, 19eleqtrd 2510 . . 3  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 0  +  1 ) ) )
213, 2, 1fourierdlem15 37771 . . . 4  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
22 pire 23390 . . . . . . 7  |-  pi  e.  RR
2322renegcli 9931 . . . . . 6  |-  -u pi  e.  RR
24 iccssre 11712 . . . . . 6  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
2523, 22, 24mp2an 676 . . . . 5  |-  ( -u pi [,] pi )  C_  RR
2625a1i 11 . . . 4  |-  ( ph  ->  ( -u pi [,] pi )  C_  RR )
2721, 26fssd 5747 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
287simprd 464 . . . 4  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
2928r19.21bi 2792 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
30 fourierdlem93.6 . . . . 5  |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )
3130adantr 466 . . . 4  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  F : ( -u pi [,] pi ) --> CC )
32 simpr 462 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )
3312eqcomd 2428 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 ) [,] ( Q `  M )
)  =  ( -u pi [,] pi ) )
3433adantr 466 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  (
( Q `  0
) [,] ( Q `
 M ) )  =  ( -u pi [,] pi ) )
3532, 34eleqtrd 2510 . . . 4  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  t  e.  ( -u pi [,] pi ) )
3631, 35ffvelrnd 6030 . . 3  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( F `  t )  e.  CC )
3727adantr 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
38 elfzofz 11929 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
3938adantl 467 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
4037, 39ffvelrnd 6030 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
41 fzofzp1 12001 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
4241adantl 467 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
4337, 42ffvelrnd 6030 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
4430feqmptd 5926 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( t  e.  ( -u pi [,] pi )  |->  ( F `
 t ) ) )
4544adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F  =  ( t  e.  ( -u pi [,] pi )  |->  ( F `  t ) ) )
4645reseq1d 5116 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( t  e.  (
-u pi [,] pi )  |->  ( F `  t ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
47 ioossicc 11716 . . . . . . . . . . 11  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
4847a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
4923rexri 9689 . . . . . . . . . . . . . 14  |-  -u pi  e.  RR*
5049a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  -u pi  e.  RR* )
5122rexri 9689 . . . . . . . . . . . . . 14  |-  pi  e.  RR*
5251a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  pi  e.  RR* )
5321ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
54 simplr 760 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
55 simpr 462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
5650, 52, 53, 54, 55fourierdlem1 37757 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  ( -u pi [,] pi ) )
5756ralrimiva 2837 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. t  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) t  e.  ( -u pi [,] pi ) )
58 dfss3 3451 . . . . . . . . . . 11  |-  ( ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  <->  A. t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) t  e.  (
-u pi [,] pi ) )
5957, 58sylibr 215 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
6048, 59sstrd 3471 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
6160resmptd 5168 . . . . . . . 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 ) ) )
6246, 61eqtrd 2461 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) )
6362eqcomd 2428 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
64 fourierdlem93.7 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
6563, 64eqeltrd 2508 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
66 fourierdlem93.9 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
6762oveq1d 6312 . . . . . 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 ) ) ) )
6866, 67eleqtrd 2510 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  t
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
69 fourierdlem93.8 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
7062oveq1d 6312 . . . . . 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 ) ) )
7169, 70eleqtrd 2510 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  t
) ) lim CC  ( Q `  i )
) )
7240, 43, 65, 68, 71iblcncfioo 37642 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  L^1 )
7330ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : ( -u pi [,] pi ) --> CC )
7473, 56ffvelrnd 6030 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  t )  e.  CC )
7540, 43, 72, 74ibliooicc 37635 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  L^1 )
7614, 20, 27, 29, 36, 75itgspltprt 37643 . 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 )
77 fvres 5887 . . . . . . . 8  |-  ( t  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  t )  =  ( F `  t ) )
7877eqcomd 2428 . . . . . . 7  |-  ( t  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  ( F `  t )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  t
) )
7978adantl 467 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  t )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  t
) )
8079itgeq2dv 22716 . . . . 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 )
81 eqid 2420 . . . . . 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 ) ) ) )
8230adantr 466 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : (
-u pi [,] pi )
--> CC )
8382, 59fssresd 5759 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
8448resabs1d 5146 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
8584, 64eqeltrd 2508 . . . . . 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 ) )
8684oveq1d 6312 . . . . . . . 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 ) ) ) )
8740, 43, 29, 83limcicciooub 37504 . . . . . . . 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 ) ) ) )
8886, 87eqtr3d 2463 . . . . . . 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 ) ) ) )
8966, 88eleqtrd 2510 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
9084eqcomd 2428 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
9190oveq1d 6312 . . . . . . . 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 ) ) )
9240, 43, 29, 83limciccioolb 37488 . . . . . . . 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 ) ) )
9391, 92eqtrd 2461 . . . . . . 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 ) ) )
9469, 93eleqtrd 2510 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
95 fourierdlem93.5 . . . . . . 7  |-  ( ph  ->  X  e.  RR )
9695adantr 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
9781, 40, 43, 29, 83, 85, 89, 94, 96fourierdlem82 37839 . . . . 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 )
9840adantr 466 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  i )  e.  RR )
9943adantr 466 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
10095ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  X  e.  RR )
10198, 100resubcld 10043 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  i
)  -  X )  e.  RR )
10299, 100resubcld 10043 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  X )  e.  RR )
103 simpr 462 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )
104 eliccre 37403 . . . . . . . . . 10  |-  ( ( ( ( Q `  i )  -  X
)  e.  RR  /\  ( ( Q `  ( i  +  1 ) )  -  X
)  e.  RR  /\  t  e.  ( (
( Q `  i
)  -  X ) [,] ( ( Q `
 ( i  +  1 ) )  -  X ) ) )  ->  t  e.  RR )
105101, 102, 103, 104syl3anc 1264 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  e.  RR )
106100, 105readdcld 9666 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( X  +  t )  e.  RR )
107 elicc2 11695 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) ) )
108101, 102, 107syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
109103, 108mpbid 213 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
110109simp2d 1018 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  i
)  -  X )  <_  t )
11198, 100, 105lesubadd2d 10208 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( ( Q `  i )  -  X
)  <_  t  <->  ( Q `  i )  <_  ( X  +  t )
) )
112110, 111mpbid 213 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  i )  <_  ( X  +  t ) )
113109simp3d 1019 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  <_  ( ( Q `  ( i  +  1 ) )  -  X
) )
114100, 105, 99leaddsub2d 10211 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( X  +  t )  <_  ( Q `  ( i  +  1 ) )  <->  t  <_  ( ( Q `  (
i  +  1 ) )  -  X ) ) )
115113, 114mpbird 235 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( X  +  t )  <_  ( Q `  (
i  +  1 ) ) )
11698, 99, 106, 112, 115eliccd 37401 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( X  +  t )  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
117 fvres 5887 . . . . . . 7  |-  ( ( X  +  t )  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  =  ( F `  ( X  +  t
) ) )
118116, 117syl 17 . . . . . 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
) ) )
119118itgeq2dv 22716 . . . . 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 )
12080, 97, 1193eqtrd 2465 . . . 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 )
121120sumeq2dv 13747 . . 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 )
122 oveq2 6305 . . . . . . 7  |-  ( s  =  t  ->  ( X  +  s )  =  ( X  +  t ) )
123122fveq2d 5877 . . . . . 6  |-  ( s  =  t  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  t
) ) )
124123cbvitgv 22711 . . . . 5  |-  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( F `  ( X  +  s
) )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( F `  ( X  +  t )
)  _d t
125124a1i 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 )
126 fourierdlem93.2 . . . . . . . . 9  |-  H  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  -  X
) )
127126a1i 11 . . . . . . . 8  |-  ( ph  ->  H  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) ) )
128 fveq2 5873 . . . . . . . . . 10  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
129128oveq1d 6312 . . . . . . . . 9  |-  ( i  =  0  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
130129adantl 467 . . . . . . . 8  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
1312nnzd 11035 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
13214, 131, 143jca 1185 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )
)
133 0le0 10695 . . . . . . . . . . 11  |-  0  <_  0
134133a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  <_  0 )
135 0red 9640 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  RR )
1362nnred 10620 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
1372nngt0d 10649 . . . . . . . . . . 11  |-  ( ph  ->  0  <  M )
138135, 136, 137ltled 9779 . . . . . . . . . 10  |-  ( ph  ->  0  <_  M )
139134, 138jca 534 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  0  /\  0  <_  M ) )
140 elfz2 11785 . . . . . . . . 9  |-  ( 0  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
141132, 139, 140sylanbrc 668 . . . . . . . 8  |-  ( ph  ->  0  e.  ( 0 ... M ) )
1428, 23syl6eqel 2516 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  e.  RR )
143142, 95resubcld 10043 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
0 )  -  X
)  e.  RR )
144127, 130, 141, 143fvmptd 5962 . . . . . . 7  |-  ( ph  ->  ( H `  0
)  =  ( ( Q `  0 )  -  X ) )
1458oveq1d 6312 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  -  X
)  =  ( -u pi  -  X ) )
146144, 145eqtr2d 2462 . . . . . 6  |-  ( ph  ->  ( -u pi  -  X )  =  ( H `  0 ) )
147 fveq2 5873 . . . . . . . . . 10  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
148147oveq1d 6312 . . . . . . . . 9  |-  ( i  =  M  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 M )  -  X ) )
149148adantl 467 . . . . . . . 8  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 M )  -  X ) )
15014, 131, 1313jca 1185 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  M  e.  ZZ )
)
151136leidd 10176 . . . . . . . . . 10  |-  ( ph  ->  M  <_  M )
152138, 151jca 534 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  M  /\  M  <_  M ) )
153 elfz2 11785 . . . . . . . . 9  |-  ( M  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  M  e.  ZZ )  /\  (
0  <_  M  /\  M  <_  M ) ) )
154150, 152, 153sylanbrc 668 . . . . . . . 8  |-  ( ph  ->  M  e.  ( 0 ... M ) )
15510, 22syl6eqel 2516 . . . . . . . . 9  |-  ( ph  ->  ( Q `  M
)  e.  RR )
156155, 95resubcld 10043 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  M )  -  X
)  e.  RR )
157127, 149, 154, 156fvmptd 5962 . . . . . . 7  |-  ( ph  ->  ( H `  M
)  =  ( ( Q `  M )  -  X ) )
15810oveq1d 6312 . . . . . . 7  |-  ( ph  ->  ( ( Q `  M )  -  X
)  =  ( pi 
-  X ) )
159157, 158eqtr2d 2462 . . . . . 6  |-  ( ph  ->  ( pi  -  X
)  =  ( H `
 M ) )
160146, 159oveq12d 6315 . . . . 5  |-  ( ph  ->  ( ( -u pi  -  X ) [,] (
pi  -  X )
)  =  ( ( H `  0 ) [,] ( H `  M ) ) )
161160itgeq1d 37620 . . . 4  |-  ( ph  ->  S. ( ( -u pi  -  X ) [,] ( pi  -  X
) ) ( F `
 ( X  +  t ) )  _d t  =  S. ( ( H `  0
) [,] ( H `
 M ) ) ( F `  ( X  +  t )
)  _d t )
16227fnvinran 37190 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
16395adantr 466 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
164162, 163resubcld 10043 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  -  X )  e.  RR )
165164, 126fmptd 6053 . . . . . 6  |-  ( ph  ->  H : ( 0 ... M ) --> RR )
16640, 43, 96, 29ltsub1dd 10221 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) )
16739, 164syldan 472 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  e.  RR )
168126fvmpt2 5965 . . . . . . . 8  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  -  X
)  e.  RR )  ->  ( H `  i )  =  ( ( Q `  i
)  -  X ) )
16939, 167, 168syl2anc 665 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  =  ( ( Q `  i
)  -  X ) )
170 fveq2 5873 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
171170oveq1d 6312 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 j )  -  X ) )
172171cbvmptv 4510 . . . . . . . . . 10  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  -  X ) )
173126, 172eqtri 2449 . . . . . . . . 9  |-  H  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  -  X
) )
174173a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  H  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  -  X ) ) )
175 fveq2 5873 . . . . . . . . . 10  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
176175oveq1d 6312 . . . . . . . . 9  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
177176adantl 467 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
17843, 96resubcld 10043 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  X )  e.  RR )
179174, 177, 42, 178fvmptd 5962 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  -  X ) )
180166, 169, 1793brtr4d 4448 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  <  ( H `  ( i  +  1 ) ) )
181 frn 5744 . . . . . . . . 9  |-  ( F : ( -u pi [,] pi ) --> CC  ->  ran 
F  C_  CC )
18230, 181syl 17 . . . . . . . 8  |-  ( ph  ->  ran  F  C_  CC )
183182adantr 466 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ran  F 
C_  CC )
184 ffun 5740 . . . . . . . . . 10  |-  ( F : ( -u pi [,] pi ) --> CC  ->  Fun 
F )
18530, 184syl 17 . . . . . . . . 9  |-  ( ph  ->  Fun  F )
186185adantr 466 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  Fun  F )
18723a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  e.  RR )
18822a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  pi  e.  RR )
18995adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  X  e.  RR )
190144, 143eqeltrd 2508 . . . . . . . . . . . . 13  |-  ( ph  ->  ( H `  0
)  e.  RR )
191190adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  0 )  e.  RR )
192157, 156eqeltrd 2508 . . . . . . . . . . . . 13  |-  ( ph  ->  ( H `  M
)  e.  RR )
193192adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  M )  e.  RR )
194 simpr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )
195 eliccre 37403 . . . . . . . . . . . 12  |-  ( ( ( H `  0
)  e.  RR  /\  ( H `  M )  e.  RR  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  RR )
196191, 193, 194, 195syl3anc 1264 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  RR )
197189, 196readdcld 9666 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  RR )
198128adantl 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  = 
0 )  ->  ( Q `  i )  =  ( Q ` 
0 ) )
199198oveq1d 6312 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
200127, 199, 141, 143fvmptd 5962 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( H `  0
)  =  ( ( Q `  0 )  -  X ) )
201200oveq2d 6313 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( H `  0 ) )  =  ( X  +  ( ( Q `
 0 )  -  X ) ) )
20295recnd 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  CC )
203142recnd 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  0
)  e.  CC )
204202, 203pncan3d 9985 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( ( Q `  0
)  -  X ) )  =  ( Q `
 0 ) )
205201, 204, 83eqtrrd 2466 . . . . . . . . . . . 12  |-  ( ph  -> 
-u pi  =  ( X  +  ( H `
 0 ) ) )
206205adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  =  ( X  +  ( H `  0 ) ) )
207 elicc2 11695 . . . . . . . . . . . . . . 15  |-  ( ( ( H `  0
)  e.  RR  /\  ( H `  M )  e.  RR )  -> 
( t  e.  ( ( H `  0
) [,] ( H `
 M ) )  <-> 
( t  e.  RR  /\  ( H `  0
)  <_  t  /\  t  <_  ( H `  M ) ) ) )
208191, 193, 207syl2anc 665 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
t  e.  ( ( H `  0 ) [,] ( H `  M ) )  <->  ( t  e.  RR  /\  ( H `
 0 )  <_ 
t  /\  t  <_  ( H `  M ) ) ) )
209194, 208mpbid 213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
t  e.  RR  /\  ( H `  0 )  <_  t  /\  t  <_  ( H `  M
) ) )
210209simp2d 1018 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  0 )  <_  t )
211191, 196, 189, 210leadd2dd 10224 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  ( H `  0 ) )  <_  ( X  +  t ) )
212206, 211eqbrtrd 4438 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  <_  ( X  +  t ) )
213209simp3d 1019 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  <_  ( H `  M
) )
214196, 193, 189, 213leadd2dd 10224 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  <_  ( X  +  ( H `  M ) ) )
215157oveq2d 6313 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( H `  M ) )  =  ( X  +  ( ( Q `
 M )  -  X ) ) )
216155recnd 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  M
)  e.  CC )
217202, 216pncan3d 9985 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( ( Q `  M
)  -  X ) )  =  ( Q `
 M ) )
218215, 217, 103eqtrrd 2466 . . . . . . . . . . . 12  |-  ( ph  ->  pi  =  ( X  +  ( H `  M ) ) )
219218adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  pi  =  ( X  +  ( H `  M ) ) )
220214, 219breqtrrd 4444 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  <_  pi )
221187, 188, 197, 212, 220eliccd 37401 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  ( -u pi [,] pi ) )
222 fdm 5742 . . . . . . . . . . . 12  |-  ( F : ( -u pi [,] pi ) --> CC  ->  dom 
F  =  ( -u pi [,] pi ) )
22330, 222syl 17 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  (
-u pi [,] pi ) )
224223eqcomd 2428 . . . . . . . . . 10  |-  ( ph  ->  ( -u pi [,] pi )  =  dom  F )
225224adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( -u pi [,] pi )  =  dom  F )
226221, 225eleqtrd 2510 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  dom  F )
227 fvelrn 6022 . . . . . . . 8  |-  ( ( Fun  F  /\  ( X  +  t )  e.  dom  F )  -> 
( F `  ( X  +  t )
)  e.  ran  F
)
228186, 226, 227syl2anc 665 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( F `  ( X  +  t ) )  e.  ran  F )
229183, 228sseldd 3462 . . . . . 6  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( F `  ( X  +  t ) )  e.  CC )
230169, 167eqeltrd 2508 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  e.  RR )
231179, 178eqeltrd 2508 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  e.  RR )
23282, 60fssresd 5759 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
23340rexrd 9686 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
234233adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
23543rexrd 9686 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
236235adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
23795ad2antrr 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
238 elioore 11662 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  ->  t  e.  RR )
239238adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
240237, 239readdcld 9666 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  e.  RR )
241169oveq2d 6313 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  i ) )  =  ( X  +  ( ( Q `
 i )  -  X ) ) )
242202adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
24340recnd 9665 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
244242, 243pncan3d 9985 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( Q `  i )  -  X
) )  =  ( Q `  i ) )
245 eqidd 2421 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( Q `  i ) )
246241, 244, 2453eqtrrd 2466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( X  +  ( H `
 i ) ) )
247246adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  =  ( X  +  ( H `  i ) ) )
248230adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  e.  RR )
249 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )
250248rexrd 9686 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  e.  RR* )
251231rexrd 9686 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  e.  RR* )
252251adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  ( i  +  1 ) )  e.  RR* )
253 elioo2 11673 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) ) )
254250, 252, 253syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) ) )
255249, 254mpbid 213 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
t  e.  RR  /\  ( H `  i )  <  t  /\  t  <  ( H `  (
i  +  1 ) ) ) )
256255simp2d 1018 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  <  t )
257248, 239, 237, 256ltadd2dd 9790 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  ( H `  i ) )  < 
( X  +  t ) )
258247, 257eqbrtrd 4438 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( X  +  t ) )
259231adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  ( i  +  1 ) )  e.  RR )
260255simp3d 1019 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  <  ( H `  (
i  +  1 ) ) )
261239, 259, 237, 260ltadd2dd 9790 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  <  ( X  +  ( H `  ( i  +  1 ) ) ) )
262179oveq2d 6313 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( X  +  ( ( Q `
 ( i  +  1 ) )  -  X ) ) )
26343recnd 9665 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
264242, 263pncan3d 9985 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( Q `  ( i  +  1 ) )  -  X
) )  =  ( Q `  ( i  +  1 ) ) )
265262, 264eqtrd 2461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( Q `
 ( i  +  1 ) ) )
266265adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( Q `  (
i  +  1 ) ) )
267261, 266breqtrd 4442 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  <  ( Q `  (
i  +  1 ) ) )
268234, 236, 240, 258, 267eliood 37395 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
269 eqid 2420 . . . . . . . . . . . 12  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) )  =  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) )
270268, 269fmptd 6053 . . . . . . . . . . 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 ) ) ) )
271 fcompt 6066 . . . . . . . . . . 11  |-  ( ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC 
/\  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) : ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) --> ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  o.  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  =  ( s  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) `  s ) ) ) )
272232, 270, 271syl2anc 665 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  o.  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  =  ( s  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) `  s ) ) ) )
273 oveq2 6305 . . . . . . . . . . . . . . . 16  |-  ( t  =  r  ->  ( X  +  t )  =  ( X  +  r ) )
274273cbvmptv 4510 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) )  =  ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) )
275274fveq1i 5874 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) `  s )  =  ( ( r  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  r ) ) `
 s )
276275fveq2i 5876 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  ( ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) `  s ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  s
) )
277276mpteq2i 4501 . . . . . . . . . . . 12  |-  ( s  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  ( ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) `  s ) ) )  =  ( s  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  s
) ) )
278277a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  t ) ) `  s
) ) )  =  ( s  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  s
) ) ) )
279 fveq2 5873 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  s
)  =  ( ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) ) `  t ) )
280279fveq2d 5877 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) ) `  s ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  ( ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) ) `  t ) ) )
281280cbvmptv 4510 . . . . . . . . . . . 12  |-  ( s  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  ( ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) ) `  s ) ) )  =  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  t
) ) )
282281a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  s
) ) )  =  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  t
) ) ) )
283 eqidd 2421 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) )  =  ( r  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  r ) ) )
284 oveq2 6305 . . . . . . . . . . . . . . . 16  |-  ( r  =  t  ->  ( X  +  r )  =  ( X  +  t ) )
285284adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  (
i  +  1 ) ) ) )  /\  r  =  t )  ->  ( X  +  r )  =  ( X  +  t ) )
286283, 285, 249, 240fvmptd 5962 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  t
)  =  ( X  +  t ) )
287286fveq2d 5877 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) ) `  t ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  ( X  +  t
) ) )
288 fvres 5887 . . . . . . . . . . . . . 14  |-  ( ( X  +  t )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  =  ( F `  ( X  +  t
) ) )
289268, 288syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  =  ( F `  ( X  +  t
) ) )
290287, 289eqtrd 2461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) ) `  t ) )  =  ( F `
 ( X  +  t ) ) )
291290mpteq2dva 4504 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  t
) ) )  =  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  t )
) ) )
292278, 282, 2913eqtrd 2465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  (
( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  t ) ) `  s
) ) )  =  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  t )
) ) )
293272, 292eqtr2d 2462 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  t
) ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  o.  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) ) )
294 eqid 2420 . . . . . . . . . . 11  |-  ( t  e.  CC  |->  ( X  +  t ) )  =  ( t  e.  CC  |->  ( X  +  t ) )
295 ssid 3480 . . . . . . . . . . . . . . 15  |-  CC  C_  CC
296295a1i 11 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  CC  C_  CC )
297 id 23 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  X  e.  CC )
298296, 297, 296constcncfg 37535 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
t  e.  CC  |->  X )  e.  ( CC
-cn-> CC ) )
299 cncfmptid 21921 . . . . . . . . . . . . . . 15  |-  ( ( CC  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  CC  |->  t )  e.  ( CC
-cn-> CC ) )
300295, 295, 299mp2an 676 . . . . . . . . . . . . . 14  |-  ( t  e.  CC  |->  t )  e.  ( CC -cn-> CC )
301300a1i 11 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
t  e.  CC  |->  t )  e.  ( CC
-cn-> CC ) )
302298, 301addcncf 37537 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
t  e.  CC  |->  ( X  +  t ) )  e.  ( CC
-cn-> CC ) )
303242, 302syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  CC  |->  ( X  +  t ) )  e.  ( CC -cn-> CC ) )
304 ioosscn 37391 . . . . . . . . . . . 12  |-  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  C_  CC
305304a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  C_  CC )
306 ioosscn 37391 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
307306a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
308294, 303, 305, 307, 268cncfmptssg 37534 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) )  e.  ( ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) ) -cn-> ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
309308, 64cncfco 21916 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  o.  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  e.  ( ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) -cn-> CC ) )
310293, 309eqeltrd 2508 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  t
) ) )  e.  ( ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) ) -cn-> CC ) )
311233adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( Q `  i )  e.  RR* )
312235adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
313 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  r  e.  ran  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  t ) ) )
314 vex 3081 . . . . . . . . . . . . . . . . . 18  |-  r  e. 
_V
315269elrnmpt 5093 . . . . . . . . . . . . . . . . . 18  |-  ( r  e.  _V  ->  (
r  e.  ran  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) )  <->  E. t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) r  =  ( X  +  t ) ) )
316314, 315ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( r  e.  ran  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) )  <->  E. t  e.  (
( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) r  =  ( X  +  t ) )
317313, 316sylib 199 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  E. t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) r  =  ( X  +  t ) )
318 nfv 1751 . . . . . . . . . . . . . . . . . 18  |-  F/ t ( ph  /\  i  e.  ( 0..^ M ) )
319 nfmpt1 4507 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t
( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  t ) )
320319nfrn 5089 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t ran  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  t ) )
321320nfcri 2575 . . . . . . . . . . . . . . . . . 18  |-  F/ t  r  e.  ran  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) )
322318, 321nfan 1983 . . . . . . . . . . . . . . . . 17  |-  F/ t ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ran  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) ) )
323 nfv 1751 . . . . . . . . . . . . . . . . 17  |-  F/ t  r  e.  RR
324 simp3 1007 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  =  ( X  +  t ) )
325953ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  X  e.  RR )
3262383ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  t  e.  RR )
327325, 326readdcld 9666 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( X  +  t )  e.  RR )
328324, 327eqeltrd 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  e.  RR )
3293283exp 1204 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  r  e.  RR ) ) )
330329ad2antrr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  r  e.  RR ) ) )
331322, 323, 330rexlimd 2907 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( E. t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) r  =  ( X  +  t )  ->  r  e.  RR ) )
332317, 331mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  r  e.  RR )
333 nfv 1751 . . . . . . . . . . . . . . . . 17  |-  F/ t ( Q `  i
)  <  r
3342583adant3 1025 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( Q `  i )  <  ( X  +  t ) )
335 simp3 1007 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  =  ( X  +  t ) )
336334, 335breqtrrd 4444 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( Q `  i )  <  r )
3373363exp 1204 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  ( Q `  i )  <  r ) ) )
338337adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  ( Q `  i )  <  r ) ) )
339322, 333, 338rexlimd 2907 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( E. t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) r  =  ( X  +  t )  ->  ( Q `  i )  <  r
) )
340317, 339mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( Q `  i )  <  r
)
341 nfv 1751 . . . . . . . . . . . . . . . . 17  |-  F/ t  r  <  ( Q `
 ( i  +  1 ) )
3422673adant3 1025 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( X  +  t )  <  ( Q `  (
i  +  1 ) ) )
343335, 342eqbrtrd 4438 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  <  ( Q `  (
i  +  1 ) ) )
3443433exp 1204 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  r  <  ( Q `  (
i  +  1 ) ) ) ) )
345344adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  r  <  ( Q `  (
i  +  1 ) ) ) ) )
346322, 341, 345rexlimd 2907 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( E. t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) r  =  ( X  +  t )  ->  r  <  ( Q `  ( i  +  1 ) ) ) )
347317, 346mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  r  <  ( Q `  ( i  +  1 ) ) )
348311, 312, 332, 340, 347eliood 37395 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  r  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
349223ineq2d 3661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  i^i  dom  F )  =  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  i^i  ( -u pi [,] pi ) ) )
350349adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  i^i 
dom  F )  =  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  i^i  ( -u pi [,] pi ) ) )
351 dmres 5137 . . . . . . . . . . . . . . . . 17  |-  dom  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  i^i  dom  F )
352351a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  i^i  dom  F
) )
353 dfss 3448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  <->  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) )  =  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  i^i  ( -u pi [,] pi ) ) )
35460, 353sylib 199 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  =  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  i^i  ( -u pi [,] pi ) ) )
355350, 352, 3543eqtr4d 2471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
356355adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
357348, 356eleqtrrd 2511 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  r  e.  dom  ( F  |`  ( ( Q `  i