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

Theorem fourierdlem73 37330
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 21689 . . . . . . . . . . . . . 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 9579 . . . . . . . . . . . . . . . . 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 36907 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A [,] B
)  C_  RR )
106, 9fssd 5723 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
1110adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
12 elfzofz 11874 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
1312adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
1411, 13ffvelrnd 6010 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
15 fzofzp1 11946 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
1615adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
1711, 16ffvelrnd 6010 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
1814, 17iccssred 36907 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  RR )
19 limccl 22571 . . . . . . . . . . . . . . . . . . . 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 3440 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  CC )
2221adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  R  e.  CC )
23 limccl 22571 . . . . . . . . . . . . . . . . . . . . 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 3440 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  CC )
2625adantr 463 . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : ( A [,] B ) --> CC )
297ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR )
308ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR )
3114adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
3217adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
33 simpr 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
34 eliccre 36908 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
3531, 32, 33, 34syl3anc 1230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
367rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  e.  RR* )
3736adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
388rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  RR* )
3938adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
406adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
4140, 13ffvelrnd 6010 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( A [,] B ) )
42 iccgelb 11635 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 i )  e.  ( A [,] B
) )  ->  A  <_  ( Q `  i
) )
4337, 39, 41, 42syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  <_  ( Q `  i )
)
4443adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  ( Q `  i
) )
4531rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
4632rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
47 iccgelb 11635 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
4845, 46, 33, 47syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
4929, 31, 35, 44, 48letrd 9773 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  x )
50 iccleub 11634 . . . . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
5236ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
5338ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
5440, 16ffvelrnd 6010 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
5554adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
56 iccleub 11634 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 ( i  +  1 ) )  e.  ( A [,] B
) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
5752, 53, 55, 56syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
5835, 32, 30, 51, 57letrd 9773 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  B )
5929, 30, 35, 49, 58eliccd 36906 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( A [,] B
) )
6028, 59ffvelrnd 6010 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
6126, 60ifcld 3928 . . . . . . . . . . . . . . . . . 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 3928 . . . . . . . . . . . . . . . . 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 6033 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  D : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
65 eqid 2402 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6665tgioo2 21600 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
67 iccntr 21618 . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . 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 37081 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
70 ioossicc 11664 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
7170sseli 3438 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
7271adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
73 fvres 5863 . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . 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 5941 . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
7972, 45syldan 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
8072, 46syldan 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
81 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
82 ioogtlb 36897 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8379, 80, 81, 82syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8478, 83gtned 9752 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  i
) )
8584neneqd 2605 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  i ) )
8685iffalsed 3896 . . . . . . . . . . . . . . . . . . . . 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 11612 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  RR )
8887adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
89 iooltub 36916 . . . . . . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  <  ( Q `  (
i  +  1 ) ) )
9188, 90ltned 9753 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  (
i  +  1 ) ) )
9291neneqd 2605 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  ( i  +  1 ) ) )
9392iffalsed 3896 . . . . . . . . . . . . . . . . . . . . 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 2448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  =  ( D `  x ) )
9574, 94eqtr2d 2444 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  x )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  x
) )
9695ralrimiva 2818 . . . . . . . . . . . . . . . . . 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 5714 . . . . . . . . . . . . . . . . . . . 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 5714 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : ( A [,] B ) --> CC  ->  F  Fn  ( A [,] B ) )
10027, 99syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F  Fn  ( A [,] B ) )
101100adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F  Fn  ( A [,] B ) )
102 simpr 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
10337, 39, 40, 102fourierdlem8 37265 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( A [,] B ) )
104 fnssres 5675 . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . 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 5967 . . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . . 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 5123 . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
112111oveq2d 6294 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( RR 
_D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
11327adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : ( A [,] B ) --> CC )
1149adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A [,] B )  C_  RR )
115106, 18sstrd 3452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
11665, 66dvres 22607 . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . 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 2415 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
_D  F )  =  G
120119a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  F )  =  G )
121 iooretop 21565 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )
122 retop 21560 . . . . . . . . . . . . . . . . . . 19  |-  ( topGen ` 
ran  (,) )  e.  Top
123 uniretop 21561 . . . . . . . . . . . . . . . . . . . 20  |-  RR  =  U. ( topGen `  ran  (,) )
124123isopn3 19860 . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . 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 5095 . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
12969, 112, 1283eqtrd 2447 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
130129feq1d 5700 . . . . . . . . . . . . 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 5902 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR  _D  D
) `  x )
) )
133132, 129eqtr3d 2445 . . . . . . . . . 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 22267 . . . . . . . . . . . 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 9765 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <_  ( Q `  ( i  +  1 ) ) )
138 volioo 37115 . . . . . . . . . . . . 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 1230 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( Q `  ( i  +  1 ) )  -  ( Q `  i ) ) )
14017, 14resubcld 10028 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  ( Q `  i ) )  e.  RR )
141139, 140eqeltrd 2490 . . . . . . . . . . 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 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. y  e.  RR  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
144 nfv 1728 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )
145 nfra1 2785 . . . . . . . . . . . . . . . 16  |-  F/ x A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y
146144, 145nfan 1956 . . . . . . . . . . . . . . 15  |-  F/ x
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )
147 simpr 459 . . . . . . . . . . . . . . . . . . . . 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 5718 . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
152 fvres 5863 . . . . . . . . . . . . . . . . . . . 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 5853 . . . . . . . . . . . . . . . . . 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 36802 . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . . . 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 5115 . . . . . . . . . . . . . . . . . . . . . . 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 3442 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  dom  G )
160151, 159syldan 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  G )
161160adantlr 713 . . . . . . . . . . . . . . . . . . 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 2770 . . . . . . . . . . . . . . . . . . 19  |-  ( A. x  e.  dom  G ( abs `  ( G `
 x ) )  <_  y  ->  (
x  e.  dom  G  ->  ( abs `  ( G `  x )
)  <_  y )
)
163156, 161, 162sylc 59 . . . . . . . . . . . . . . . . . 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 717 . . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . 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 2804 . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . 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 2879 . . . . . . . . . . . 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 37129 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  L^1 )
172133, 171eqeltrd 2490 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  e.  L^1 )
173172adantr 463 . . . . . . . 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 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  ( vol `  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  RR )
176133, 1eqeltrd 2490 . . . . . . . . . . . 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 463 . . . . . . . . . . 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 23132 . . . . . . . . . . . . . 14  |-  cos  e.  ( CC -cn-> CC )
179178a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  cos  e.  ( CC -cn-> CC ) )
180 ioosscn 36896 . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  RR )
183182recnd 9652 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  CC )
184 ssid 3461 . . . . . . . . . . . . . . . 16  |-  CC  C_  CC
185184a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  CC  C_  CC )
186181, 183, 185constcncfg 37041 . . . . . . . . . . . . . 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 37042 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  x )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
190189ad2antrr 724 . . . . . . . . . . . . . 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 22151 . . . . . . . . . . . . 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 21709 . . . . . . . . . . . 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 37051 . . . . . . . . . . 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 22151 . . . . . . . . . 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 1728 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ph  /\  i  e.  ( 0..^ M ) )
196195, 145nfan 1956 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
197129fveq1d 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  D ) `  x )  =  ( ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )
198197, 152sylan9eq 2463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  =  ( G `  x ) )
199198fveq2d 5853 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR 
_D  D ) `  x ) )  =  ( abs `  ( G `  x )
) )
200199adantlr 713 . . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . 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 59 . . . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . 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 2804 . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . 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 2878 . . . . . . . . . . . . 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 463 . . . . . . . . . . 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 2403 . . . . . . . . . . . . . . . . . . 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 5849 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( RR  _D  D
) `  x )  =  ( ( RR 
_D  D ) `  z ) )
213 eleq1 2474 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
214213anbi2d 702 . . . . . . . . . . . . . . . . . . . . . . . 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 5849 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  ( G `  x )  =  ( G `  z ) )
216212, 215eqeq12d 2424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( RR  _D  D ) `  x
)  =  ( G `
 x )  <->  ( ( RR  _D  D ) `  z )  =  ( G `  z ) ) )
217214, 216imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . 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 2041 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  z )  =  ( G `  z ) )
219212, 218sylan9eqr 2465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  x  =  z )  ->  ( ( RR  _D  D ) `  x
)  =  ( G `
 z ) )
220 oveq2 6286 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
r  x.  x )  =  ( r  x.  z ) )
221220fveq2d 5853 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( cos `  ( r  x.  x ) )  =  ( cos `  (
r  x.  z ) ) )
222221negeqd 9850 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  -u ( cos `  ( r  x.  x ) )  = 
-u ( cos `  (
r  x.  z ) ) )
223222adantl 464 . . . . . . . . . . . . . . . . . . . . 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 6296 . . . . . . . . . . . . . . . . . . . 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 717 . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . 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 5863 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
228227adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
2293ffvelrnda 6009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  e.  CC )
230228, 229eqeltrrd 2491 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
231230adantlr 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
232 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
r  e.  RR )
233 elioore 11612 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  RR )
234233adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
z  e.  RR )
235232, 234remulcld 9654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  RR )
236235recnd 9652 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  CC )
237236coscld 14075 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( cos `  (
r  x.  z ) )  e.  CC )
238237negcld 9954 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -u ( cos `  (
r  x.  z ) )  e.  CC )
239238adantll 712 . . . . . . . . . . . . . . . . . . . 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 9646 . . . . . . . . . . . . . . . . . . 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 5938 . . . . . . . . . . . . . . . . . 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 5853 . . . . . . . . . . . . . . . . 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 36802 . . . . . . . . . . . . . . . 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 13416 . . . . . . . . . . . . . . . . . 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 36802 . . . . . . . . . . . . . . . . 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 13416 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  RR )
247246adant423 36802 . . . . . . . . . . . . . . . . 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 761 . . . . . . . . . . . . . . . . 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 13416 . . . . . . . . . . . . . . . . . . . 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 9641 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  1  e.  RR )
251231absge0d 13424 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  0  <_  ( abs `  ( G `
 z ) ) )
252237absnegd 13429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  =  ( abs `  ( cos `  ( r  x.  z ) ) ) )
253 abscosbd 36834 . . . . . . . . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  <_  1 )
256255adantll 712 . . . . . . . . . . . . . . . . . . . 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 10526 . . . . . . . . . . . . . . . . . . 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 13434 . . . . . . . . . . . . . . . . . . 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 9652 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  CC )
260259mulid1d 9643 . . . . . . . . . . . . . . . . . . . 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 2410 . . . . . . . . . . . . . . . . . . 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 4425 . . . . . . . . . . . . . . . . . 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 36802 . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . 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 2785 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ x A. x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y
266195, 265nfan 1956 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )
267199eqcomd 2410 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  x ) )  =  ( abs `  (
( RR  _D  D
) `  x )
) )
268267adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  -> 
( abs `  ( G `  x )
)  <_  y )
271270ex 432 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( abs `  (
( RR  _D  D
) `  x )
)  <_  y  ->  ( abs `  ( G `
 x ) )  <_  y ) )
272271adantlr 713 . . . . . . . . . . . . . . . . . . . . . 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 2806 . . . . . . . . . . . . . . . . . . . . 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 5853 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  ( abs `  ( G `  x ) )  =  ( abs `  ( G `  z )
) )
276275breq1d 4405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( abs `  ( G `  x )
)  <_  y  <->  ( abs `  ( G `  z
) )  <_  y
) )
277276cbvralv 3034 . . . . . . . . . . . . . . . . . . . 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 36802 . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . 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 9773 . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . 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 2818 . . . . . . . . . . . . . 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 6009 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  e.  CC )
285284adantlr 713 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( ( RR  _D  D ) `  x )  e.  CC )
286 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
r  e.  RR )
28787adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  x  e.  RR )
288286, 287remulcld 9654 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  x
)  e.  RR )
289288recnd 9652 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  x
)  e.  CC )
290289coscld 14075 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( cos `  (
r  x.  x ) )  e.  CC )
291290negcld 9954 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( r  e.  RR  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -u ( cos `  (
r  x.  x ) )  e.  CC )
292291adantll 712 . . . . . . . . . . . . . . . . . . 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 9646 . . . . . . . . . . . . . . . . . 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 2818 . . . . . . . . . . . . . . . . 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 5320 . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . 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 `