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

Theorem fourierdlem93 31871
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 31780 . . . . . . . . 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 16 . . . . . . . 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 210 . . . . . . 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 463 . . . . . 6  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
87simplld 754 . . . . 5  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
98eqcomd 2451 . . . 4  |-  ( ph  -> 
-u pi  =  ( Q `  0 ) )
107simplrd 31380 . . . . 5  |-  ( ph  ->  ( Q `  M
)  =  pi )
1110eqcomd 2451 . . . 4  |-  ( ph  ->  pi  =  ( Q `
 M ) )
129, 11oveq12d 6299 . . 3  |-  ( ph  ->  ( -u pi [,] pi )  =  (
( Q `  0
) [,] ( Q `
 M ) ) )
1312itgeq1d 31645 . 2  |-  ( ph  ->  S. ( -u pi [,] pi ) ( F `
 t )  _d t  =  S. ( ( Q `  0
) [,] ( Q `
 M ) ) ( F `  t
)  _d t )
14 0zd 10883 . . 3  |-  ( ph  ->  0  e.  ZZ )
15 nnuz 11126 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
162, 15syl6eleq 2541 . . . 4  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
17 1e0p1 11013 . . . . . 6  |-  1  =  ( 0  +  1 )
1817a1i 11 . . . . 5  |-  ( ph  ->  1  =  ( 0  +  1 ) )
1918fveq2d 5860 . . . 4  |-  ( ph  ->  ( ZZ>= `  1 )  =  ( ZZ>= `  (
0  +  1 ) ) )
2016, 19eleqtrd 2533 . . 3  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 0  +  1 ) ) )
213, 2, 1fourierdlem15 31793 . . . 4  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
22 pire 22827 . . . . . . 7  |-  pi  e.  RR
2322renegcli 9885 . . . . . 6  |-  -u pi  e.  RR
24 iccssre 11616 . . . . . 6  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
2523, 22, 24mp2an 672 . . . . 5  |-  ( -u pi [,] pi )  C_  RR
2625a1i 11 . . . 4  |-  ( ph  ->  ( -u pi [,] pi )  C_  RR )
2721, 26fssd 5730 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
287simprd 463 . . . 4  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
2928r19.21bi 2812 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
30 fourierdlem93.6 . . . . 5  |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )
3130adantr 465 . . . 4  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  F : ( -u pi [,] pi ) --> CC )
32 simpr 461 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )
3312eqcomd 2451 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 ) [,] ( Q `  M )
)  =  ( -u pi [,] pi ) )
3433adantr 465 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  (
( Q `  0
) [,] ( Q `
 M ) )  =  ( -u pi [,] pi ) )
3532, 34eleqtrd 2533 . . . 4  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  t  e.  ( -u pi [,] pi ) )
3631, 35ffvelrnd 6017 . . 3  |-  ( (
ph  /\  t  e.  ( ( Q ` 
0 ) [,] ( Q `  M )
) )  ->  ( F `  t )  e.  CC )
3727adantr 465 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
38 elfzofz 11824 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
3938adantl 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
4037, 39ffvelrnd 6017 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
41 fzofzp1 11890 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
4241adantl 466 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
4337, 42ffvelrnd 6017 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
4430feqmptd 5911 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( t  e.  ( -u pi [,] pi )  |->  ( F `
 t ) ) )
4544adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F  =  ( t  e.  ( -u pi [,] pi )  |->  ( F `  t ) ) )
4645reseq1d 5262 . . . . . . . 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 11620 . . . . . . . . . . 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 9649 . . . . . . . . . . . . . 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 9649 . . . . . . . . . . . . . 14  |-  pi  e.  RR*
5251a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  pi  e.  RR* )
5321ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
54 simplr 755 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0..^ M ) )
55 simpr 461 . . . . . . . . . . . . 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 31779 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  ( -u pi [,] pi ) )
5756ralrimiva 2857 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. t  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) t  e.  ( -u pi [,] pi ) )
58 dfss3 3479 . . . . . . . . . . 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 212 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
6048, 59sstrd 3499 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
6160resmptd 5315 . . . . . . . 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 2484 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) )
6362eqcomd 2451 . . . . . 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 2531 . . . . 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 6296 . . . . . 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 2533 . . . . 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 6296 . . . . . 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 2533 . . . . 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 31667 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  L^1 )
7330ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : ( -u pi [,] pi ) --> CC )
7473, 56ffvelrnd 6017 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  t )  e.  CC )
7540, 43, 72, 74ibliooicc 31660 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  L^1 )
7614, 20, 27, 29, 36, 75itgspltprt 31668 . 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 5870 . . . . . . . 8  |-  ( t  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  t )  =  ( F `  t ) )
7877eqcomd 2451 . . . . . . 7  |-  ( t  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  ( F `  t )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  t
) )
7978adantl 466 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  t )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  t
) )
8079itgeq2dv 22165 . . . . 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 2443 . . . . . 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 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : (
-u pi [,] pi )
--> CC )
8382, 59fssresd 5742 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
8448resabs1d 5293 . . . . . . 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 2531 . . . . . 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 6296 . . . . . . . 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 31551 . . . . . . . 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 2486 . . . . . . 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 2533 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
9084eqcomd 2451 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
9190oveq1d 6296 . . . . . . . 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 31535 . . . . . . . 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 2484 . . . . . . 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 2533 . . . . . 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 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
9781, 40, 43, 29, 83, 85, 89, 94, 96fourierdlem82 31860 . . . . 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 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  i )  e.  RR )
9943adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
10095ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  X  e.  RR )
10198, 100resubcld 9994 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  i
)  -  X )  e.  RR )
10299, 100resubcld 9994 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  X )  e.  RR )
103 simpr 461 . . . . . . . . . 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 31476 . . . . . . . . . 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 1229 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  e.  RR )
106100, 105readdcld 9626 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( X  +  t )  e.  RR )
107 elicc2 11599 . . . . . . . . . . . 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 661 . . . . . . . . . . 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 210 . . . . . . . . . 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 1010 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  (
( Q `  i
)  -  X )  <_  t )
11198, 100, 105lesubadd2d 10158 . . . . . . . . 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 210 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  ( Q `  i )  <_  ( X  +  t ) )
113109simp3d 1011 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i )  -  X ) [,] (
( Q `  (
i  +  1 ) )  -  X ) ) )  ->  t  <_  ( ( Q `  ( i  +  1 ) )  -  X
) )
114100, 105, 99leaddsub2d 10161 . . . . . . . . 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 232 . . . . . . . 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 31474 . . . . . . 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 5870 . . . . . . 7  |-  ( ( X  +  t )  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  =  ( F `  ( X  +  t
) ) )
118116, 117syl 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
) ) )
119118itgeq2dv 22165 . . . . 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 2488 . . . 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 13506 . . 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 6289 . . . . . . 7  |-  ( s  =  t  ->  ( X  +  s )  =  ( X  +  t ) )
123122fveq2d 5860 . . . . . 6  |-  ( s  =  t  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  t
) ) )
124123cbvitgv 22160 . . . . 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 5856 . . . . . . . . . 10  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
129128oveq1d 6296 . . . . . . . . 9  |-  ( i  =  0  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
130129adantl 466 . . . . . . . 8  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
1312nnzd 10974 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
13214, 131, 143jca 1177 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )
)
133 0le0 10632 . . . . . . . . . . 11  |-  0  <_  0
134133a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  <_  0 )
135 0red 9600 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  RR )
1362nnred 10558 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
1372nngt0d 10586 . . . . . . . . . . 11  |-  ( ph  ->  0  <  M )
138135, 136, 137ltled 9736 . . . . . . . . . 10  |-  ( ph  ->  0  <_  M )
139134, 138jca 532 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  0  /\  0  <_  M ) )
140 elfz2 11689 . . . . . . . . 9  |-  ( 0  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  0  e.  ZZ )  /\  (
0  <_  0  /\  0  <_  M ) ) )
141132, 139, 140sylanbrc 664 . . . . . . . 8  |-  ( ph  ->  0  e.  ( 0 ... M ) )
1428, 23syl6eqel 2539 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  e.  RR )
143142, 95resubcld 9994 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
0 )  -  X
)  e.  RR )
144127, 130, 141, 143fvmptd 5946 . . . . . . 7  |-  ( ph  ->  ( H `  0
)  =  ( ( Q `  0 )  -  X ) )
1458oveq1d 6296 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  -  X
)  =  ( -u pi  -  X ) )
146144, 145eqtr2d 2485 . . . . . 6  |-  ( ph  ->  ( -u pi  -  X )  =  ( H `  0 ) )
147 fveq2 5856 . . . . . . . . . 10  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
148147oveq1d 6296 . . . . . . . . 9  |-  ( i  =  M  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 M )  -  X ) )
149148adantl 466 . . . . . . . 8  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 M )  -  X ) )
15014, 131, 1313jca 1177 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  M  e.  ZZ )
)
151136leidd 10126 . . . . . . . . . 10  |-  ( ph  ->  M  <_  M )
152138, 151jca 532 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  M  /\  M  <_  M ) )
153 elfz2 11689 . . . . . . . . 9  |-  ( M  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  M  e.  ZZ )  /\  (
0  <_  M  /\  M  <_  M ) ) )
154150, 152, 153sylanbrc 664 . . . . . . . 8  |-  ( ph  ->  M  e.  ( 0 ... M ) )
15510, 22syl6eqel 2539 . . . . . . . . 9  |-  ( ph  ->  ( Q `  M
)  e.  RR )
156155, 95resubcld 9994 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  M )  -  X
)  e.  RR )
157127, 149, 154, 156fvmptd 5946 . . . . . . 7  |-  ( ph  ->  ( H `  M
)  =  ( ( Q `  M )  -  X ) )
15810oveq1d 6296 . . . . . . 7  |-  ( ph  ->  ( ( Q `  M )  -  X
)  =  ( pi 
-  X ) )
159157, 158eqtr2d 2485 . . . . . 6  |-  ( ph  ->  ( pi  -  X
)  =  ( H `
 M ) )
160146, 159oveq12d 6299 . . . . 5  |-  ( ph  ->  ( ( -u pi  -  X ) [,] (
pi  -  X )
)  =  ( ( H `  0 ) [,] ( H `  M ) ) )
161160itgeq1d 31645 . . . 4  |-  ( ph  ->  S. ( ( -u pi  -  X ) [,] ( pi  -  X
) ) ( F `
 ( X  +  t ) )  _d t  =  S. ( ( H `  0
) [,] ( H `
 M ) ) ( F `  ( X  +  t )
)  _d t )
16227fnvinran 31343 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
16395adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
164162, 163resubcld 9994 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  -  X )  e.  RR )
165164, 126fmptd 6040 . . . . . 6  |-  ( ph  ->  H : ( 0 ... M ) --> RR )
16640, 43, 96, 29ltsub1dd 10171 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) )
16739, 164syldan 470 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  e.  RR )
168126fvmpt2 5948 . . . . . . . 8  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  -  X
)  e.  RR )  ->  ( H `  i )  =  ( ( Q `  i
)  -  X ) )
16939, 167, 168syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  =  ( ( Q `  i
)  -  X ) )
170 fveq2 5856 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
171170oveq1d 6296 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 j )  -  X ) )
172171cbvmptv 4528 . . . . . . . . . 10  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  -  X ) )
173126, 172eqtri 2472 . . . . . . . . 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 5856 . . . . . . . . . 10  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
176175oveq1d 6296 . . . . . . . . 9  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
177176adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
17843, 96resubcld 9994 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  X )  e.  RR )
179174, 177, 42, 178fvmptd 5946 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  -  X ) )
180166, 169, 1793brtr4d 4467 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  <  ( H `  ( i  +  1 ) ) )
181 frn 5727 . . . . . . . . 9  |-  ( F : ( -u pi [,] pi ) --> CC  ->  ran 
F  C_  CC )
18230, 181syl 16 . . . . . . . 8  |-  ( ph  ->  ran  F  C_  CC )
183182adantr 465 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ran  F 
C_  CC )
184 ffun 5723 . . . . . . . . . 10  |-  ( F : ( -u pi [,] pi ) --> CC  ->  Fun 
F )
18530, 184syl 16 . . . . . . . . 9  |-  ( ph  ->  Fun  F )
186185adantr 465 . . . . . . . 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 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  X  e.  RR )
190144, 143eqeltrd 2531 . . . . . . . . . . . . 13  |-  ( ph  ->  ( H `  0
)  e.  RR )
191190adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  0 )  e.  RR )
192157, 156eqeltrd 2531 . . . . . . . . . . . . 13  |-  ( ph  ->  ( H `  M
)  e.  RR )
193192adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  M )  e.  RR )
194 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )
195 eliccre 31476 . . . . . . . . . . . 12  |-  ( ( ( H `  0
)  e.  RR  /\  ( H `  M )  e.  RR  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  RR )
196191, 193, 194, 195syl3anc 1229 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  e.  RR )
197189, 196readdcld 9626 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  RR )
198128adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  = 
0 )  ->  ( Q `  i )  =  ( Q ` 
0 ) )
199198oveq1d 6296 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 0 )  -  X ) )
200127, 199, 141, 143fvmptd 5946 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( H `  0
)  =  ( ( Q `  0 )  -  X ) )
201200oveq2d 6297 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( H `  0 ) )  =  ( X  +  ( ( Q `
 0 )  -  X ) ) )
20295recnd 9625 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  CC )
203142recnd 9625 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  0
)  e.  CC )
204202, 203pncan3d 9939 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( ( Q `  0
)  -  X ) )  =  ( Q `
 0 ) )
205201, 204, 83eqtrrd 2489 . . . . . . . . . . . 12  |-  ( ph  -> 
-u pi  =  ( X  +  ( H `
 0 ) ) )
206205adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  =  ( X  +  ( H `  0 ) ) )
207 elicc2 11599 . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  (
t  e.  RR  /\  ( H `  0 )  <_  t  /\  t  <_  ( H `  M
) ) )
210209simp2d 1010 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( H `  0 )  <_  t )
211191, 196, 189, 210leadd2dd 10174 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  ( H `  0 ) )  <_  ( X  +  t ) )
212206, 211eqbrtrd 4457 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  -u pi  <_  ( X  +  t ) )
213209simp3d 1011 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  t  <_  ( H `  M
) )
214196, 193, 189, 213leadd2dd 10174 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  <_  ( X  +  ( H `  M ) ) )
215157oveq2d 6297 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( H `  M ) )  =  ( X  +  ( ( Q `
 M )  -  X ) ) )
216155recnd 9625 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  M
)  e.  CC )
217202, 216pncan3d 9939 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( ( Q `  M
)  -  X ) )  =  ( Q `
 M ) )
218215, 217, 103eqtrrd 2489 . . . . . . . . . . . 12  |-  ( ph  ->  pi  =  ( X  +  ( H `  M ) ) )
219218adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  pi  =  ( X  +  ( H `  M ) ) )
220214, 219breqtrrd 4463 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  <_  pi )
221187, 188, 197, 212, 220eliccd 31474 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  ( -u pi [,] pi ) )
222 fdm 5725 . . . . . . . . . . . 12  |-  ( F : ( -u pi [,] pi ) --> CC  ->  dom 
F  =  ( -u pi [,] pi ) )
22330, 222syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  (
-u pi [,] pi ) )
224223eqcomd 2451 . . . . . . . . . 10  |-  ( ph  ->  ( -u pi [,] pi )  =  dom  F )
225224adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( -u pi [,] pi )  =  dom  F )
226221, 225eleqtrd 2533 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( X  +  t )  e.  dom  F )
227 fvelrn 6009 . . . . . . . 8  |-  ( ( Fun  F  /\  ( X  +  t )  e.  dom  F )  -> 
( F `  ( X  +  t )
)  e.  ran  F
)
228186, 226, 227syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( F `  ( X  +  t ) )  e.  ran  F )
229183, 228sseldd 3490 . . . . . 6  |-  ( (
ph  /\  t  e.  ( ( H ` 
0 ) [,] ( H `  M )
) )  ->  ( F `  ( X  +  t ) )  e.  CC )
230169, 167eqeltrd 2531 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  i )  e.  RR )
231179, 178eqeltrd 2531 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  e.  RR )
23282, 60fssresd 5742 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
23340rexrd 9646 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
234233adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
23543rexrd 9646 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
236235adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
23795ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
238 elioore 11569 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  ->  t  e.  RR )
239238adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
240237, 239readdcld 9626 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  e.  RR )
241169oveq2d 6297 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  i ) )  =  ( X  +  ( ( Q `
 i )  -  X ) ) )
242202adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
24340recnd 9625 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
244242, 243pncan3d 9939 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( Q `  i )  -  X
) )  =  ( Q `  i ) )
245 eqidd 2444 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( Q `  i ) )
246241, 244, 2453eqtrrd 2489 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( X  +  ( H `
 i ) ) )
247246adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  =  ( X  +  ( H `  i ) ) )
248230adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  e.  RR )
249 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )
250248rexrd 9646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  e.  RR* )
251231rexrd 9646 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H `  ( i  +  1 ) )  e.  RR* )
252251adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  ( i  +  1 ) )  e.  RR* )
253 elioo2 11580 . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  (
t  e.  RR  /\  ( H `  i )  <  t  /\  t  <  ( H `  (
i  +  1 ) ) ) )
256255simp2d 1010 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  i )  <  t )
257248, 239, 237, 256ltadd2dd 9744 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  ( H `  i ) )  < 
( X  +  t ) )
258247, 257eqbrtrd 4457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( X  +  t ) )
259231adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( H `  ( i  +  1 ) )  e.  RR )
260255simp3d 1011 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  t  <  ( H `  (
i  +  1 ) ) )
261239, 259, 237, 260ltadd2dd 9744 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  <  ( X  +  ( H `  ( i  +  1 ) ) ) )
262179oveq2d 6297 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( X  +  ( ( Q `
 ( i  +  1 ) )  -  X ) ) )
26343recnd 9625 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
264242, 263pncan3d 9939 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( Q `  ( i  +  1 ) )  -  X
) )  =  ( Q `  ( i  +  1 ) ) )
265262, 264eqtrd 2484 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( Q `
 ( i  +  1 ) ) )
266265adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  ( H `  ( i  +  1 ) ) )  =  ( Q `  (
i  +  1 ) ) )
267261, 266breqtrd 4461 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  <  ( Q `  (
i  +  1 ) ) )
268234, 236, 240, 258, 267eliood 31467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) ) )  ->  ( X  +  t )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
269 eqid 2443 . . . . . . . . . . . 12  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) )  =  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) )
270268, 269fmptd 6040 . . . . . . . . . . 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 6052 . . . . . . . . . . 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 661 . . . . . . . . . 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 6289 . . . . . . . . . . . . . . . 16  |-  ( t  =  r  ->  ( X  +  t )  =  ( X  +  r ) )
274273cbvmptv 4528 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) )  =  ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) )
275274fveq1i 5857 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) `  s )  =  ( ( r  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  r ) ) `
 s )
276275fveq2i 5859 . . . . . . . . . . . . 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 4520 . . . . . . . . . . . 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 5856 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  (
( r  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  r ) ) `  s
)  =  ( ( r  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  r ) ) `  t ) )
280279fveq2d 5860 . . . . . . . . . . . . 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 4528 . . . . . . . . . . . 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 2444 . . . . . . . . . . . . . . 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 6289 . . . . . . . . . . . . . . . 16  |-  ( r  =  t  ->  ( X  +  r )  =  ( X  +  t ) )
285284adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  (
i  +  1 ) ) ) )  /\  r  =  t )  ->  ( X  +  r )  =  ( X  +  t ) )
286283, 285, 249, 240fvmptd 5946 . . . . . . . . . . . . . 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 5860 . . . . . . . . . . . . 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 5870 . . . . . . . . . . . . . 14  |-  ( ( X  +  t )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  ( X  +  t ) )  =  ( F `  ( X  +  t
) ) )
289268, 288syl 16 . . . . . . . . . . . . 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 2484 . . . . . . . . . . . 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 4523 . . . . . . . . . . 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 2488 . . . . . . . . . 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 2485 . . . . . . . . 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 2443 . . . . . . . . . . 11  |-  ( t  e.  CC  |->  ( X  +  t ) )  =  ( t  e.  CC  |->  ( X  +  t ) )
295 ssid 3508 . . . . . . . . . . . . . . 15  |-  CC  C_  CC
296295a1i 11 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  CC  C_  CC )
297 id 22 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  X  e.  CC )
298296, 297, 296constcncfg 31580 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
t  e.  CC  |->  X )  e.  ( CC
-cn-> CC ) )
299 cncfmptid 21393 . . . . . . . . . . . . . . 15  |-  ( ( CC  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  CC  |->  t )  e.  ( CC
-cn-> CC ) )
300295, 295, 299mp2an 672 . . . . . . . . . . . . . 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 31582 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
t  e.  CC  |->  ( X  +  t ) )  e.  ( CC
-cn-> CC ) )
303242, 302syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  CC  |->  ( X  +  t ) )  e.  ( CC -cn-> CC ) )
304 ioosscn 31463 . . . . . . . . . . . 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 31463 . . . . . . . . . . . 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 31579 . . . . . . . . . 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 21388 . . . . . . . . 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 2531 . . . . . . . 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 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  ( Q `  i )  e.  RR* )
312235adantr 465 . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . 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 3098 . . . . . . . . . . . . . . . . . 18  |-  r  e. 
_V
315269elrnmpt 5239 . . . . . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . . . 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 1694 . . . . . . . . . . . . . . . . . 18  |-  F/ t ( ph  /\  i  e.  ( 0..^ M ) )
319 nfmpt1 4526 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t
( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  t ) )
320319nfrn 5235 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t ran  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) ) 
|->  ( X  +  t ) )
321320nfcri 2598 . . . . . . . . . . . . . . . . . 18  |-  F/ t  r  e.  ran  (
t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) )
322318, 321nfan 1914 . . . . . . . . . . . . . . . . 17  |-  F/ t ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ran  ( t  e.  ( ( H `
 i ) (,) ( H `  (
i  +  1 ) ) )  |->  ( X  +  t ) ) )
323 nfv 1694 . . . . . . . . . . . . . . . . 17  |-  F/ t  r  e.  RR
324 simp3 999 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  =  ( X  +  t ) )
325953ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  X  e.  RR )
3262383ad2ant2 1019 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  t  e.  RR )
327325, 326readdcld 9626 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( X  +  t )  e.  RR )
328324, 327eqeltrd 2531 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  e.  RR )
3293283exp 1196 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( t  e.  ( ( H `  i
) (,) ( H `
 ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  r  e.  RR ) ) )
330329ad2antrr 725 . . . . . . . . . . . . . . . . 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 2927 . . . . . . . . . . . . . . . 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 1694 . . . . . . . . . . . . . . . . 17  |-  F/ t ( Q `  i
)  <  r
3342583adant3 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( Q `  i )  <  ( X  +  t ) )
335 simp3 999 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  =  ( X  +  t ) )
336334, 335breqtrrd 4463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( Q `  i )  <  r )
3373363exp 1196 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  ( Q `  i )  <  r ) ) )
338337adantr 465 . . . . . . . . . . . . . . . . 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 2927 . . . . . . . . . . . . . . . 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 1694 . . . . . . . . . . . . . . . . 17  |-  F/ t  r  <  ( Q `
 ( i  +  1 ) )
3422673adant3 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  ( X  +  t )  <  ( Q `  (
i  +  1 ) ) )
343335, 342eqbrtrd 4457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  /\  r  =  ( X  +  t ) )  ->  r  <  ( Q `  (
i  +  1 ) ) )
3443433exp 1196 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  ->  ( r  =  ( X  +  t )  ->  r  <  ( Q `  (
i  +  1 ) ) ) ) )
345344adantr 465 . . . . . . . . . . . . . . . . 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 2927 . . . . . . . . . . . . . . . 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 31467 . . . . . . . . . . . . . 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 3685 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  i^i  dom  F )  =  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  i^i  ( -u pi [,] pi ) ) )
350349adantr 465 . . . . . . . . . . . . . . . 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 5284 . . . . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  =  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  i^i  ( -u pi [,] pi ) ) )
355350, 352, 3543eqtr4d 2494 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
356355adantr 465 . . . . . . . . . . . . . 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 2534 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e. 
ran  ( t  e.  ( ( H `  i ) (,) ( H `  ( i  +  1 ) ) )  |->  ( X  +  t ) ) )  ->  r  e.  dom  ( F  |`  ( ( Q