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

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

Proof of Theorem fourierdlem73
Dummy variables  m  z  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 753 . . . . . 6  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  i  e.  ( 0..^ M ) )  ->  ph )
2 simpr 461 . . . . . 6  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
3 simpr 461 . . . . . . 7  |-  ( (
ph  /\  e  e.  RR+ )  ->  e  e.  RR+ )
43adantr 465 . . . . . 6  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  i  e.  ( 0..^ M ) )  ->  e  e.  RR+ )
5 fourierdlem73.gcn . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
6 cncff 21265 . . . . . . . . . . . . . . 15  |-  ( ( 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 )
75, 6syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
8 recn 9594 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  RR  ->  y  e.  CC )
98ssriv 3513 . . . . . . . . . . . . . . . . . 18  |-  RR  C_  CC
109a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  CC )
11 fourierdlem73.qf . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
12 fourierdlem73.a . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  e.  RR )
13 fourierdlem73.b . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  RR )
1412, 13iccssred 31426 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( A [,] B
)  C_  RR )
1511, 14fssd 5746 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
1615adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
17 elfzofz 11823 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
1817adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
1916, 18ffvelrnd 6033 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
20 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
2120adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
2216, 21ffvelrnd 6033 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2319, 22iccssred 31426 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  RR )
24 limccl 22147 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) )  C_  CC
25 fourierdlem73.r . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
2624, 25sseldi 3507 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  CC )
2726adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  R  e.  CC )
28 limccl 22147 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  C_  CC
29 fourierdlem73.l . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
3028, 29sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  CC )
3130adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  L  e.  CC )
32 fourierdlem73.f . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F : ( A [,] B ) --> CC )
3332ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  F : ( A [,] B ) --> CC )
3412ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR )
3513ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR )
3619adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
3722adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
38 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
39 eliccre 31427 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
4036, 37, 38, 39syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
4112rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  A  e.  RR* )
4241adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
4313rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  B  e.  RR* )
4443adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
4511adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
4645, 18ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( A [,] B ) )
47 iccgelb 11593 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 i )  e.  ( A [,] B
) )  ->  A  <_  ( Q `  i
) )
4842, 44, 46, 47syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  <_  ( Q `  i )
)
4948adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  ( Q `  i
) )
5036rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
5137rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
52 iccgelb 11593 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
5350, 51, 38, 52syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  x )
5434, 36, 40, 49, 53letrd 9750 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  <_  x )
55 iccleub 11592 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
5650, 51, 38, 55syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  ( Q `  (
i  +  1 ) ) )
5742adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  A  e.  RR* )
5844adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  B  e.  RR* )
5945, 21ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
6059adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  ( A [,] B ) )
61 iccleub 11592 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 ( i  +  1 ) )  e.  ( A [,] B
) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
6257, 58, 60, 61syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  <_  B )
6340, 37, 35, 56, 62letrd 9750 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  <_  B )
6434, 35, 40, 54, 63eliccd 31425 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( A [,] B
) )
6533, 64ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  e.  CC )
6631, 65ifcld 3988 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  e.  CC )
6727, 66ifcld 3988 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
68 fourierdlem73.d . . . . . . . . . . . . . . . . . 18  |-  D  =  ( x  e.  ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) 
|->  if ( x  =  ( Q `  i
) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )
6967, 68fmptd 6056 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  D : ( ( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) --> CC )
70 eqid 2467 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
7170tgioo2 21176 . . . . . . . . . . . . . . . . 17  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
72 iccntr 21194 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
7319, 22, 72syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
7410, 23, 69, 71, 70, 73dvresntr 31569 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
75 ioossicc 11622 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
7675sseli 3505 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
7776adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
78 fvres 5886 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( F `  x ) )
8077, 67syldan 470 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 )
8168fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 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 ) ) ) )
8277, 80, 81syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) ) )
8319adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
8477, 50syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
8577, 51syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
86 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
87 ioogtlb 31415 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8884, 85, 86, 87syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  x )
8983, 88gtned 9731 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  i
) )
9089neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  i ) )
9190iffalsed 3956 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )  =  if ( x  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 x ) ) )
92 elioore 11571 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  x  e.  RR )
9386, 92syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
94 iooltub 31435 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  <  ( Q `  (
i  +  1 ) ) )
9584, 85, 86, 94syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  <  ( Q `  (
i  +  1 ) ) )
9693, 95ltned 9732 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  =/=  ( Q `  (
i  +  1 ) ) )
9796neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  x  =  ( Q `  ( i  +  1 ) ) )
9897iffalsed 3956 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  x ) )  =  ( F `
 x ) )
9982, 91, 983eqtrrd 2513 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  x )  =  ( D `  x ) )
10079, 99eqtr2d 2509 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  x )  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) ) `  x
) )
101100ralrimiva 2881 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( D `  x
)  =  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  (
i  +  1 ) ) ) ) `  x ) )
102 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( D : ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) --> CC  ->  D  Fn  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) ) )
10369, 102syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  D  Fn  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
104 ffn 5737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : ( A [,] B ) --> CC  ->  F  Fn  ( A [,] B ) )
10532, 104syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F  Fn  ( A [,] B ) )
106105adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F  Fn  ( A [,] B ) )
107 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
10842, 44, 45, 107fourierdlem8 31738 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( A [,] B ) )
109 fnssres 5700 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F  Fn  ( A [,] B )  /\  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )  C_  ( A [,] B ) )  -> 
( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  Fn  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )
110106, 108, 109syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  Fn  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
11175a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
112 fvreseq 5990 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
113103, 110, 111, 112syl21anc 1227 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) )
114101, 113mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
115111resabs1d 5309 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
116114, 115eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
117116oveq2d 6311 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( D  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( RR 
_D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) ) )
11832adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : ( A [,] B ) --> CC )
11914adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A [,] B )  C_  RR )
120111, 23sstrd 3519 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
12170, 71dvres 22183 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) ) ) )
12210, 118, 119, 120, 121syl22anc 1229 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) ) )
123 fourierdlem73.g . . . . . . . . . . . . . . . . . . . 20  |-  G  =  ( RR  _D  F
)
124123eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( RR 
_D  F )  =  G
125124a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  F )  =  G )
126 iooretop 21141 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )
127126a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  e.  (
topGen `  ran  (,) )
)
128 retop 21136 . . . . . . . . . . . . . . . . . . . . 21  |-  ( topGen ` 
ran  (,) )  e.  Top
129128a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( topGen `  ran  (,) )  e.  Top )
130 uniretop 21137 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  =  U. ( topGen `  ran  (,) )
131130isopn3 19435 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) ) ) )
132129, 120, 131syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) ) ) )
133127, 132mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
134125, 133reseq12d 5280 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
135 eqidd 2468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
136122, 134, 1353eqtrd 2512 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
13774, 117, 1363eqtrd 2512 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
138137feq1d 5723 . . . . . . . . . . . . . 14  |-  ( (
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 ) )
1397, 138mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
140139feqmptd 5927 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  D )  =  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR  _D  D
) `  x )
) )
141140eqcomd 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  =  ( RR  _D  D
) )
142141, 137eqtrd 2508 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  =  ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
143 ioombl 21843 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  e. 
dom  vol
144143a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  e.  dom  vol )
145 fourierdlem73.qilt . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
14619, 22, 145ltled 9744 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <_  ( Q `  ( i  +  1 ) ) )
147 volioo 31589 . . . . . . . . . . . . 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 )
) )
14819, 22, 146, 147syl3anc 1228 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( ( Q `  ( i  +  1 ) )  -  ( Q `  i ) ) )
14922, 19resubcld 9999 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  ( Q `  i ) )  e.  RR )
150148, 149eqeltrd 2555 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( vol `  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  RR )
151 fourierdlem73.gbd . . . . . . . . . . . . 13  |-  ( ph  ->  E. y  e.  RR  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
152151adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. y  e.  RR  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
153 nfv 1683 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )
154 nfra1 2848 . . . . . . . . . . . . . . . 16  |-  F/ x A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y
155153, 154nfan 1875 . . . . . . . . . . . . . . 15  |-  F/ x
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )
156 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
157 fdm 5741 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC  ->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
1587, 157syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
159158adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) ) )
160159eleq2d 2537 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  -> 
( x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  <-> 
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
161156, 160mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
162 fvres 5886 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( G `  x ) )
163161, 162syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  -> 
( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
)  =  ( G `
 x ) )
164163fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) ) )
165164adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  ( abs `  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
) )  =  ( abs `  ( G `
 x ) ) )
166165adantlr 714 . . . . . . . . . . . . . . . . 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 ) ) )
167 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
)
168 ssdmres 5301 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  G  <->  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
169158, 168sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  G )
170169adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  G )
171170, 86sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  x  e.  dom  G )
172161, 171syldan 470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e. 
dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  G )
173172adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  x  e.  dom  G )
174 rsp 2833 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. x  e.  dom  G ( abs `  ( G `
 x ) )  <_  y  ->  (
x  e.  dom  G  ->  ( abs `  ( G `  x )
)  <_  y )
)
175174imp 429 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y  /\  x  e.  dom  G )  ->  ( abs `  ( G `  x )
)  <_  y )
176167, 173, 175syl2anc 661 . . . . . . . . . . . . . . . . . 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
)
177176adantllr 718 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )  /\  x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )  ->  ( abs `  ( G `  x
) )  <_  y
)
178166, 177eqbrtrd 4473 . . . . . . . . . . . . . . . 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
)
179178ex 434 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  /\  A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y )  ->  ( x  e.  dom  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )  <_  y )
)
180155, 179ralrimi 2867 . . . . . . . . . . . . . 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 )
181180ex 434 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  RR )  ->  ( A. x  e.  dom  G ( abs `  ( G `  x )
)  <_  y  ->  A. x  e.  dom  ( G  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) ( abs `  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  x ) )  <_ 
y ) )
182181reximdva 2942 . . . . . . . . . . . 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 ) )
183152, 182mpd 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 )
184144, 150, 5, 183cnbdibl 31603 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  L^1 )
185142, 184eqeltrd 2555 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR 
_D  D ) `  x ) )  e.  L^1 )
186185adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  e  e.  RR+ )  ->  ( x  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( RR  _D  D ) `
 x ) )  e.  L^1 )
187143a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  e.  dom  vol )
188150adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  ( vol `  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  RR )
189142, 5eqeltrd 2555 . . . . . . . . . . . 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 ) )
190189adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( RR  _D  D
) `  x )
)  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
191 coscn 22707 . . . . . . . . . . . . . 14  |-  cos  e.  ( CC -cn-> CC )
192191a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  cos  e.  ( CC -cn-> CC ) )
193 ioosscn 31414 . . . . . . . . . . . . . . . 16  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
194193a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  CC )
195 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  RR )
1969, 195sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  r  e.  CC )
197 ssid 3528 . . . . . . . . . . . . . . . 16  |-  CC  C_  CC
198197a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  CC  C_  CC )
199194, 196, 198constcncfg 31532 . . . . . . . . . . . . . 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 ) )
200193a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC )
201197a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  CC  C_  CC )
202200, 201idcncfg 31533 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  x )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
203202adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  x )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
204203adantr 465 . . . . . . . . . . . . . 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 ) )
205199, 204mulcncf 21727 . . . . . . . . . . . . 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 ) )
206192, 205cncfmpt1f 21285 . . . . . . . . . . . 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 ) )
207206negcncfg 31542 . . . . . . . . . . 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 ) )
208190, 207mulcncf 21727 . . . . . . . . . 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 ) )
209 nfv 1683 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ph  /\  i  e.  ( 0..^ M ) )
210209, 154nfan 1875 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )
211137fveq1d 5874 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  D ) `  x )  =  ( ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x ) )
212211adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  =  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  x
) )
213162adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  x )  =  ( G `  x ) )
214212, 213eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  x )  =  ( G `  x ) )
215214fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR 
_D  D ) `  x ) )  =  ( abs `  ( G `  x )
) )
216215adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( RR  _D  D ) `  x
) )  =  ( abs `  ( G `
 x ) ) )
217 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
)
218171adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  x  e.  dom  G )
219217, 218, 174sylc 60 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G
( abs `  ( G `  x )
)  <_  y )  /\  x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  x
) )  <_  y
)
220216, 219eqbrtrd 4473 . . . . . . . . . . . . . . . . 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
)
221220ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  dom  G ( abs `  ( G `  x
) )  <_  y
)  ->  ( x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( abs `  ( ( RR  _D  D ) `  x
) )  <_  y
) )
222210, 221ralrimi 2867 . . . . . . . . . . . . . . 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 )
223222ex 434 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A. x  e.  dom  G ( abs `  ( G `  x
) )  <_  y  ->  A. x  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
)
224223reximdv 2941 . . . . . . . . . . . . 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 ) )
225152, 224mpd 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 )
226225adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  ->  E. y  e.  RR  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
227 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) ) ) ) )
228 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  (
( RR  _D  D
) `  x )  =  ( ( RR 
_D  D ) `  z ) )
229 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ x
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( RR  _D  D ) `  z
)  =  ( G `
 z ) )
230 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  z  ->  (
x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
231230anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) ) ) ) )
232 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  z  ->  ( G `  x )  =  ( G `  z ) )
233228, 232eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
( ( RR  _D  D ) `  x
)  =  ( G `
 x )  <->  ( ( RR  _D  D ) `  z )  =  ( G `  z ) ) )
234231, 233imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) )
235229, 234, 214chvar 1982 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( RR  _D  D
) `  z )  =  ( G `  z ) )
236228, 235sylan9eqr 2530 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  x  =  z )  ->  ( ( RR  _D  D ) `  x
)  =  ( G `
 z ) )
237 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
r  x.  x )  =  ( r  x.  z ) )
238237fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  ( cos `  ( r  x.  x ) )  =  ( cos `  (
r  x.  z ) ) )
239238negeqd 9826 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  -u ( cos `  ( r  x.  x ) )  = 
-u ( cos `  (
r  x.  z ) ) )
240239adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  x  =  z )  -> 
-u ( cos `  (
r  x.  x ) )  =  -u ( cos `  ( r  x.  z ) ) )
241236, 240oveq12d 6313 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) ) ) )
242241adantllr 718 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 ) ) ) )
243 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
244 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
245 fvres 5886 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
246244, 245syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  =  ( G `  z ) )
247246eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( G `  z )  =  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  z
) )
2487ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  z )  e.  CC )
249247, 248eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
250249adantlr 714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( G `  z )  e.  CC )
251 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
r  e.  RR )
252 elioore 11571 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  z  e.  RR )
253252adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
z  e.  RR )
254251, 253remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  RR )
255254recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( r  x.  z
)  e.  CC )
256255coscld 13744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( cos `  (
r  x.  z ) )  e.  CC )
257256negcld 9929 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -u ( cos `  (
r  x.  z ) )  e.  CC )
258257adantll 713 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  -u ( cos `  ( r  x.  z
) )  e.  CC )
259250, 258mulcld 9628 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
260227, 242, 243, 259fvmptd 5962 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) `  z )  =  ( ( G `
 z )  x.  -u ( cos `  (
r  x.  z ) ) ) )
261260fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) ) ) ) )
262261adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  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 ) ) ) ) )
263262adantlr 714 . . . . . . . . . . . . . . . 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 ) ) ) ) )
264259abscld 13247 . . . . . . . . . . . . . . . . . . 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 ) ) ) )  e.  RR )
265264adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  e.  RR )
266265adantlr 714 . . . . . . . . . . . . . . . . 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 )
267250abscld 13247 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  RR )
268267adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  RR )
269268adantlr 714 . . . . . . . . . . . . . . . . 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 )
270 simpllr 758 . . . . . . . . . . . . . . . . 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 )
271258abscld 13247 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  -u ( cos `  (
r  x.  z ) ) )  e.  RR )
272 1re 9607 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR
273272a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  1  e.  RR )
274250absge0d 13255 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  0  <_  ( abs `  ( G `
 z ) ) )
275256absnegd 13260 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  =  ( abs `  ( cos `  ( r  x.  z ) ) ) )
276 abscosbd 31360 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( r  x.  z )  e.  RR  ->  ( abs `  ( cos `  (
r  x.  z ) ) )  <_  1
)
277254, 276syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  ( cos `  ( r  x.  z ) ) )  <_  1 )
278275, 277eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( r  e.  RR  /\  z  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( abs `  -u ( cos `  ( r  x.  z ) ) )  <_  1 )
279278adantll 713 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  -u ( cos `  (
r  x.  z ) ) )  <_  1
)
280271, 273, 267, 274, 279lemul2ad 10498 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
281250, 258absmuld 13265 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) ) ) ) )
2829, 267sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  e.  CC )
283282mulid1d 9625 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( ( abs `  ( G `  z ) )  x.  1 )  =  ( abs `  ( G `
 z ) ) )
284283eqcomd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  z  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  z
) )  =  ( ( abs `  ( G `  z )
)  x.  1 ) )
285281, 284breq12d 4466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
)  <->  ( ( abs `  ( G `  z
) )  x.  ( abs `  -u ( cos `  (
r  x.  z ) ) ) )  <_ 
( ( abs `  ( G `  z )
)  x.  1 ) ) )
286280, 285mpbird 232 . . . . . . . . . . . . . . . . . . 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
) ) )
287286adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  RR )  /\  y  e.  RR )  /\  z  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( abs `  ( ( G `  z )  x.  -u ( cos `  ( r  x.  z ) ) ) )  <_  ( abs `  ( G `  z
) ) )
288287adantlr 714 . . . . . . . . . . . . . . . . 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
) ) )
289 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 )
290 nfra1 2848 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ x A. x  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  D
) `  x )
)  <_  y
291209, 290nfan 1875 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ x
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )
292215eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( abs `  ( G `  x ) )  =  ( abs `  (
( RR  _D  D
) `  x )
) )
293292adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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
) ) )
294 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  -> 
( abs `  (
( RR  _D  D
) `  x )
)  <_  y )
295293, 294eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  ( abs `  ( ( RR  _D  D ) `
 x ) )  <_  y )  -> 
( abs `  ( G `  x )
)  <_  y )
296295ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( abs `  (
( RR  _D  D
) `  x )
)  <_  y  ->  ( abs `  ( G `
 x ) )  <_  y ) )
297296adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) )
298291, 297ralimdaa 2869 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) )
299289, 298mpd 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 )
300232fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  ( abs `  ( G `  x ) )  =  ( abs `  ( G `  z )
) )
301300breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  (
( abs `  ( G `  x )
)  <_  y  <->  ( abs `  ( G `  z
) )  <_  y
) )
302301cbvralv 3093 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ( abs `  ( G `  x
) )  <_  y  <->  A. z  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( abs `  ( G `
 z ) )  <_  y )
303299, 302sylib 196 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  A. x  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 )