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

Theorem fourierdlem73 32144
Description: A version of the Reimann Lebesgue lemma: as  r increases, the integral in  S goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem73.a  |-  ( ph  ->  A  e.  RR )
fourierdlem73.b  |-  ( ph  ->  B  e.  RR )
fourierdlem73.f  |-  ( ph  ->  F : ( A [,] B ) --> CC )
fourierdlem73.m  |-  ( ph  ->  M  e.  NN )
fourierdlem73.qf  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
fourierdlem73.q0  |-  ( ph  ->  ( Q `  0
)  =  A )
fourierdlem73.qm  |-  ( ph  ->  ( Q `  M
)  =  B )
fourierdlem73.qilt  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
fourierdlem73.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem73.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
fourierdlem73.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem73.g  |-  G  =  ( RR  _D  F
)
fourierdlem73.gcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem73.gbd  |-  ( ph  ->  E. y  e.  RR  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
fourierdlem73.s  |-  S  =  ( r  e.  RR+  |->  S. ( A (,) B
) ( ( F `
 x )  x.  ( sin `  (
r  x.  x ) ) )  _d x )
fourierdlem73.d  |-  D  =  ( x  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
Assertion
Ref Expression
fourierdlem73  |-  ( ph  ->  A. e  e.  RR+  E. n  e.  NN  A. r  e.  ( n (,) +oo ) ( abs `  S. ( A (,) B ) ( ( F `  x )  x.  ( sin `  (
r  x.  x ) ) )  _d x )  <  e )
Distinct variable groups:    x, A    x, B    D, r, x, y   
i, F, n, x   
x, G, y    x, L    e, M, i, n, r, x    y, M, i    Q, i, n, r, x    y, Q    x, R    ph, e, i, n, r, x    ph, y
Allowed substitution hints:    A( y, e, i, n, r)    B( y, e, i, n, r)    D( e, i, n)    Q( e)    R( y, e, i, n, r)    S( x, y, e, i, n, r)    F( y, e, r)    G( e, i, n, r)    L( y, e, i, n, r)

Proof of Theorem fourierdlem73
Dummy variables  m  z  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem73.gcn . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
2 cncff 21523 . . . . . . . . . . . . . 14  |-  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
31, 2syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
4 ax-resscn 9566 . . . . . . . . . . . . . . . . 17  |-  RR  C_  CC
54a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  CC )
6 fourierdlem73.qf . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
7 fourierdlem73.a . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  RR )
8 fourierdlem73.b . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR )
97, 8iccssred 31721 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A [,] B
)  C_  RR )
106, 9fssd 5746 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
1110adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
12 elfzofz 11841 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
1312adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
1411, 13ffvelrnd 6033 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
15 fzofzp1 11912 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
1615adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
1711, 16ffvelrnd 6033 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
1814, 17iccssred 31721 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  RR )
19 limccl 22405 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) )  C_  CC
20 fourierdlem73.r . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
2119, 20sseldi 3497 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  CC )
2221adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  R  e.  CC )
23 limccl 22405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  C_  CC
24 fourierdlem73.l . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
2523, 24sseldi 3497 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  CC )
2625adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  L  e.  CC )
27 fourierdlem73.f . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : ( A [,] B ) --> CC )
2827ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : ( A [,] B ) --> CC )
297ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR )
308ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR )
3114adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
3217adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
33 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
34 eliccre 31722 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
3531, 32, 33, 34syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
367rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  e.  RR* )
3736adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
388rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  RR* )
3938adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
406adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
4140, 13ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( A [,] B ) )
42 iccgelb 11606 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 i )  e.  ( A [,] B
) )  ->  A  <_  ( Q `  i
) )
4337, 39, 41, 42syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  <_  ( Q `  i )
)
4443adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  ( Q `  i
) )
4531rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
4632rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
47 iccgelb 11606 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
4845, 46, 33, 47syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
4929, 31, 35, 44, 48letrd 9756 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  x )
50 iccleub 11605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
5145, 46, 33, 50syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
5236ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
5338ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
5440, 16ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
5554adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
56 iccleub 11605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 ( i  +  1 ) )  e.  ( A [,] B
) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
5752, 53, 55, 56syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
5835, 32, 30, 51, 57letrd 9756 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  B )
5929, 30, 35, 49, 58eliccd 31720 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( A [,] B
) )
6028, 59ffvelrnd 6033 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
6126, 60ifcld 3987 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  e.  CC )
6222, 61ifcld 3987 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  e.  CC )
63 fourierdlem73.d . . . . . . . . . . . . . . . . 17  |-  D  =  ( x  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
6462, 63fmptd 6056 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  D : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
65 eqid 2457 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6665tgioo2 21434 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
67 iccntr 21452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
6814, 17, 67syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
695, 18, 64, 66, 65, 68dvresntr 31895 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
70 ioossicc 11635 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
7170sseli 3495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
7271adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
73 fvres 5886 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
7472, 73syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
7572, 62syldan 470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  e.  CC )
7663fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  /\  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) )  e.  CC )  ->  ( D `  x )  =  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
7772, 75, 76syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  x )  =  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
7814adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
7972, 45syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
8072, 46syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
81 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
82 ioogtlb 31710 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8379, 80, 81, 82syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8478, 83gtned 9737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  i
) )
8584neneqd 2659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  i ) )
8685iffalsed 3955 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )  =  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
87 elioore 11584 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  RR )
8887adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
89 iooltub 31730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  <  ( Q `  (
i  +  1 ) ) )
9079, 80, 81, 89syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  <  ( Q `  (
i  +  1 ) ) )
9188, 90ltned 9738 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  (
i  +  1 ) ) )
9291neneqd 2659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  ( i  +  1 ) ) )
9392iffalsed 3955 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  ( F `
 x ) )
9477, 86, 933eqtrrd 2503 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  =  ( D `  x ) )
9574, 94eqtr2d 2499 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  x )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  x
) )
9695ralrimiva 2871 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( D `  x
)  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) ) `  x ) )
97 ffn 5737 . . . . . . . . . . . . . . . . . . . 20  |-  ( D : ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) --> CC  ->  D  Fn  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) )
9864, 97syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  D  Fn  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
99 ffn 5737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : ( A [,] B ) --> CC  ->  F  Fn  ( A [,] B ) )
10027, 99syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F  Fn  ( A [,] B ) )
101100adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F  Fn  ( A [,] B ) )
102 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
10337, 39, 40, 102fourierdlem8 32079 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( A [,] B ) )
104 fnssres 5700 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F  Fn  ( A [,] B )  /\  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  C_  ( A [,] B ) )  -> 
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  Fn  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
105101, 103, 104syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  Fn  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
10670a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
107 fvreseq 5990 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( D  Fn  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) )  /\  ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  Fn  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  /\  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  (
( D  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  <->  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( D `  x )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) )
10898, 105, 106, 107syl21anc 1227 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  <->  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( D `  x )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x ) ) )
10996, 108mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
110106resabs1d 5313 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
111109, 110eqtrd 2498 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
112111oveq2d 6312 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( RR 
_D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
11327adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : ( A [,] B ) --> CC )
1149adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A [,] B )  C_  RR )
115106, 18sstrd 3509 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
11665, 66dvres 22441 . . . . . . . . . . . . . . . . 17  |-  ( ( ( RR  C_  CC  /\  F : ( A [,] B ) --> CC )  /\  ( ( A [,] B ) 
C_  RR  /\  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  RR ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) )
1175, 113, 114, 115, 116syl22anc 1229 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) )
118 fourierdlem73.g . . . . . . . . . . . . . . . . . . 19  |-  G  =  ( RR  _D  F
)
119118eqcomi 2470 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
_D  F )  =  G
120119a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  F )  =  G )
121 iooretop 21399 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )
122 retop 21394 . . . . . . . . . . . . . . . . . . 19  |-  ( topGen ` 
ran  (,) )  e.  Top
123 uniretop 21395 . . . . . . . . . . . . . . . . . . . 20  |-  RR  =  U. ( topGen `  ran  (,) )
124123isopn3 19694 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR )  ->  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
125122, 115, 124sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
126121, 125mpbii 211 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
127120, 126reseq12d 5284 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
128117, 127eqtrd 2498 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
12969, 112, 1283eqtrd 2502 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
130129feq1d 5723 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  D ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC  <->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC ) )
1313, 130mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
132131feqmptd 5926 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR  _D  D
) `  x )
) )
133132, 129eqtr3d 2500 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  =  ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
134 ioombl 22101 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  e. 
dom  vol
135134a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  e.  dom  vol )
136 fourierdlem73.qilt . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
13714, 17, 136ltled 9750 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <_  ( Q `  ( i  +  1 ) ) )
138 volioo 31929 . . . . . . . . . . . . 13  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR  /\  ( Q `  i )  <_  ( Q `  (
i  +  1 ) ) )  ->  ( vol `  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  ( i  +  1 ) )  -  ( Q `  i )
) )
13914, 17, 137, 138syl3anc 1228 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( Q `  ( i  +  1 ) )  -  ( Q `  i ) ) )
14017, 14resubcld 10008 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  ( Q `  i ) )  e.  RR )
141139, 140eqeltrd 2545 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  RR )
142 fourierdlem73.gbd . . . . . . . . . . . . 13  |-  ( ph  ->  E. y  e.  RR  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
143142adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. y  e.  RR  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
144 nfv 1708 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )
145 nfra1 2838 . . . . . . . . . . . . . . . 16  |-  F/ x A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y
146144, 145nfan 1929 . . . . . . . . . . . . . . 15  |-  F/ x
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )
147 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
148 fdm 5741 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC  ->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
1493, 148syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
150149adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  dom  ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
151147, 150eleqtrd 2547 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
152 fvres 5886 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( G `  x ) )
153151, 152syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  -> 
( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
)  =  ( G `
 x ) )
154153fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  -> 
( abs `  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  =  ( abs `  ( G `  x
) ) )
155154adant423 31607 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  ( abs `  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
) )  =  ( abs `  ( G `
 x ) ) )
156 simplr 755 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  A. x  e.  dom  G ( abs `  ( G `  x
) )  <_  y
)
157 ssdmres 5305 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  G  <->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
158149, 157sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  G )
159158sselda 3499 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  dom  G )
160151, 159syldan 470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  G )
161160adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  G )
162 rsp 2823 . . . . . . . . . . . . . . . . . . 19  |-  ( A. x  e.  dom  G ( abs `  ( G `
 x ) )  <_  y  ->  (
x  e.  dom  G  ->  ( abs `  ( G `  x )
)  <_  y )
)
163156, 161, 162sylc 60 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  ( abs `  ( G `  x
) )  <_  y
)
164163adantllr 718 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  ( abs `  ( G `  x
) )  <_  y
)
165155, 164eqbrtrd 4476 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  ( abs `  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
) )  <_  y
)
166165ex 434 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )  ->  ( x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  <_  y )
)
167146, 166ralrimi 2857 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )  ->  A. x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ( abs `  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  <_  y )
168167ex 434 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  ->  ( A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y  ->  A. x  e.  dom  ( G  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ( abs `  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )  <_ 
y ) )
169168reximdva 2932 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( E. y  e.  RR  A. x  e. 
dom  G ( abs `  ( G `  x
) )  <_  y  ->  E. y  e.  RR  A. x  e.  dom  ( G  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ( abs `  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )  <_ 
y ) )
170143, 169mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. y  e.  RR  A. x  e.  dom  ( G  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ( abs `  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )  <_ 
y )
171135, 141, 1, 170cnbdibl 31943 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  L^1 )
172133, 171eqeltrd 2545 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  e.  L^1 )
173172adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  e  e.  RR+ )  ->  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( RR  _D  D ) `
 x ) )  e.  L^1 )
174134a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  e.  dom  vol )
175141adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  ( vol `  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  RR )
176133, 1eqeltrd 2545 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
177176adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR  _D  D
) `  x )
)  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
178 coscn 22966 . . . . . . . . . . . . . 14  |-  cos  e.  ( CC -cn-> CC )
179178a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  cos  e.  ( CC -cn-> CC ) )
180 ioosscn 31709 . . . . . . . . . . . . . . . 16  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
181180a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  CC )
182 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  RR )
183182recnd 9639 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  CC )
184 ssid 3518 . . . . . . . . . . . . . . . 16  |-  CC  C_  CC
185184a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  CC  C_  CC )
186181, 183, 185constcncfg 31855 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  r )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
187180a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC )
188184a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  CC  C_  CC )
189187, 188idcncfg 31856 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  x )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
190189ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  x )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
191186, 190mulcncf 21985 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( r  x.  x ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
192179, 191cncfmpt1f 21543 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( cos `  ( r  x.  x ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
193192negcncfg 31865 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  -u ( cos `  ( r  x.  x ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
194177, 193mulcncf 21985 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( RR  _D  D ) `  x
)  x.  -u ( cos `  ( r  x.  x ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
195 nfv 1708 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ph  /\  i  e.  ( 0..^ M ) )
196195, 145nfan 1929 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
197129fveq1d 5874 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  D ) `  x )  =  ( ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )
198197, 152sylan9eq 2518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  =  ( G `  x ) )
199198fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR 
_D  D ) `  x ) )  =  ( abs `  ( G `  x )
) )
200199adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR  _D  D ) `  x
) )  =  ( abs `  ( G `
 x ) ) )
201 simplr 755 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  A. x  e.  dom  G ( abs `  ( G `  x
) )  <_  y
)
202159adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  x  e.  dom  G )
203201, 202, 162sylc 60 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  x
) )  <_  y
)
204200, 203eqbrtrd 4476 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR  _D  D ) `  x
) )  <_  y
)
205204ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G ( abs `  ( G `  x
) )  <_  y
)  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( abs `  ( ( RR  _D  D ) `  x
) )  <_  y
) )
206196, 205ralrimi 2857 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G ( abs `  ( G `  x
) )  <_  y
)  ->  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
207206ex 434 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A. x  e.  dom  G ( abs `  ( G `  x
) )  <_  y  ->  A. x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
)
208207reximdv 2931 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( E. y  e.  RR  A. x  e. 
dom  G ( abs `  ( G `  x
) )  <_  y  ->  E. y  e.  RR  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y ) )
209143, 208mpd 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. y  e.  RR  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )
210209adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  E. y  e.  RR  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
211 eqidd 2458 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( RR  _D  D ) `
 x )  x.  -u ( cos `  (
r  x.  x ) ) ) )  =  ( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( ( RR 
_D  D ) `  x )  x.  -u ( cos `  ( r  x.  x ) ) ) ) )
212 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( RR  _D  D
) `  x )  =  ( ( RR 
_D  D ) `  z ) )
213 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
214213anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  <->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) ) )
215 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  ( G `  x )  =  ( G `  z ) )
216212, 215eqeq12d 2479 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( RR  _D  D ) `  x
)  =  ( G `
 x )  <->  ( ( RR  _D  D ) `  z )  =  ( G `  z ) ) )
217214, 216imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  (
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( RR  _D  D ) `  x
)  =  ( G `
 x ) )  <-> 
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( RR  _D  D ) `  z
)  =  ( G `
 z ) ) ) )
218217, 198chvarv 2015 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  z )  =  ( G `  z ) )
219212, 218sylan9eqr 2520 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  x  =  z )  ->  ( ( RR  _D  D ) `  x
)  =  ( G `
 z ) )
220 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
r  x.  x )  =  ( r  x.  z ) )
221220fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( cos `  ( r  x.  x ) )  =  ( cos `  (
r  x.  z ) ) )
222221negeqd 9833 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  -u ( cos `  ( r  x.  x ) )  = 
-u ( cos `  (
r  x.  z ) ) )
223222adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  x  =  z )  -> 
-u ( cos `  (
r  x.  x ) )  =  -u ( cos `  ( r  x.  z ) ) )
224219, 223oveq12d 6314 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  x  =  z )  ->  ( ( ( RR 
_D  D ) `  x )  x.  -u ( cos `  ( r  x.  x ) ) )  =  ( ( G `
 z )  x.  -u ( cos `  (
r  x.  z ) ) ) )
225224adantllr 718 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  /\  x  =  z )  ->  (
( ( RR  _D  D ) `  x
)  x.  -u ( cos `  ( r  x.  x ) ) )  =  ( ( G `
 z )  x.  -u ( cos `  (
r  x.  z ) ) ) )
226 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
227 fvres 5886 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
228227adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
2293ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  e.  CC )
230228, 229eqeltrrd 2546 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
231230adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
232 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
r  e.  RR )
233 elioore 11584 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  RR )
234233adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
z  e.  RR )
235232, 234remulcld 9641 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  RR )
236235recnd 9639 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  CC )
237236coscld 13878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( cos `  (
r  x.  z ) )  e.  CC )
238237negcld 9937 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -u ( cos `  (
r  x.  z ) )  e.  CC )
239238adantll 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  -u ( cos `  ( r  x.  z
) )  e.  CC )
240231, 239mulcld 9633 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( ( G `  z )  x.  -u ( cos `  (
r  x.  z ) ) )  e.  CC )
241211, 225, 226, 240fvmptd 5961 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( RR  _D  D ) `  x
)  x.  -u ( cos `  ( r  x.  x ) ) ) ) `  z )  =  ( ( G `
 z )  x.  -u ( cos `  (
r  x.  z ) ) ) )
242241fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( RR  _D  D ) `
 x )  x.  -u ( cos `  (
r  x.  x ) ) ) ) `  z ) )  =  ( abs `  (
( G `  z
)  x.  -u ( cos `  ( r  x.  z ) ) ) ) )
243242adant423 31607 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( RR  _D  D ) `
 x )  x.  -u ( cos `  (
r  x.  x ) ) ) ) `  z ) )  =  ( abs `  (
( G `  z
)  x.  -u ( cos `  ( r  x.  z ) ) ) ) )
244240abscld 13279 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  e.  RR )
245244adant423 31607 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  e.  RR )
246231abscld 13279 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  RR )
247246adant423 31607 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  RR )
248 simpllr 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  y  e.  RR )
249239abscld 13279 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  -u ( cos `  (
r  x.  z ) ) )  e.  RR )
250 1red 9628 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  1  e.  RR )
251231absge0d 13287 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  0  <_  ( abs `  ( G `
 z ) ) )
252237absnegd 13292 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  =  ( abs `  ( cos `  ( r  x.  z ) ) ) )
253 abscosbd 31642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  x.  z )  e.  RR  ->  ( abs `  ( cos `  (
r  x.  z ) ) )  <_  1
)
254235, 253syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  ( cos `  ( r  x.  z ) ) )  <_  1 )
255252, 254eqbrtrd 4476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  <_  1 )
256255adantll 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  -u ( cos `  (
r  x.  z ) ) )  <_  1
)
257249, 250, 246, 251, 256lemul2ad 10506 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( ( abs `  ( G `  z ) )  x.  ( abs `  -u ( cos `  ( r  x.  z ) ) ) )  <_  ( ( abs `  ( G `  z ) )  x.  1 ) )
258231, 239absmuld 13297 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  =  ( ( abs `  ( G `
 z ) )  x.  ( abs `  -u ( cos `  ( r  x.  z ) ) ) ) )
259246recnd 9639 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  CC )
260259mulid1d 9630 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( ( abs `  ( G `  z ) )  x.  1 )  =  ( abs `  ( G `
 z ) ) )
261260eqcomd 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  =  ( ( abs `  ( G `  z )
)  x.  1 ) )
262257, 258, 2613brtr4d 4486 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  <_  ( abs `  ( G `  z
) ) )
263262adant423 31607 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  <_  ( abs `  ( G `  z
) ) )
264 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  ->  A. x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
265 nfra1 2838 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ x A. x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y
266195, 265nfan 1929 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )
267199eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  x ) )  =  ( abs `  (
( RR  _D  D
) `  x )
) )
268267adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  -> 
( abs `  ( G `  x )
)  =  ( abs `  ( ( RR  _D  D ) `  x
) ) )
269 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  -> 
( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
270268, 269eqbrtrd 4476 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  -> 
( abs `  ( G `  x )
)  <_  y )
271270ex 434 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( abs `  (
( RR  _D  D
) `  x )
)  <_  y  ->  ( abs `  ( G `
 x ) )  <_  y ) )
272271adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( abs `  (
( RR  _D  D
) `  x )
)  <_  y  ->  ( abs `  ( G `
 x ) )  <_  y ) )
273266, 272ralimdaa 2859 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  ->  ( A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y  ->  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( G `
 x ) )  <_  y ) )
274264, 273mpd 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  ->  A. x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  ( G `  x )
)  <_  y )
275215fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  ( abs `  ( G `  x ) )  =  ( abs `  ( G `  z )
) )
276275breq1d 4466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( abs `  ( G `  x )
)  <_  y  <->  ( abs `  ( G `  z
) )  <_  y
) )
277276cbvralv 3084 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ( abs `  ( G `  x
) )  <_  y  <->  A. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( G `
 z ) )  <_  y )
278274, 277sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  ->  A. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  ( G `  z )
)  <_  y )
279278adant423 31607 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  ->  A. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  ( G `  z )
)  <_  y )
280279r19.21bi 2826 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  <_  y
)
281245, 247, 248, 263, 280letrd 9756 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  <_  y )
282243, 281eqbrtrd 4476 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( RR  _D  D ) `
 x )  x.  -u ( cos `  (
r  x.  x ) ) ) ) `  z ) )  <_ 
y )
283282ralrimiva 2871 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  ->  A. z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( ( RR 
_D  D ) `  x )  x.  -u ( cos `  ( r  x.  x ) ) ) ) `  z ) )  <_  y )
284131ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  e.  CC )
285284adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( ( RR  _D  D ) `  x )  e.  CC )
286 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
r  e.  RR )
28787adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  x  e.  RR )
288286, 287remulcld 9641 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  x
)  e.  RR )
289288recnd 9639 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  x
)  e.  CC )
290289coscld 13878 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( cos `  (
r  x.  x ) )  e.  CC )
291290negcld 9937 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -u ( cos `  (
r  x.  x ) )  e.  CC )
292291adantll 713 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  -u ( cos `  ( r  x.  x
) )  e.  CC )
293285, 292mulcld 9633 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( (
( RR  _D  D
) `  x )  x.  -u ( cos `  (
r  x.  x ) ) )  e.  CC )
294293ralrimiva 2871 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( ( ( RR  _D  D ) `
 x )  x.  -u ( cos `  (
r  x.  x ) ) )  e.  CC )
295 dmmptg 5510 . . . . . . . . . . . . . . . . 17  |-  ( A. x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ( ( ( RR  _D  D
) `  x )  x.  -u ( cos `  (
r  x.  x ) ) )  e.  CC  ->  dom  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( RR  _D  D ) `
 x )  x.  -u ( cos `  (
r  x.  x ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
296294, 295syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  dom  ( x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( ( RR 
_D  D ) `  x )  x.  -u ( cos `  ( r  x.  x ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
297296ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )  ->  dom  ( x  e.  ( ( Q `