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

Theorem fourierdlem73 37863
Description: A version of the Riemann 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 21912 . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
4 ax-resscn 9597 . . . . . . . . . . . . . . . . 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 37433 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A [,] B
)  C_  RR )
106, 9fssd 5752 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
1110adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
12 elfzofz 11936 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
1312adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
1411, 13ffvelrnd 6035 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
15 fzofzp1 12008 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
1615adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
1711, 16ffvelrnd 6035 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
1814, 17iccssred 37433 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  RR )
19 limccl 22817 . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  CC )
2221adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  R  e.  CC )
23 limccl 22817 . . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  CC )
2625adantr 466 . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : ( A [,] B ) --> CC )
297ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR )
308ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR )
3114adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
3217adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
33 simpr 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
34 eliccre 37434 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
3531, 32, 33, 34syl3anc 1264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
367rexrd 9691 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  e.  RR* )
3736adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
388rexrd 9691 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  RR* )
3938adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
406adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
4140, 13ffvelrnd 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( A [,] B ) )
42 iccgelb 11692 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 i )  e.  ( A [,] B
) )  ->  A  <_  ( Q `  i
) )
4337, 39, 41, 42syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  <_  ( Q `  i )
)
4443adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  ( Q `  i
) )
4531rexrd 9691 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
4632rexrd 9691 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
47 iccgelb 11692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
4845, 46, 33, 47syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
4929, 31, 35, 44, 48letrd 9793 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  x )
50 iccleub 11691 . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
5236ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
5338ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
5440, 16ffvelrnd 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
5554adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
56 iccleub 11691 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 ( i  +  1 ) )  e.  ( A [,] B
) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
5752, 53, 55, 56syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
5835, 32, 30, 51, 57letrd 9793 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  B )
5929, 30, 35, 49, 58eliccd 37432 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( A [,] B
) )
6028, 59ffvelrnd 6035 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
6126, 60ifcld 3952 . . . . . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . . . . . . 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 6058 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  D : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
65 eqid 2422 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6665tgioo2 21808 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
67 iccntr 21826 . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . 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 37608 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
70 ioossicc 11721 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
7170sseli 3460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
7271adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
73 fvres 5892 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
7472, 73syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
7572, 62syldan 472 . . . . . . . . . . . . . . . . . . . . . 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 5970 . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
7972, 45syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
8072, 46syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
81 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
82 ioogtlb 37423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8379, 80, 81, 82syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8478, 83gtned 9771 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  i
) )
8584neneqd 2625 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  i ) )
8685iffalsed 3920 . . . . . . . . . . . . . . . . . . . . 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 11667 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  RR )
8887adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
89 iooltub 37441 . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  <  ( Q `  (
i  +  1 ) ) )
9188, 90ltned 9772 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  (
i  +  1 ) ) )
9291neneqd 2625 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  ( i  +  1 ) ) )
9392iffalsed 3920 . . . . . . . . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  =  ( D `  x ) )
9574, 94eqtr2d 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  x )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  x
) )
9695ralrimiva 2839 . . . . . . . . . . . . . . . . . 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 5743 . . . . . . . . . . . . . . . . . . . 20  |-  ( D : ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) --> CC  ->  D  Fn  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) )
9864, 97syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  D  Fn  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
99 ffn 5743 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : ( A [,] B ) --> CC  ->  F  Fn  ( A [,] B ) )
10027, 99syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F  Fn  ( A [,] B ) )
101100adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F  Fn  ( A [,] B ) )
102 simpr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
10337, 39, 40, 102fourierdlem8 37797 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( A [,] B ) )
104 fnssres 5704 . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . 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 5996 . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
110106resabs1d 5150 . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
112111oveq2d 6318 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( RR 
_D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
11327adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : ( A [,] B ) --> CC )
1149adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A [,] B )  C_  RR )
115106, 18sstrd 3474 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
11665, 66dvres 22853 . . . . . . . . . . . . . . . . 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 1265 . . . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
_D  F )  =  G
120119a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  F )  =  G )
121 iooretop 21773 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )
122 retop 21769 . . . . . . . . . . . . . . . . . . 19  |-  ( topGen ` 
ran  (,) )  e.  Top
123 uniretop 21770 . . . . . . . . . . . . . . . . . . . 20  |-  RR  =  U. ( topGen `  ran  (,) )
124123isopn3 20069 . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
127120, 126reseq12d 5122 . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
12969, 112, 1283eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
130129feq1d 5729 . . . . . . . . . . . . 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 235 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
132131feqmptd 5931 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR  _D  D
) `  x )
) )
133132, 129eqtr3d 2465 . . . . . . . . . 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 22505 . . . . . . . . . . . 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 9784 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <_  ( Q `  ( i  +  1 ) ) )
138 volioo 37645 . . . . . . . . . . . . 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 1264 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( Q `  ( i  +  1 ) )  -  ( Q `  i ) ) )
14017, 14resubcld 10048 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  ( Q `  i ) )  e.  RR )
141139, 140eqeltrd 2510 . . . . . . . . . . 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 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. y  e.  RR  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
144 nfv 1751 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )
145 nfra1 2806 . . . . . . . . . . . . . . . 16  |-  F/ x A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y
146144, 145nfan 1984 . . . . . . . . . . . . . . 15  |-  F/ x
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )
147 simpr 462 . . . . . . . . . . . . . . . . . . . . 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 5747 . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
150149adantr 466 . . . . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
152 fvres 5892 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( G `  x ) )
153151, 152syl 17 . . . . . . . . . . . . . . . . . . 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 5882 . . . . . . . . . . . . . . . . . 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 37228 . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . 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 5142 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  G  <->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
158149, 157sylibr 215 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  G )
159158sselda 3464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  dom  G )
160151, 159syldan 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  G )
161160adantlr 719 . . . . . . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . . . . . 19  |-  ( A. x  e.  dom  G ( abs `  ( G `
 x ) )  <_  y  ->  (
x  e.  dom  G  ->  ( abs `  ( G `  x )
)  <_  y )
)
163156, 161, 162sylc 62 . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . 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 4441 . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . 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 2825 . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . 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 2900 . . . . . . . . . . . 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 37659 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  L^1 )
172133, 171eqeltrd 2510 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  e.  L^1 )
173172adantr 466 . . . . . . . 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 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  ( vol `  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  RR )
176133, 1eqeltrd 2510 . . . . . . . . . . . 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 466 . . . . . . . . . . 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 23387 . . . . . . . . . . . . . 14  |-  cos  e.  ( CC -cn-> CC )
179178a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  cos  e.  ( CC -cn-> CC ) )
180 ioosscn 37422 . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  RR )
183182recnd 9670 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  CC )
184 ssid 3483 . . . . . . . . . . . . . . . 16  |-  CC  C_  CC
185184a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  CC  C_  CC )
186181, 183, 185constcncfg 37568 . . . . . . . . . . . . . 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 37569 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  x )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
190189ad2antrr 730 . . . . . . . . . . . . . 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 22385 . . . . . . . . . . . . 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 21932 . . . . . . . . . . . 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 37578 . . . . . . . . . . 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 22385 . . . . . . . . . 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 1751 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ph  /\  i  e.  ( 0..^ M ) )
196195, 145nfan 1984 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
197129fveq1d 5880 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  D ) `  x )  =  ( ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )
198197, 152sylan9eq 2483 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  =  ( G `  x ) )
199198fveq2d 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR 
_D  D ) `  x ) )  =  ( abs `  ( G `  x )
) )
200199adantlr 719 . . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . . . 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 62 . . . . . . . . . . . . . . . . . 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 4441 . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . 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 2825 . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . 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 2899 . . . . . . . . . . . . 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 466 . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( RR  _D  D
) `  x )  =  ( ( RR 
_D  D ) `  z ) )
213 eleq1 2494 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
214213anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  ( G `  x )  =  ( G `  z ) )
216212, 215eqeq12d 2444 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( RR  _D  D ) `  x
)  =  ( G `
 x )  <->  ( ( RR  _D  D ) `  z )  =  ( G `  z ) ) )
217214, 216imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . 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 2068 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  z )  =  ( G `  z ) )
219212, 218sylan9eqr 2485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  x  =  z )  ->  ( ( RR  _D  D ) `  x
)  =  ( G `
 z ) )
220 oveq2 6310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
r  x.  x )  =  ( r  x.  z ) )
221220fveq2d 5882 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( cos `  ( r  x.  x ) )  =  ( cos `  (
r  x.  z ) ) )
222221negeqd 9870 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  -u ( cos `  ( r  x.  x ) )  = 
-u ( cos `  (
r  x.  z ) ) )
223222adantl 467 . . . . . . . . . . . . . . . . . . . . 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 6320 . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . 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 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
228227adantl 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
2293ffvelrnda 6034 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  e.  CC )
230228, 229eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
231230adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
232 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
r  e.  RR )
233 elioore 11667 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  RR )
234233adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
z  e.  RR )
235232, 234remulcld 9672 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  RR )
236235recnd 9670 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  CC )
237236coscld 14173 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( cos `  (
r  x.  z ) )  e.  CC )
238237negcld 9974 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -u ( cos `  (
r  x.  z ) )  e.  CC )
239238adantll 718 . . . . . . . . . . . . . . . . . . . 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 9664 . . . . . . . . . . . . . . . . . . 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 5967 . . . . . . . . . . . . . . . . . 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 5882 . . . . . . . . . . . . . . . . 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 37228 . . . . . . . . . . . . . . . 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 13486 . . . . . . . . . . . . . . . . . 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 37228 . . . . . . . . . . . . . . . . 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 13486 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  RR )
247246adant423 37228 . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . 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 13486 . . . . . . . . . . . . . . . . . . . 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 9659 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  1  e.  RR )
251231absge0d 13494 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  0  <_  ( abs `  ( G `
 z ) ) )
252237absnegd 13499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  =  ( abs `  ( cos `  ( r  x.  z ) ) ) )
253 abscosbd 37330 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  x.  z )  e.  RR  ->  ( abs `  ( cos `  (
r  x.  z ) ) )  <_  1
)
254235, 253syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  ( cos `  ( r  x.  z ) ) )  <_  1 )
255252, 254eqbrtrd 4441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  <_  1 )
256255adantll 718 . . . . . . . . . . . . . . . . . . . 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 10548 . . . . . . . . . . . . . . . . . . 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 13504 . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  CC )
260259mulid1d 9661 . . . . . . . . . . . . . . . . . . . 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 2430 . . . . . . . . . . . . . . . . . . 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 4451 . . . . . . . . . . . . . . . . . 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 37228 . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . 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 2806 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ x A. x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y
266195, 265nfan 1984 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )
267199eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  x ) )  =  ( abs `  (
( RR  _D  D
) `  x )
) )
268267adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . . . . 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 4441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  -> 
( abs `  ( G `  x )
)  <_  y )
271270ex 435 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( abs `  (
( RR  _D  D
) `  x )
)  <_  y  ->  ( abs `  ( G `
 x ) )  <_  y ) )
272271adantlr 719 . . . . . . . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . . . . . . 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 5882 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  ( abs `  ( G `  x ) )  =  ( abs `  ( G `  z )
) )
276275breq1d 4430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( abs `  ( G `  x )
)  <_  y  <->  ( abs `  ( G `  z
) )  <_  y
) )
277276cbvralv 3055 . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . 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 37228 . . . . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . . . . 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 9793 . . . . . . . . . . . . . . . 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 4441 . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  e.  CC )
285284adantlr 719 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( ( RR  _D  D ) `  x )  e.  CC )
286 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
r  e.  RR )
28787adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  x  e.  RR )
288286, 287remulcld 9672 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  x
)  e.  RR )
289288recnd 9670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  x
)  e.  CC )
290289coscld 14173 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( cos `  (
r  x.  x ) )  e.  CC )
291290negcld 9974 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -u ( cos `  (
r  x.  x ) )  e.  CC )
292291adantll 718 . . . . . . . . . . . . . . . . . . 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 9664 . . . . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . . . . 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 5348 . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . 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 `  i