Metamath Proof Explorer

Theorem fourierdlem73

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)

Ref Expression
Hypotheses 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 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem73.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( 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 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 )

Proof

Step Hyp Ref Expression
1 fourierdlem73.a 
 |-  ( ph -> A e. RR )
2 fourierdlem73.b 
 |-  ( ph -> B e. RR )
3 fourierdlem73.f 
 |-  ( ph -> F : ( A [,] B ) --> CC )
4 fourierdlem73.m 
 |-  ( ph -> M e. NN )
5 fourierdlem73.qf 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
6 fourierdlem73.q0 
 |-  ( ph -> ( Q ` 0 ) = A )
7 fourierdlem73.qm 
 |-  ( ph -> ( Q ` M ) = B )
8 fourierdlem73.qilt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
9 fourierdlem73.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
10 fourierdlem73.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
11 fourierdlem73.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
12 fourierdlem73.g 
 |-  G = ( RR _D F )
13 fourierdlem73.gcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
14 fourierdlem73.gbd 
 |-  ( ph -> E. y e. RR A. x e. dom G ( abs ` ( G ` x ) ) <_ y )
15 fourierdlem73.s 
 |-  S = ( r e. RR+ |-> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
16 fourierdlem73.d 
 |-  D = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
17 cncff 
 |-  ( ( 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 )
18 13 17 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
19 ax-resscn 
 |-  RR C_ CC
20 19 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> RR C_ CC )
21 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
22 5 21 fssd 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
23 22 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
24 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
25 24 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
26 23 25 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
27 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
28 27 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
29 23 28 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
30 26 29 iccssred 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ RR )
31 limccl 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) C_ CC
32 31 11 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. CC )
33 32 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> R e. CC )
34 limccl 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) C_ CC
35 34 10 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. CC )
36 35 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> L e. CC )
37 3 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : ( A [,] B ) --> CC )
38 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> A e. RR )
39 2 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> B e. RR )
40 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
41 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
42 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
43 eliccre 
 |-  ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
44 40 41 42 43 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
45 1 rexrd 
 |-  ( ph -> A e. RR* )
46 45 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR* )
47 2 rexrd 
 |-  ( ph -> B e. RR* )
48 47 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> B e. RR* )
49 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
50 49 25 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( A [,] B ) )
51 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` i ) e. ( A [,] B ) ) -> A <_ ( Q ` i ) )
52 46 48 50 51 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A <_ ( Q ` i ) )
53 52 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> A <_ ( Q ` i ) )
54 40 rexrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
55 41 rexrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
56 iccgelb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ x )
57 54 55 42 56 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ x )
58 38 40 44 53 57 letrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> A <_ x )
59 iccleub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
60 54 55 42 59 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
61 45 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
62 47 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
63 49 28 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( A [,] B ) )
64 63 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. ( A [,] B ) )
65 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` ( i + 1 ) ) e. ( A [,] B ) ) -> ( Q ` ( i + 1 ) ) <_ B )
66 61 62 64 65 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) <_ B )
67 44 41 39 60 66 letrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ B )
68 38 39 44 58 67 eliccd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
69 37 68 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
70 36 69 ifcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) e. CC )
71 33 70 ifcld 
 |-  ( ( ( 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 )
72 71 16 fmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> D : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
73 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
74 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
75 iccntr 
 |-  ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
76 26 29 75 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
77 20 30 72 73 74 76 dvresntr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D D ) = ( RR _D ( D |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
78 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
79 78 sseli 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
80 79 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
81 fvres 
 |-  ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
82 80 81 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
83 80 71 syldan 
 |-  ( ( ( 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 )
84 16 fvmpt2 
 |-  ( ( 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 ) ) ) )
85 80 83 84 syl2anc 
 |-  ( ( ( 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 ) ) ) )
86 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
87 80 54 syldan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
88 80 55 syldan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
89 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
90 ioogtlb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < x )
91 87 88 89 90 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < x )
92 86 91 gtned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x =/= ( Q ` i ) )
93 92 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. x = ( Q ` i ) )
94 93 iffalsed 
 |-  ( ( ( 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 ) ) )
95 elioore 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> x e. RR )
96 95 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
97 iooltub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x < ( Q ` ( i + 1 ) ) )
98 87 88 89 97 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x < ( Q ` ( i + 1 ) ) )
99 96 98 ltned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x =/= ( Q ` ( i + 1 ) ) )
100 99 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. x = ( Q ` ( i + 1 ) ) )
101 100 iffalsed 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
102 85 94 101 3eqtrrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) = ( D ` x ) )
103 82 102 eqtr2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( D ` x ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` x ) )
104 103 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( D ` x ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` x ) )
105 ffn 
 |-  ( D : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC -> D Fn ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
106 72 105 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> D Fn ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
107 ffn 
 |-  ( F : ( A [,] B ) --> CC -> F Fn ( A [,] B ) )
108 3 107 syl 
 |-  ( ph -> F Fn ( A [,] B ) )
109 108 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F Fn ( A [,] B ) )
110 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
111 46 48 49 110 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
112 fnssres 
 |-  ( ( F Fn ( A [,] B ) /\ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) ) -> ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) Fn ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
113 109 111 112 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) Fn ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
114 78 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
115 fvreseq 
 |-  ( ( ( 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 ) ) )
116 106 113 114 115 syl21anc 
 |-  ( ( 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 ) ) )
117 104 116 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
118 114 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
119 117 118 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
120 119 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D ( D |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
121 3 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : ( A [,] B ) --> CC )
122 21 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A [,] B ) C_ RR )
123 114 30 sstrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
124 74 73 dvres 
 |-  ( ( ( 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 ) ) ) ) ) )
125 20 121 122 123 124 syl22anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
126 12 eqcomi 
 |-  ( RR _D F ) = G
127 126 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D F ) = G )
128 iooretop 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. ( topGen ` ran (,) )
129 retop 
 |-  ( topGen ` ran (,) ) e. Top
130 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
131 130 isopn3 
 |-  ( ( ( 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 ) ) ) ) )
132 129 123 131 sylancr 
 |-  ( ( 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 ) ) ) ) )
133 128 132 mpbii 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
134 127 133 reseq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
135 125 134 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
136 77 120 135 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D D ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
137 136 feq1d 
 |-  ( ( 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 ) )
138 18 137 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D D ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
139 138 feqmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D D ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( RR _D D ) ` x ) ) )
140 139 136 eqtr3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( RR _D D ) ` x ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
141 ioombl 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. dom vol
142 141 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. dom vol )
143 26 29 8 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) <_ ( Q ` ( i + 1 ) ) )
144 volioo 
 |-  ( ( ( 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 ) ) )
145 26 29 143 144 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( vol ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` ( i + 1 ) ) - ( Q ` i ) ) )
146 29 26 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - ( Q ` i ) ) e. RR )
147 145 146 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( vol ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. RR )
148 14 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. y e. RR A. x e. dom G ( abs ` ( G ` x ) ) <_ y )
149 nfv 
 |-  F/ x ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. RR )
150 nfra1 
 |-  F/ x A. x e. dom G ( abs ` ( G ` x ) ) <_ y
151 149 150 nfan 
 |-  F/ x ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. RR ) /\ A. x e. dom G ( abs ` ( G ` x ) ) <_ y )
152 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> x e. dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
153 fdm 
 |-  ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
154 18 153 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
155 154 adantr 
 |-  ( ( ( 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 ) ) ) )
156 152 155 eleqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
157 fvres 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( G ` x ) )
158 156 157 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( G ` x ) )
159 158 fveq2d 
 |-  ( ( ( 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 ) ) )
160 159 ad4ant14 
 |-  ( ( ( ( ( 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 ) ) )
161 simplr 
 |-  ( ( ( ( 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 )
162 ssdmres 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G <-> dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
163 154 162 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
164 163 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. dom G )
165 156 164 syldan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. dom ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> x e. dom G )
166 165 adantlr 
 |-  ( ( ( ( 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 )
167 rsp 
 |-  ( A. x e. dom G ( abs ` ( G ` x ) ) <_ y -> ( x e. dom G -> ( abs ` ( G ` x ) ) <_ y ) )
168 161 166 167 sylc 
 |-  ( ( ( ( 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 )
169 168 adantllr 
 |-  ( ( ( ( ( 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 )
170 160 169 eqbrtrd 
 |-  ( ( ( ( ( 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 )
171 170 ex 
 |-  ( ( ( ( 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 ) )
172 151 171 ralrimi 
 |-  ( ( ( ( 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 )
173 172 ex 
 |-  ( ( ( 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 ) )
174 173 reximdva 
 |-  ( ( 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 ) )
175 148 174 mpd 
 |-  ( ( 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 )
176 142 147 13 175 cnbdibl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. L^1 )
177 140 176 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( RR _D D ) ` x ) ) e. L^1 )
178 177 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( RR _D D ) ` x ) ) e. L^1 )
179 141 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. dom vol )
180 147 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( vol ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. RR )
181 140 13 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( RR _D D ) ` x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
182 181 adantr 
 |-  ( ( ( 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 ) )
183 coscn 
 |-  cos e. ( CC -cn-> CC )
184 183 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> cos e. ( CC -cn-> CC ) )
185 ioosscn 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
186 185 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
187 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> r e. RR )
188 187 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> r e. CC )
189 ssid 
 |-  CC C_ CC
190 189 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> CC C_ CC )
191 186 188 190 constcncfg 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
192 185 a1i 
 |-  ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
193 189 a1i 
 |-  ( ph -> CC C_ CC )
194 192 193 idcncfg 
 |-  ( ph -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
195 194 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
196 191 195 mulcncf 
 |-  ( ( ( 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 ) )
197 184 196 cncfmpt1f 
 |-  ( ( ( 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 ) )
198 197 negcncfg 
 |-  ( ( ( 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 ) )
199 182 198 mulcncf 
 |-  ( ( ( 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 ) )
200 nfv 
 |-  F/ x ( ph /\ i e. ( 0 ..^ M ) )
201 200 150 nfan 
 |-  F/ x ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. x e. dom G ( abs ` ( G ` x ) ) <_ y )
202 136 fveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D D ) ` x ) = ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) )
203 202 157 sylan9eq 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D D ) ` x ) = ( G ` x ) )
204 203 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D D ) ` x ) ) = ( abs ` ( G ` x ) ) )
205 204 adantlr 
 |-  ( ( ( ( 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 ) ) )
206 simplr 
 |-  ( ( ( ( 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 )
207 164 adantlr 
 |-  ( ( ( ( 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 )
208 206 207 167 sylc 
 |-  ( ( ( ( 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 )
209 205 208 eqbrtrd 
 |-  ( ( ( ( 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 )
210 209 ex 
 |-  ( ( ( 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 ) )
211 201 210 ralrimi 
 |-  ( ( ( 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 )
212 211 ex 
 |-  ( ( 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 ) )
213 212 reximdv 
 |-  ( ( 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 ) )
214 148 213 mpd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. y e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) <_ y )
215 214 adantr 
 |-  ( ( ( 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 )
216 eqidd 
 |-  ( ( ( ( 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 ) ) ) ) )
217 fveq2 
 |-  ( x = z -> ( ( RR _D D ) ` x ) = ( ( RR _D D ) ` z ) )
218 eleq1w 
 |-  ( x = z -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
219 218 anbi2d 
 |-  ( 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 ) ) ) ) ) )
220 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
221 217 220 eqeq12d 
 |-  ( x = z -> ( ( ( RR _D D ) ` x ) = ( G ` x ) <-> ( ( RR _D D ) ` z ) = ( G ` z ) ) )
222 219 221 imbi12d 
 |-  ( 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 ) ) ) )
223 222 203 chvarvv 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D D ) ` z ) = ( G ` z ) )
224 217 223 sylan9eqr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ x = z ) -> ( ( RR _D D ) ` x ) = ( G ` z ) )
225 oveq2 
 |-  ( x = z -> ( r x. x ) = ( r x. z ) )
226 225 fveq2d 
 |-  ( x = z -> ( cos ` ( r x. x ) ) = ( cos ` ( r x. z ) ) )
227 226 negeqd 
 |-  ( x = z -> -u ( cos ` ( r x. x ) ) = -u ( cos ` ( r x. z ) ) )
228 227 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ x = z ) -> -u ( cos ` ( r x. x ) ) = -u ( cos ` ( r x. z ) ) )
229 224 228 oveq12d 
 |-  ( ( ( ( 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 ) ) ) )
230 229 adantllr 
 |-  ( ( ( ( ( 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 ) ) ) )
231 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
232 fvres 
 |-  ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` z ) = ( G ` z ) )
233 232 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` z ) = ( G ` z ) )
234 18 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` z ) e. CC )
235 233 234 eqeltrrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( G ` z ) e. CC )
236 235 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( G ` z ) e. CC )
237 simpl 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. RR )
238 elioore 
 |-  ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> z e. RR )
239 238 adantl 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
240 237 239 remulcld 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. z ) e. RR )
241 240 recnd 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. z ) e. CC )
242 241 coscld 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( cos ` ( r x. z ) ) e. CC )
243 242 negcld 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -u ( cos ` ( r x. z ) ) e. CC )
244 243 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -u ( cos ` ( r x. z ) ) e. CC )
245 236 244 mulcld 
 |-  ( ( ( ( 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 )
246 216 230 231 245 fvmptd 
 |-  ( ( ( ( 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 ) ) ) )
247 246 fveq2d 
 |-  ( ( ( ( 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 ) ) ) ) )
248 247 ad4ant14 
 |-  ( ( ( ( ( ( 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 ) ) ) ) )
249 245 abscld 
 |-  ( ( ( ( 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 )
250 249 ad4ant14 
 |-  ( ( ( ( ( ( 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 )
251 236 abscld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( G ` z ) ) e. RR )
252 251 ad4ant14 
 |-  ( ( ( ( ( ( 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 )
253 simpllr 
 |-  ( ( ( ( ( ( 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 )
254 244 abscld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` -u ( cos ` ( r x. z ) ) ) e. RR )
255 1red 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 1 e. RR )
256 236 absge0d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 <_ ( abs ` ( G ` z ) ) )
257 242 absnegd 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` -u ( cos ` ( r x. z ) ) ) = ( abs ` ( cos ` ( r x. z ) ) ) )
258 abscosbd 
 |-  ( ( r x. z ) e. RR -> ( abs ` ( cos ` ( r x. z ) ) ) <_ 1 )
259 240 258 syl 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( cos ` ( r x. z ) ) ) <_ 1 )
260 257 259 eqbrtrd 
 |-  ( ( r e. RR /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` -u ( cos ` ( r x. z ) ) ) <_ 1 )
261 260 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` -u ( cos ` ( r x. z ) ) ) <_ 1 )
262 254 255 251 256 261 lemul2ad 
 |-  ( ( ( ( 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 ) )
263 236 244 absmuld 
 |-  ( ( ( ( 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 ) ) ) ) )
264 251 recnd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( G ` z ) ) e. CC )
265 264 mulridd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( abs ` ( G ` z ) ) x. 1 ) = ( abs ` ( G ` z ) ) )
266 265 eqcomd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( G ` z ) ) = ( ( abs ` ( G ` z ) ) x. 1 ) )
267 262 263 266 3brtr4d 
 |-  ( ( ( ( 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 ) ) )
268 267 ad4ant14 
 |-  ( ( ( ( ( ( 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 ) ) )
269 simpr 
 |-  ( ( ( 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 )
270 nfra1 
 |-  F/ x A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) <_ y
271 200 270 nfan 
 |-  F/ x ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) <_ y )
272 204 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( G ` x ) ) = ( abs ` ( ( RR _D D ) ` x ) ) )
273 272 adantr 
 |-  ( ( ( ( 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 ) ) )
274 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ ( abs ` ( ( RR _D D ) ` x ) ) <_ y ) -> ( abs ` ( ( RR _D D ) ` x ) ) <_ y )
275 273 274 eqbrtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ ( abs ` ( ( RR _D D ) ` x ) ) <_ y ) -> ( abs ` ( G ` x ) ) <_ y )
276 275 ex 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( abs ` ( ( RR _D D ) ` x ) ) <_ y -> ( abs ` ( G ` x ) ) <_ y ) )
277 276 adantlr 
 |-  ( ( ( ( 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 ) )
278 271 277 ralimdaa 
 |-  ( ( ( 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 ) )
279 269 278 mpd 
 |-  ( ( ( 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 )
280 220 fveq2d 
 |-  ( x = z -> ( abs ` ( G ` x ) ) = ( abs ` ( G ` z ) ) )
281 280 breq1d 
 |-  ( x = z -> ( ( abs ` ( G ` x ) ) <_ y <-> ( abs ` ( G ` z ) ) <_ y ) )
282 281 cbvralvw 
 |-  ( A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( G ` x ) ) <_ y <-> A. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( G ` z ) ) <_ y )
283 279 282 sylib 
 |-  ( ( ( 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 )
284 283 ad4ant14 
 |-  ( ( ( ( ( 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 )
285 284 r19.21bi 
 |-  ( ( ( ( ( ( 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 )
286 250 252 253 268 285 letrd 
 |-  ( ( ( ( ( ( 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 )
287 248 286 eqbrtrd 
 |-  ( ( ( ( ( ( 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 )
288 287 ralrimiva 
 |-  ( ( ( ( ( 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 )
289 138 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D D ) ` x ) e. CC )
290 289 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D D ) ` x ) e. CC )
291 simpl 
 |-  ( ( r e. RR /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. RR )
292 95 adantl 
 |-  ( ( r e. RR /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
293 291 292 remulcld 
 |-  ( ( r e. RR /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. RR )
294 293 recnd 
 |-  ( ( r e. RR /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
295 294 coscld 
 |-  ( ( r e. RR /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( cos ` ( r x. x ) ) e. CC )
296 295 negcld 
 |-  ( ( r e. RR /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -u ( cos ` ( r x. x ) ) e. CC )
297 296 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -u ( cos ` ( r x. x ) ) e. CC )
298 290 297 mulcld 
 |-  ( ( ( ( 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 )
299 298 ralrimiva 
 |-  ( ( ( 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 )
300 dmmptg 
 |-  ( 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 ) ) ) )
301 299 300 syl 
 |-  ( ( ( 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 ) ) ) )
302 301 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) /\ y e. RR ) /\ A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) <_ y ) -> dom ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
303 288 302 raleqtrrdv 
 |-  ( ( ( ( ( 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. dom ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ( abs ` ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ` z ) ) <_ y )
304 303 ex 
 |-  ( ( ( ( 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. dom ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ( abs ` ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ` z ) ) <_ y ) )
305 304 reximdva 
 |-  ( ( ( 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 -> E. y e. RR A. z e. dom ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ( abs ` ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ` z ) ) <_ y ) )
306 215 305 mpd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> E. y e. RR A. z e. dom ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ( abs ` ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) ` z ) ) <_ y )
307 179 180 199 306 cnbdibl 
 |-  ( ( ( 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. L^1 )
308 307 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. RR ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( RR _D D ) ` x ) x. -u ( cos ` ( r x. x ) ) ) ) e. L^1 )
309 289 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D D ) ` x ) e. CC )
310 simpr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ r e. CC ) -> r e. CC )
311 185 sseli 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> x e. CC )
312 311 ad2antlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ r e. CC ) -> x e. CC )
313 310 312 mulcld 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ r e. CC ) -> ( r x. x ) e. CC )
314 313 coscld 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ r e. CC ) -> ( cos ` ( r x. x ) ) e. CC )
315 293 ancoms 
 |-  ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ r e. RR ) -> ( r x. x ) e. RR )
316 abscosbd 
 |-  ( ( r x. x ) e. RR -> ( abs ` ( cos ` ( r x. x ) ) ) <_ 1 )
317 315 316 syl 
 |-  ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. x ) ) ) <_ 1 )
318 317 adantll 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. x ) ) ) <_ 1 )
319 16 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> D = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) ) )
320 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. RR )
321 8 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
322 eqcom 
 |-  ( ( Q ` ( i + 1 ) ) = x <-> x = ( Q ` ( i + 1 ) ) )
323 322 bilanri 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) = x )
324 321 323 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < x )
325 320 324 gtned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> x =/= ( Q ` i ) )
326 325 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> -. x = ( Q ` i ) )
327 326 iffalsed 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
328 iftrue 
 |-  ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
329 328 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
330 327 329 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = L )
331 29 leidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
332 26 29 29 143 331 eliccd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
333 319 330 332 10 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` ( i + 1 ) ) ) = L )
334 333 35 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` ( i + 1 ) ) ) e. CC )
335 334 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( D ` ( Q ` ( i + 1 ) ) ) e. CC )
336 eqid 
 |-  ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) = ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) )
337 iftrue 
 |-  ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
338 337 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` i ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
339 26 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
340 29 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
341 lbicc2 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
342 339 340 143 341 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
343 319 338 342 11 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` i ) ) = R )
344 343 32 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` i ) ) e. CC )
345 344 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( D ` ( Q ` i ) ) e. CC )
346 eqid 
 |-  ( abs ` ( D ` ( Q ` i ) ) ) = ( abs ` ( D ` ( Q ` i ) ) )
347 eqid 
 |-  S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x = S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x
348 simpr 
 |-  ( ( ph /\ e e. RR+ ) -> e e. RR+ )
349 4 nnrpd 
 |-  ( ph -> M e. RR+ )
350 349 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> M e. RR+ )
351 348 350 rpdivcld 
 |-  ( ( ph /\ e e. RR+ ) -> ( e / M ) e. RR+ )
352 351 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( e / M ) e. RR+ )
353 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> r e. CC )
354 29 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
355 354 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( Q ` ( i + 1 ) ) e. CC )
356 353 355 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( r x. ( Q ` ( i + 1 ) ) ) e. CC )
357 356 coscld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) e. CC )
358 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( Q ` ( i + 1 ) ) e. RR )
359 187 358 remulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( r x. ( Q ` ( i + 1 ) ) ) e. RR )
360 abscosbd 
 |-  ( ( r x. ( Q ` ( i + 1 ) ) ) e. RR -> ( abs ` ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) ) <_ 1 )
361 359 360 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) ) <_ 1 )
362 361 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) ) <_ 1 )
363 26 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
364 363 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( Q ` i ) e. CC )
365 353 364 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( r x. ( Q ` i ) ) e. CC )
366 365 coscld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( cos ` ( r x. ( Q ` i ) ) ) e. CC )
367 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( Q ` i ) e. RR )
368 187 367 remulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( r x. ( Q ` i ) ) e. RR )
369 abscosbd 
 |-  ( ( r x. ( Q ` i ) ) e. RR -> ( abs ` ( cos ` ( r x. ( Q ` i ) ) ) ) <_ 1 )
370 368 369 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` i ) ) ) ) <_ 1 )
371 370 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` i ) ) ) ) <_ 1 )
372 fveq2 
 |-  ( z = x -> ( ( RR _D D ) ` z ) = ( ( RR _D D ) ` x ) )
373 372 fveq2d 
 |-  ( z = x -> ( abs ` ( ( RR _D D ) ` z ) ) = ( abs ` ( ( RR _D D ) ` x ) ) )
374 373 cbvitgv 
 |-  S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` z ) ) _d z = S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x
375 374 oveq2i 
 |-  ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` z ) ) _d z ) = ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x )
376 375 oveq1i 
 |-  ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` z ) ) _d z ) / ( e / M ) ) = ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x ) / ( e / M ) )
377 376 oveq1i 
 |-  ( ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` z ) ) _d z ) / ( e / M ) ) + 1 ) = ( ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x ) / ( e / M ) ) + 1 )
378 377 fveq2i 
 |-  ( |_ ` ( ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` z ) ) _d z ) / ( e / M ) ) + 1 ) ) = ( |_ ` ( ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x ) / ( e / M ) ) + 1 ) )
379 378 oveq1i 
 |-  ( ( |_ ` ( ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` z ) ) _d z ) / ( e / M ) ) + 1 ) ) + 1 ) = ( ( |_ ` ( ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x ) / ( e / M ) ) + 1 ) ) + 1 )
380 178 308 309 314 318 335 336 345 346 347 352 357 362 366 371 379 fourierdlem47 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) ) < ( e / M ) )
381 simplll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> ph )
382 simpllr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> i e. ( 0 ..^ M ) )
383 elioore 
 |-  ( r e. ( m (,) +oo ) -> r e. RR )
384 383 adantl 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> r e. RR )
385 0red 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> 0 e. RR )
386 nnre 
 |-  ( m e. NN -> m e. RR )
387 386 adantr 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> m e. RR )
388 nngt0 
 |-  ( m e. NN -> 0 < m )
389 388 adantr 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> 0 < m )
390 387 rexrd 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> m e. RR* )
391 pnfxr 
 |-  +oo e. RR*
392 391 a1i 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> +oo e. RR* )
393 simpr 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> r e. ( m (,) +oo ) )
394 ioogtlb 
 |-  ( ( m e. RR* /\ +oo e. RR* /\ r e. ( m (,) +oo ) ) -> m < r )
395 390 392 393 394 syl3anc 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> m < r )
396 385 387 384 389 395 lttrd 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> 0 < r )
397 384 396 elrpd 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> r e. RR+ )
398 397 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> r e. RR+ )
399 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( Q ` i ) e. RR )
400 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( Q ` ( i + 1 ) ) e. RR )
401 72 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( D ` x ) e. CC )
402 401 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( D ` x ) e. CC )
403 rpcn 
 |-  ( r e. RR+ -> r e. CC )
404 403 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
405 44 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
406 405 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
407 404 406 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
408 407 sincld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
409 402 408 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
410 399 400 409 itgioo 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
411 143 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( Q ` i ) <_ ( Q ` ( i + 1 ) ) )
412 72 feqmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> D = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( D ` x ) ) )
413 iftrue 
 |-  ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
414 328 413 eqtr4d 
 |-  ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
415 414 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
416 iffalse 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) )
417 416 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) )
418 54 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. RR* )
419 55 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
420 44 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. RR )
421 26 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR )
422 44 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x e. RR )
423 57 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) <_ x )
424 neqne 
 |-  ( -. x = ( Q ` i ) -> x =/= ( Q ` i ) )
425 424 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x =/= ( Q ` i ) )
426 421 422 423 425 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) < x )
427 426 adantr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < x )
428 44 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. RR )
429 29 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
430 60 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
431 322 biimpi 
 |-  ( ( Q ` ( i + 1 ) ) = x -> x = ( Q ` ( i + 1 ) ) )
432 431 necon3bi 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) =/= x )
433 432 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) =/= x )
434 428 429 430 433 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x < ( Q ` ( i + 1 ) ) )
435 434 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x < ( Q ` ( i + 1 ) ) )
436 418 419 420 427 435 eliood 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
437 fvres 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
438 436 437 syl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
439 iffalse 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
440 439 eqcomd 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> ( F ` x ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
441 440 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( F ` x ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
442 417 438 441 3eqtrrd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
443 415 442 pm2.61dan 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
444 443 ifeq2da 
 |-  ( ( ( 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 ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
445 444 mpteq2dva 
 |-  ( ( 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 ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) )
446 319 412 445 3eqtr3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( D ` x ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) )
447 eqid 
 |-  ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
448 200 447 26 29 9 10 11 cncfiooicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
449 446 448 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( D ` x ) ) e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
450 412 449 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> D e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
451 450 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> D e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
452 eqid 
 |-  ( RR _D D ) = ( RR _D D )
453 136 13 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D D ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
454 453 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( RR _D D ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
455 214 adantr 
 |-  ( ( ( 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 )
456 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> r e. RR+ )
457 399 400 411 451 452 454 455 456 fourierdlem39 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) )
458 410 457 eqtr3d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) )
459 381 382 398 458 syl21anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) )
460 459 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) = ( abs ` ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) ) )
461 460 breq1d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> ( ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> ( abs ` ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) ) < ( e / M ) ) )
462 461 ralbidva 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) -> ( A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> A. r e. ( m (,) +oo ) ( abs ` ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) ) < ( e / M ) ) )
463 462 rexbidva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) ) < ( e / M ) ) )
464 463 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` ( ( ( ( D ` ( Q ` ( i + 1 ) ) ) x. -u ( ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) / r ) ) - ( ( D ` ( Q ` i ) ) x. -u ( ( cos ` ( r x. ( Q ` i ) ) ) / r ) ) ) - S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( ( RR _D D ) ` x ) x. -u ( ( cos ` ( r x. x ) ) / r ) ) _d x ) ) < ( e / M ) ) )
465 380 464 mpbird 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
466 465 an32s 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
467 102 oveq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) = ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) )
468 467 itgeq2dv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
469 468 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
470 469 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
471 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> ( Q ` i ) e. RR )
472 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> ( Q ` ( i + 1 ) ) e. RR )
473 401 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( D ` x ) e. CC )
474 383 recnd 
 |-  ( r e. ( m (,) +oo ) -> r e. CC )
475 474 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
476 405 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
477 475 476 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
478 477 sincld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
479 473 478 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
480 471 472 479 itgioo 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
481 69 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
482 481 478 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
483 471 472 482 itgioo 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
484 470 480 483 3eqtr3d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
485 484 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) = ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
486 485 breq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> ( ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) )
487 486 ralbidva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) )
488 487 adantlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) )
489 488 rexbidv 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( D ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) )
490 466 489 mpbid 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
491 490 ralrimiva 
 |-  ( ( ph /\ e e. RR+ ) -> A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
492 491 ralrimiva 
 |-  ( ph -> A. e e. RR+ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
493 nfv 
 |-  F/ i ( ph /\ e e. RR+ )
494 nfra1 
 |-  F/ i A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M )
495 493 494 nfan 
 |-  F/ i ( ( ph /\ e e. RR+ ) /\ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
496 nfv 
 |-  F/ r ( ph /\ e e. RR+ )
497 nfcv 
 |-  F/_ r ( 0 ..^ M )
498 nfcv 
 |-  F/_ r NN
499 nfra1 
 |-  F/ r A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M )
500 498 499 nfrexw 
 |-  F/ r E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M )
501 497 500 nfralw 
 |-  F/ r A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M )
502 496 501 nfan 
 |-  F/ r ( ( ph /\ e e. RR+ ) /\ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
503 nfmpt1 
 |-  F/_ i ( i e. ( 0 ..^ M ) |-> inf ( { m e. NN | A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) } , RR , < ) )
504 fzofi 
 |-  ( 0 ..^ M ) e. Fin
505 504 a1i 
 |-  ( ( ( ph /\ e e. RR+ ) /\ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> ( 0 ..^ M ) e. Fin )
506 simpr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
507 eqid 
 |-  { m e. NN | A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) } = { m e. NN | A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) }
508 eqid 
 |-  ( i e. ( 0 ..^ M ) |-> inf ( { m e. NN | A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) } , RR , < ) ) = ( i e. ( 0 ..^ M ) |-> inf ( { m e. NN | A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) } , RR , < ) )
509 eqid 
 |-  sup ( ran ( i e. ( 0 ..^ M ) |-> inf ( { m e. NN | A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) } , RR , < ) ) , RR , < ) = sup ( ran ( i e. ( 0 ..^ M ) |-> inf ( { m e. NN | A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) } , RR , < ) ) , RR , < )
510 495 502 503 505 506 507 508 509 fourierdlem31 
 |-  ( ( ( ph /\ e e. RR+ ) /\ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
511 simpr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
512 nfv 
 |-  F/ n ( ph /\ e e. RR+ )
513 nfre1 
 |-  F/ n E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M )
514 512 513 nfan 
 |-  F/ n ( ( ph /\ e e. RR+ ) /\ E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
515 nfv 
 |-  F/ r n e. NN
516 nfra1 
 |-  F/ r A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M )
517 496 515 516 nf3an 
 |-  F/ r ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
518 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ph )
519 elioore 
 |-  ( r e. ( n (,) +oo ) -> r e. RR )
520 519 adantl 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> r e. RR )
521 0red 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> 0 e. RR )
522 nnre 
 |-  ( n e. NN -> n e. RR )
523 522 adantr 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> n e. RR )
524 nngt0 
 |-  ( n e. NN -> 0 < n )
525 524 adantr 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> 0 < n )
526 523 rexrd 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> n e. RR* )
527 391 a1i 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> +oo e. RR* )
528 simpr 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> r e. ( n (,) +oo ) )
529 ioogtlb 
 |-  ( ( n e. RR* /\ +oo e. RR* /\ r e. ( n (,) +oo ) ) -> n < r )
530 526 527 528 529 syl3anc 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> n < r )
531 521 523 520 525 530 lttrd 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> 0 < r )
532 520 531 elrpd 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> r e. RR+ )
533 532 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> r e. RR+ )
534 1 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> A e. RR )
535 2 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> B e. RR )
536 3 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
537 536 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
538 403 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> r e. CC )
539 21 sselda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
540 539 recnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
541 540 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> x e. CC )
542 538 541 mulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( r x. x ) e. CC )
543 542 sincld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( sin ` ( r x. x ) ) e. CC )
544 537 543 mulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
545 534 535 544 itgioo 
 |-  ( ( ph /\ r e. RR+ ) -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( A [,] B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
546 6 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
547 7 eqcomd 
 |-  ( ph -> B = ( Q ` M ) )
548 546 547 oveq12d 
 |-  ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
549 548 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
550 549 itgeq1d 
 |-  ( ( ph /\ r e. RR+ ) -> S. ( A [,] B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
551 0zd 
 |-  ( ( ph /\ r e. RR+ ) -> 0 e. ZZ )
552 nnuz 
 |-  NN = ( ZZ>= ` 1 )
553 0p1e1 
 |-  ( 0 + 1 ) = 1
554 553 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
555 552 554 eqtr4i 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
556 4 555 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
557 556 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
558 22 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> Q : ( 0 ... M ) --> RR )
559 8 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
560 simpr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
561 548 eqcomd 
 |-  ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( A [,] B ) )
562 561 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( A [,] B ) )
563 560 562 eleqtrd 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( A [,] B ) )
564 563 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( A [,] B ) )
565 564 544 syldan 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
566 26 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
567 29 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
568 114 111 sstrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
569 121 568 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
570 569 9 eqeltrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
571 570 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
572 sincn 
 |-  sin e. ( CC -cn-> CC )
573 572 a1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> sin e. ( CC -cn-> CC ) )
574 185 a1i 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
575 403 adantl 
 |-  ( ( ph /\ r e. RR+ ) -> r e. CC )
576 189 a1i 
 |-  ( ( ph /\ r e. RR+ ) -> CC C_ CC )
577 574 575 576 constcncfg 
 |-  ( ( ph /\ r e. RR+ ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
578 194 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
579 577 578 mulcncf 
 |-  ( ( ph /\ r e. RR+ ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
580 579 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
581 573 580 cncfmpt1f 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( sin ` ( r x. x ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
582 571 581 mulcncf 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
583 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) )
584 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( sin ` ( r x. x ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( sin ` ( r x. x ) ) )
585 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) )
586 3 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> F : ( A [,] B ) --> CC )
587 45 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
588 47 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
589 5 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
590 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
591 587 588 589 590 80 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
592 586 591 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
593 592 adantllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
594 575 ad2antrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
595 311 adantl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
596 594 595 mulcld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
597 596 sincld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
598 569 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` ( i + 1 ) ) ) )
599 10 598 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` ( i + 1 ) ) ) )
600 599 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` ( i + 1 ) ) ) )
601 rpre 
 |-  ( r e. RR+ -> r e. RR )
602 601 adantr 
 |-  ( ( r e. RR+ /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. RR )
603 95 adantl 
 |-  ( ( r e. RR+ /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
604 602 603 remulcld 
 |-  ( ( r e. RR+ /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. RR )
605 604 adantll 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. RR )
606 605 ad2ant2r 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ ( r x. x ) =/= ( r x. ( Q ` ( i + 1 ) ) ) ) ) -> ( r x. x ) e. RR )
607 recn 
 |-  ( y e. RR -> y e. CC )
608 607 sincld 
 |-  ( y e. RR -> ( sin ` y ) e. CC )
609 608 adantl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ y e. RR ) -> ( sin ` y ) e. CC )
610 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r )
611 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x )
612 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) )
613 185 a1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
614 575 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. CC )
615 567 recnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
616 610 613 614 615 constlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) limCC ( Q ` ( i + 1 ) ) ) )
617 613 611 615 idlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) limCC ( Q ` ( i + 1 ) ) ) )
618 610 611 612 594 595 616 617 mullimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( r x. ( Q ` ( i + 1 ) ) ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) ) limCC ( Q ` ( i + 1 ) ) ) )
619 eqid 
 |-  ( y e. CC |-> ( sin ` y ) ) = ( y e. CC |-> ( sin ` y ) )
620 sinf 
 |-  sin : CC --> CC
621 620 a1i 
 |-  ( T. -> sin : CC --> CC )
622 621 feqmptd 
 |-  ( T. -> sin = ( y e. CC |-> ( sin ` y ) ) )
623 622 572 eqeltrrdi 
 |-  ( T. -> ( y e. CC |-> ( sin ` y ) ) e. ( CC -cn-> CC ) )
624 19 a1i 
 |-  ( T. -> RR C_ CC )
625 resincl 
 |-  ( y e. RR -> ( sin ` y ) e. RR )
626 625 adantl 
 |-  ( ( T. /\ y e. RR ) -> ( sin ` y ) e. RR )
627 619 623 624 624 626 cncfmptssg 
 |-  ( T. -> ( y e. RR |-> ( sin ` y ) ) e. ( RR -cn-> RR ) )
628 627 mptru 
 |-  ( y e. RR |-> ( sin ` y ) ) e. ( RR -cn-> RR )
629 628 a1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( y e. RR |-> ( sin ` y ) ) e. ( RR -cn-> RR ) )
630 601 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. RR )
631 630 567 remulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( r x. ( Q ` ( i + 1 ) ) ) e. RR )
632 fveq2 
 |-  ( y = ( r x. ( Q ` ( i + 1 ) ) ) -> ( sin ` y ) = ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) )
633 629 631 632 cnmptlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) e. ( ( y e. RR |-> ( sin ` y ) ) limCC ( r x. ( Q ` ( i + 1 ) ) ) ) )
634 fveq2 
 |-  ( y = ( r x. x ) -> ( sin ` y ) = ( sin ` ( r x. x ) ) )
635 fveq2 
 |-  ( ( r x. x ) = ( r x. ( Q ` ( i + 1 ) ) ) -> ( sin ` ( r x. x ) ) = ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) )
636 635 ad2antll 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ ( r x. x ) = ( r x. ( Q ` ( i + 1 ) ) ) ) ) -> ( sin ` ( r x. x ) ) = ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) )
637 606 609 618 633 634 636 limcco 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( sin ` ( r x. x ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
638 583 584 585 593 597 600 637 mullimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( L x. ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
639 569 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` i ) ) )
640 11 639 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` i ) ) )
641 640 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` i ) ) )
642 605 ad2ant2r 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ ( r x. x ) =/= ( r x. ( Q ` i ) ) ) ) -> ( r x. x ) e. RR )
643 566 recnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
644 610 613 614 643 constlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) limCC ( Q ` i ) ) )
645 613 611 643 idlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) limCC ( Q ` i ) ) )
646 610 611 612 594 595 644 645 mullimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( r x. ( Q ` i ) ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) ) limCC ( Q ` i ) ) )
647 630 566 remulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( r x. ( Q ` i ) ) e. RR )
648 fveq2 
 |-  ( y = ( r x. ( Q ` i ) ) -> ( sin ` y ) = ( sin ` ( r x. ( Q ` i ) ) ) )
649 629 647 648 cnmptlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( sin ` ( r x. ( Q ` i ) ) ) e. ( ( y e. RR |-> ( sin ` y ) ) limCC ( r x. ( Q ` i ) ) ) )
650 fveq2 
 |-  ( ( r x. x ) = ( r x. ( Q ` i ) ) -> ( sin ` ( r x. x ) ) = ( sin ` ( r x. ( Q ` i ) ) ) )
651 650 ad2antll 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ ( r x. x ) = ( r x. ( Q ` i ) ) ) ) -> ( sin ` ( r x. x ) ) = ( sin ` ( r x. ( Q ` i ) ) ) )
652 642 609 646 649 634 651 limcco 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( sin ` ( r x. ( Q ` i ) ) ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( sin ` ( r x. x ) ) ) limCC ( Q ` i ) ) )
653 583 584 585 593 597 641 652 mullimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( R x. ( sin ` ( r x. ( Q ` i ) ) ) ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) ) limCC ( Q ` i ) ) )
654 566 567 582 638 653 iblcncfioo 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) ) e. L^1 )
655 simpll 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ph /\ r e. RR+ ) )
656 68 adantllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
657 655 656 544 syl2anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
658 566 567 654 657 ibliooicc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) ) e. L^1 )
659 551 557 558 559 565 658 itgspltprt 
 |-  ( ( ph /\ r e. RR+ ) -> S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
660 545 550 659 3eqtrd 
 |-  ( ( ph /\ r e. RR+ ) -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
661 518 533 660 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
662 504 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ( 0 ..^ M ) e. Fin )
663 69 adantllr 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
664 519 recnd 
 |-  ( r e. ( n (,) +oo ) -> r e. CC )
665 664 adantl 
 |-  ( ( ph /\ r e. ( n (,) +oo ) ) -> r e. CC )
666 665 ad2antrr 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
667 405 adantllr 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
668 666 667 mulcld 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
669 668 sincld 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
670 663 669 mulcld 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
671 670 adantl3r 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
672 simplll 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> ph )
673 533 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> r e. RR+ )
674 simpr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
675 672 673 674 658 syl21anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) ) e. L^1 )
676 671 675 itgcl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
677 662 676 fsumcl 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
678 661 677 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
679 678 adantllr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
680 679 3adantl3 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
681 680 abscld 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) e. RR )
682 676 abscld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) e. RR )
683 662 682 fsumrecl 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) e. RR )
684 683 adantllr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) e. RR )
685 684 3adantl3 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) e. RR )
686 rpre 
 |-  ( e e. RR+ -> e e. RR )
687 686 ad2antlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ r e. ( n (,) +oo ) ) -> e e. RR )
688 687 3ad2antl1 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> e e. RR )
689 661 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) = ( abs ` sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
690 662 676 fsumabs 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ( abs ` sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) <_ sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
691 689 690 eqbrtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) <_ sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
692 691 adantllr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) <_ sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
693 692 3adantl3 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) <_ sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
694 504 a1i 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> ( 0 ..^ M ) e. Fin )
695 0zd 
 |-  ( ph -> 0 e. ZZ )
696 4 nnzd 
 |-  ( ph -> M e. ZZ )
697 4 nngt0d 
 |-  ( ph -> 0 < M )
698 fzolb 
 |-  ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
699 695 696 697 698 syl3anbrc 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
700 ne0i 
 |-  ( 0 e. ( 0 ..^ M ) -> ( 0 ..^ M ) =/= (/) )
701 699 700 syl 
 |-  ( ph -> ( 0 ..^ M ) =/= (/) )
702 701 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ r e. ( n (,) +oo ) ) -> ( 0 ..^ M ) =/= (/) )
703 702 3ad2antl1 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> ( 0 ..^ M ) =/= (/) )
704 simp1l 
 |-  ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> ph )
705 704 ad2antrr 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> ph )
706 simpll2 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> n e. NN )
707 705 706 jca 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> ( ph /\ n e. NN ) )
708 simplr 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> r e. ( n (,) +oo ) )
709 simpr 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> j e. ( 0 ..^ M ) )
710 eleq1w 
 |-  ( i = j -> ( i e. ( 0 ..^ M ) <-> j e. ( 0 ..^ M ) ) )
711 710 anbi2d 
 |-  ( i = j -> ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) <-> ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) ) )
712 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
713 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
714 713 fveq2d 
 |-  ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
715 712 714 oveq12d 
 |-  ( i = j -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) )
716 715 itgeq1d 
 |-  ( i = j -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
717 716 eleq1d 
 |-  ( i = j -> ( S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC <-> S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC ) )
718 711 717 imbi12d 
 |-  ( i = j -> ( ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC ) <-> ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC ) ) )
719 718 676 chvarvv 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
720 707 708 709 719 syl21anc 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
721 720 abscld 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) e. RR )
722 351 rpred 
 |-  ( ( ph /\ e e. RR+ ) -> ( e / M ) e. RR )
723 722 3ad2ant1 
 |-  ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> ( e / M ) e. RR )
724 723 ad2antrr 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> ( e / M ) e. RR )
725 simpll3 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
726 rspa 
 |-  ( ( A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) /\ r e. ( n (,) +oo ) ) -> A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
727 726 adantr 
 |-  ( ( ( A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
728 716 fveq2d 
 |-  ( i = j -> ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) = ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
729 728 breq1d 
 |-  ( i = j -> ( ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) )
730 729 cbvralvw 
 |-  ( A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) <-> A. j e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
731 727 730 sylib 
 |-  ( ( ( A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> A. j e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
732 rspa 
 |-  ( ( A. j e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) /\ j e. ( 0 ..^ M ) ) -> ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
733 731 732 sylancom 
 |-  ( ( ( A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
734 725 708 709 733 syl21anc 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) /\ j e. ( 0 ..^ M ) ) -> ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) )
735 694 703 721 724 734 fsumlt 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> sum_ j e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < sum_ j e. ( 0 ..^ M ) ( e / M ) )
736 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
737 oveq1 
 |-  ( j = i -> ( j + 1 ) = ( i + 1 ) )
738 737 fveq2d 
 |-  ( j = i -> ( Q ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) )
739 736 738 oveq12d 
 |-  ( j = i -> ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) = ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
740 739 itgeq1d 
 |-  ( j = i -> S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
741 740 fveq2d 
 |-  ( j = i -> ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) = ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
742 741 cbvsumv 
 |-  sum_ j e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) = sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )
743 742 a1i 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> sum_ j e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) = sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) )
744 351 rpcnd 
 |-  ( ( ph /\ e e. RR+ ) -> ( e / M ) e. CC )
745 fsumconst 
 |-  ( ( ( 0 ..^ M ) e. Fin /\ ( e / M ) e. CC ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) )
746 504 744 745 sylancr 
 |-  ( ( ph /\ e e. RR+ ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) )
747 4 nnnn0d 
 |-  ( ph -> M e. NN0 )
748 hashfzo0 
 |-  ( M e. NN0 -> ( # ` ( 0 ..^ M ) ) = M )
749 747 748 syl 
 |-  ( ph -> ( # ` ( 0 ..^ M ) ) = M )
750 749 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) = ( M x. ( e / M ) ) )
751 750 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) = ( M x. ( e / M ) ) )
752 348 rpcnd 
 |-  ( ( ph /\ e e. RR+ ) -> e e. CC )
753 350 rpcnd 
 |-  ( ( ph /\ e e. RR+ ) -> M e. CC )
754 350 rpne0d 
 |-  ( ( ph /\ e e. RR+ ) -> M =/= 0 )
755 752 753 754 divcan2d 
 |-  ( ( ph /\ e e. RR+ ) -> ( M x. ( e / M ) ) = e )
756 746 751 755 3eqtrd 
 |-  ( ( ph /\ e e. RR+ ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = e )
757 756 adantr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ r e. ( n (,) +oo ) ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = e )
758 757 3ad2antl1 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = e )
759 735 743 758 3brtr3d 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> sum_ i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e )
760 681 685 688 693 759 lelttrd 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) /\ r e. ( n (,) +oo ) ) -> ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e )
761 760 ex 
 |-  ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> ( r e. ( n (,) +oo ) -> ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e ) )
762 517 761 ralrimi 
 |-  ( ( ( ph /\ e e. RR+ ) /\ n e. NN /\ A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e )
763 762 3exp 
 |-  ( ( ph /\ e e. RR+ ) -> ( n e. NN -> ( A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) -> A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e ) ) )
764 763 adantr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> ( n e. NN -> ( A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) -> A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e ) ) )
765 514 764 reximdai 
 |-  ( ( ( ph /\ e e. RR+ ) /\ E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> ( E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) -> E. n e. NN A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e ) )
766 511 765 mpd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ E. n e. NN A. r e. ( n (,) +oo ) A. i e. ( 0 ..^ M ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> E. n e. NN A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e )
767 510 766 syldan 
 |-  ( ( ( ph /\ e e. RR+ ) /\ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) ) -> E. n e. NN A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e )
768 767 ex 
 |-  ( ( ph /\ e e. RR+ ) -> ( A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) -> E. n e. NN A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e ) )
769 768 ralimdva 
 |-  ( ph -> ( A. e e. RR+ A. i e. ( 0 ..^ M ) E. m e. NN A. r e. ( m (,) +oo ) ( abs ` S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < ( e / M ) -> 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 ) )
770 492 769 mpd 
 |-  ( 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 )