This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimpri 
 |-  ( x = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) = x )
324 323 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) = x )
325 321 324 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < x )
326 320 325 gtned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> x =/= ( Q ` i ) )
327 326 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> -. x = ( Q ` i ) )
328 327 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 ) ) )
329 iftrue 
 |-  ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
330 329 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
331 328 330 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = L )
332 29 leidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
333 26 29 29 143 332 eliccd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
334 319 331 333 10 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` ( i + 1 ) ) ) = L )
335 334 35 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` ( i + 1 ) ) ) e. CC )
336 335 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( D ` ( Q ` ( i + 1 ) ) ) e. CC )
337 eqid 
 |-  ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) = ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) )
338 iftrue 
 |-  ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
339 338 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( Q ` i ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
340 26 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
341 29 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
342 lbicc2 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
343 340 341 143 342 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
344 319 339 343 11 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` i ) ) = R )
345 344 32 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` ( Q ` i ) ) e. CC )
346 345 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( D ` ( Q ` i ) ) e. CC )
347 eqid 
 |-  ( abs ` ( D ` ( Q ` i ) ) ) = ( abs ` ( D ` ( Q ` i ) ) )
348 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
349 simpr 
 |-  ( ( ph /\ e e. RR+ ) -> e e. RR+ )
350 4 nnrpd 
 |-  ( ph -> M e. RR+ )
351 350 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> M e. RR+ )
352 349 351 rpdivcld 
 |-  ( ( ph /\ e e. RR+ ) -> ( e / M ) e. RR+ )
353 352 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) -> ( e / M ) e. RR+ )
354 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> r e. CC )
355 29 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
356 355 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( Q ` ( i + 1 ) ) e. CC )
357 354 356 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( r x. ( Q ` ( i + 1 ) ) ) e. CC )
358 357 coscld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) e. CC )
359 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( Q ` ( i + 1 ) ) e. RR )
360 187 359 remulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( r x. ( Q ` ( i + 1 ) ) ) e. RR )
361 abscosbd 
 |-  ( ( r x. ( Q ` ( i + 1 ) ) ) e. RR -> ( abs ` ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) ) <_ 1 )
362 360 361 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) ) <_ 1 )
363 362 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` ( i + 1 ) ) ) ) ) <_ 1 )
364 26 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
365 364 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( Q ` i ) e. CC )
366 354 365 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( r x. ( Q ` i ) ) e. CC )
367 366 coscld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. CC ) -> ( cos ` ( r x. ( Q ` i ) ) ) e. CC )
368 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( Q ` i ) e. RR )
369 187 368 remulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( r x. ( Q ` i ) ) e. RR )
370 abscosbd 
 |-  ( ( r x. ( Q ` i ) ) e. RR -> ( abs ` ( cos ` ( r x. ( Q ` i ) ) ) ) <_ 1 )
371 369 370 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` i ) ) ) ) <_ 1 )
372 371 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ e e. RR+ ) /\ r e. RR ) -> ( abs ` ( cos ` ( r x. ( Q ` i ) ) ) ) <_ 1 )
373 fveq2 
 |-  ( z = x -> ( ( RR _D D ) ` z ) = ( ( RR _D D ) ` x ) )
374 373 fveq2d 
 |-  ( z = x -> ( abs ` ( ( RR _D D ) ` z ) ) = ( abs ` ( ( RR _D D ) ` x ) ) )
375 374 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
376 375 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 )
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 ) ) = ( ( ( ( abs ` ( D ` ( Q ` ( i + 1 ) ) ) ) + ( abs ` ( D ` ( Q ` i ) ) ) ) + S. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D D ) ` x ) ) _d x ) / ( e / M ) )
378 377 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 )
379 378 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 ) )
380 379 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 )
381 178 308 309 314 318 336 337 346 347 348 353 358 363 367 372 380 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 ) )
382 simplll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> ph )
383 simpllr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> i e. ( 0 ..^ M ) )
384 elioore 
 |-  ( r e. ( m (,) +oo ) -> r e. RR )
385 384 adantl 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> r e. RR )
386 0red 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> 0 e. RR )
387 nnre 
 |-  ( m e. NN -> m e. RR )
388 387 adantr 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> m e. RR )
389 nngt0 
 |-  ( m e. NN -> 0 < m )
390 389 adantr 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> 0 < m )
391 388 rexrd 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> m e. RR* )
392 pnfxr 
 |-  +oo e. RR*
393 392 a1i 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> +oo e. RR* )
394 simpr 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> r e. ( m (,) +oo ) )
395 ioogtlb 
 |-  ( ( m e. RR* /\ +oo e. RR* /\ r e. ( m (,) +oo ) ) -> m < r )
396 391 393 394 395 syl3anc 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> m < r )
397 386 388 385 390 396 lttrd 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> 0 < r )
398 385 397 elrpd 
 |-  ( ( m e. NN /\ r e. ( m (,) +oo ) ) -> r e. RR+ )
399 398 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ m e. NN ) /\ r e. ( m (,) +oo ) ) -> r e. RR+ )
400 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( Q ` i ) e. RR )
401 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( Q ` ( i + 1 ) ) e. RR )
402 72 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( D ` x ) e. CC )
403 402 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( D ` x ) e. CC )
404 rpcn 
 |-  ( r e. RR+ -> r e. CC )
405 404 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
406 44 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
407 406 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
408 405 407 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
409 408 sincld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
410 403 409 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 )
411 400 401 410 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 )
412 143 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( Q ` i ) <_ ( Q ` ( i + 1 ) ) )
413 72 feqmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> D = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( D ` x ) ) )
414 iftrue 
 |-  ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
415 329 414 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 ) ) )
416 415 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 ) ) )
417 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 ) )
418 417 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 ) )
419 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* )
420 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* )
421 44 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. RR )
422 26 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR )
423 44 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x e. RR )
424 57 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) <_ x )
425 neqne 
 |-  ( -. x = ( Q ` i ) -> x =/= ( Q ` i ) )
426 425 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x =/= ( Q ` i ) )
427 422 423 424 426 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) < x )
428 427 adantr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < x )
429 44 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. RR )
430 29 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
431 60 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
432 322 biimpi 
 |-  ( ( Q ` ( i + 1 ) ) = x -> x = ( Q ` ( i + 1 ) ) )
433 432 necon3bi 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) =/= x )
434 433 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) =/= x )
435 429 430 431 434 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x < ( Q ` ( i + 1 ) ) )
436 435 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x < ( Q ` ( i + 1 ) ) )
437 419 420 421 428 436 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 ) ) ) )
438 fvres 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
439 437 438 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 ) )
440 iffalse 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
441 440 eqcomd 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> ( F ` x ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
442 441 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 ) ) )
443 418 439 442 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 ) ) )
444 416 443 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 ) ) )
445 444 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 ) ) ) )
446 445 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 ) ) ) ) )
447 319 413 446 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 ) ) ) ) )
448 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 ) ) ) )
449 200 448 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 ) )
450 447 449 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( D ` x ) ) e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
451 413 450 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> D e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
452 451 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> D e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
453 eqid 
 |-  ( RR _D D ) = ( RR _D D )
454 136 13 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D D ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
455 454 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> ( RR _D D ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
456 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 )
457 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. RR+ ) -> r e. RR+ )
458 400 401 412 452 453 455 456 457 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 ) )
459 411 458 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 ) )
460 382 383 399 459 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 ) )
461 460 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 ) ) )
462 461 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 ) ) )
463 462 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 ) ) )
464 463 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 ) ) )
465 464 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 ) ) )
466 381 465 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 ) )
467 466 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 ) )
468 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 ) ) ) )
469 468 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 )
470 469 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 )
471 470 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 )
472 26 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> ( Q ` i ) e. RR )
473 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) -> ( Q ` ( i + 1 ) ) e. RR )
474 402 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( D ` x ) e. CC )
475 384 recnd 
 |-  ( r e. ( m (,) +oo ) -> r e. CC )
476 475 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
477 406 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
478 476 477 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
479 478 sincld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
480 474 479 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 )
481 472 473 480 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 )
482 69 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( m (,) +oo ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
483 482 479 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 )
484 472 473 483 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 )
485 471 481 484 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 )
486 485 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 ) )
487 486 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 ) ) )
488 487 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 ) ) )
489 488 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 ) ) )
490 489 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 ) ) )
491 467 490 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 ) )
492 491 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 ) )
493 492 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 ) )
494 nfv 
 |-  F/ i ( ph /\ e e. RR+ )
495 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 )
496 494 495 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 ) )
497 nfv 
 |-  F/ r ( ph /\ e e. RR+ )
498 nfcv 
 |-  F/_ r ( 0 ..^ M )
499 nfcv 
 |-  F/_ r NN
500 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 )
501 499 500 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 )
502 498 501 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 )
503 497 502 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 ) )
504 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 , < ) )
505 fzofi 
 |-  ( 0 ..^ M ) e. Fin
506 505 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 )
507 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 ) )
508 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 ) }
509 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 , < ) )
510 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 , < )
511 496 503 504 506 507 508 509 510 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 ) )
512 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 ) )
513 nfv 
 |-  F/ n ( ph /\ e e. RR+ )
514 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 )
515 513 514 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 ) )
516 nfv 
 |-  F/ r n e. NN
517 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 )
518 497 516 517 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 ) )
519 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ph )
520 elioore 
 |-  ( r e. ( n (,) +oo ) -> r e. RR )
521 520 adantl 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> r e. RR )
522 0red 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> 0 e. RR )
523 nnre 
 |-  ( n e. NN -> n e. RR )
524 523 adantr 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> n e. RR )
525 nngt0 
 |-  ( n e. NN -> 0 < n )
526 525 adantr 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> 0 < n )
527 524 rexrd 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> n e. RR* )
528 392 a1i 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> +oo e. RR* )
529 simpr 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> r e. ( n (,) +oo ) )
530 ioogtlb 
 |-  ( ( n e. RR* /\ +oo e. RR* /\ r e. ( n (,) +oo ) ) -> n < r )
531 527 528 529 530 syl3anc 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> n < r )
532 522 524 521 526 531 lttrd 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> 0 < r )
533 521 532 elrpd 
 |-  ( ( n e. NN /\ r e. ( n (,) +oo ) ) -> r e. RR+ )
534 533 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> r e. RR+ )
535 1 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> A e. RR )
536 2 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> B e. RR )
537 3 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
538 537 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
539 404 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> r e. CC )
540 21 sselda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
541 540 recnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
542 541 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> x e. CC )
543 539 542 mulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( r x. x ) e. CC )
544 543 sincld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( sin ` ( r x. x ) ) e. CC )
545 538 544 mulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( A [,] B ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
546 535 536 545 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 )
547 6 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
548 7 eqcomd 
 |-  ( ph -> B = ( Q ` M ) )
549 547 548 oveq12d 
 |-  ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
550 549 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
551 550 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 )
552 0zd 
 |-  ( ( ph /\ r e. RR+ ) -> 0 e. ZZ )
553 nnuz 
 |-  NN = ( ZZ>= ` 1 )
554 0p1e1 
 |-  ( 0 + 1 ) = 1
555 554 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
556 553 555 eqtr4i 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
557 4 556 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
558 557 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
559 22 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> Q : ( 0 ... M ) --> RR )
560 8 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
561 simpr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
562 549 eqcomd 
 |-  ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( A [,] B ) )
563 562 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( A [,] B ) )
564 561 563 eleqtrd 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( A [,] B ) )
565 564 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( A [,] B ) )
566 565 545 syldan 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) e. CC )
567 26 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
568 29 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
569 114 111 sstrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
570 121 569 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
571 570 9 eqeltrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
572 571 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 ) )
573 sincn 
 |-  sin e. ( CC -cn-> CC )
574 573 a1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> sin e. ( CC -cn-> CC ) )
575 185 a1i 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
576 404 adantl 
 |-  ( ( ph /\ r e. RR+ ) -> r e. CC )
577 189 a1i 
 |-  ( ( ph /\ r e. RR+ ) -> CC C_ CC )
578 575 576 577 constcncfg 
 |-  ( ( ph /\ r e. RR+ ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
579 194 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
580 578 579 mulcncf 
 |-  ( ( ph /\ r e. RR+ ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
581 580 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 ) )
582 574 581 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 ) )
583 572 582 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 ) )
584 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) )
585 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( sin ` ( r x. x ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( sin ` ( r x. x ) ) )
586 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 ) ) ) )
587 3 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> F : ( A [,] B ) --> CC )
588 45 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
589 47 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
590 5 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
591 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
592 588 589 590 591 80 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
593 587 592 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
594 593 adantllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
595 576 ad2antrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
596 311 adantl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
597 595 596 mulcld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
598 597 sincld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
599 570 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 ) ) ) )
600 10 599 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` ( i + 1 ) ) ) )
601 600 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` ( i + 1 ) ) ) )
602 rpre 
 |-  ( r e. RR+ -> r e. RR )
603 602 adantr 
 |-  ( ( r e. RR+ /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. RR )
604 95 adantl 
 |-  ( ( r e. RR+ /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
605 603 604 remulcld 
 |-  ( ( r e. RR+ /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. RR )
606 605 adantll 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. RR )
607 606 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 )
608 recn 
 |-  ( y e. RR -> y e. CC )
609 608 sincld 
 |-  ( y e. RR -> ( sin ` y ) e. CC )
610 609 adantl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ y e. RR ) -> ( sin ` y ) e. CC )
611 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r )
612 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x )
613 eqid 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( r x. x ) )
614 185 a1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
615 576 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. CC )
616 568 recnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
617 611 614 615 616 constlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) limCC ( Q ` ( i + 1 ) ) ) )
618 614 612 616 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 ) ) ) )
619 611 612 613 595 596 617 618 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 ) ) ) )
620 eqid 
 |-  ( y e. CC |-> ( sin ` y ) ) = ( y e. CC |-> ( sin ` y ) )
621 sinf 
 |-  sin : CC --> CC
622 621 a1i 
 |-  ( T. -> sin : CC --> CC )
623 622 feqmptd 
 |-  ( T. -> sin = ( y e. CC |-> ( sin ` y ) ) )
624 623 573 eqeltrrdi 
 |-  ( T. -> ( y e. CC |-> ( sin ` y ) ) e. ( CC -cn-> CC ) )
625 19 a1i 
 |-  ( T. -> RR C_ CC )
626 resincl 
 |-  ( y e. RR -> ( sin ` y ) e. RR )
627 626 adantl 
 |-  ( ( T. /\ y e. RR ) -> ( sin ` y ) e. RR )
628 620 624 625 625 627 cncfmptssg 
 |-  ( T. -> ( y e. RR |-> ( sin ` y ) ) e. ( RR -cn-> RR ) )
629 628 mptru 
 |-  ( y e. RR |-> ( sin ` y ) ) e. ( RR -cn-> RR )
630 629 a1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( y e. RR |-> ( sin ` y ) ) e. ( RR -cn-> RR ) )
631 602 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. RR )
632 631 568 remulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( r x. ( Q ` ( i + 1 ) ) ) e. RR )
633 fveq2 
 |-  ( y = ( r x. ( Q ` ( i + 1 ) ) ) -> ( sin ` y ) = ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) )
634 630 632 633 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 ) ) ) ) )
635 fveq2 
 |-  ( y = ( r x. x ) -> ( sin ` y ) = ( sin ` ( r x. x ) ) )
636 fveq2 
 |-  ( ( r x. x ) = ( r x. ( Q ` ( i + 1 ) ) ) -> ( sin ` ( r x. x ) ) = ( sin ` ( r x. ( Q ` ( i + 1 ) ) ) ) )
637 636 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 ) ) ) ) )
638 607 610 619 634 635 637 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 ) ) ) )
639 584 585 586 594 598 601 638 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 ) ) ) )
640 570 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 ) ) )
641 11 640 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` i ) ) )
642 641 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` i ) ) )
643 606 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 )
644 567 recnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
645 611 614 615 644 constlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> r e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> r ) limCC ( Q ` i ) ) )
646 614 612 644 idlimc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> x ) limCC ( Q ` i ) ) )
647 611 612 613 595 596 645 646 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 ) ) )
648 631 567 remulcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) -> ( r x. ( Q ` i ) ) e. RR )
649 fveq2 
 |-  ( y = ( r x. ( Q ` i ) ) -> ( sin ` y ) = ( sin ` ( r x. ( Q ` i ) ) ) )
650 630 648 649 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 ) ) ) )
651 fveq2 
 |-  ( ( r x. x ) = ( r x. ( Q ` i ) ) -> ( sin ` ( r x. x ) ) = ( sin ` ( r x. ( Q ` i ) ) ) )
652 651 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 ) ) ) )
653 643 610 647 650 635 652 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 ) ) )
654 584 585 586 594 598 642 653 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 ) ) )
655 567 568 583 639 654 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 )
656 simpll 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( ph /\ r e. RR+ ) )
657 68 adantllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
658 656 657 545 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 )
659 567 568 655 658 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 )
660 552 558 559 560 566 659 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 )
661 546 551 660 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 )
662 519 534 661 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 )
663 505 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> ( 0 ..^ M ) e. Fin )
664 69 adantllr 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
665 520 recnd 
 |-  ( r e. ( n (,) +oo ) -> r e. CC )
666 665 adantl 
 |-  ( ( ph /\ r e. ( n (,) +oo ) ) -> r e. CC )
667 666 ad2antrr 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> r e. CC )
668 406 adantllr 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. CC )
669 667 668 mulcld 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( r x. x ) e. CC )
670 669 sincld 
 |-  ( ( ( ( ph /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( sin ` ( r x. x ) ) e. CC )
671 664 670 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 )
672 671 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 )
673 simplll 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> ph )
674 534 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> r e. RR+ )
675 simpr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
676 673 674 675 659 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 )
677 672 676 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 )
678 663 677 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 )
679 662 678 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ r e. ( n (,) +oo ) ) -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x e. CC )
680 679 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 )
681 680 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 )
682 681 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 )
683 677 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 )
684 663 683 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 )
685 684 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 )
686 685 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 )
687 rpre 
 |-  ( e e. RR+ -> e e. RR )
688 687 ad2antlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ r e. ( n (,) +oo ) ) -> e e. RR )
689 688 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 )
690 662 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 ) )
691 663 677 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 ) )
692 690 691 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 ) )
693 692 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 ) )
694 693 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 ) )
695 505 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 )
696 0zd 
 |-  ( ph -> 0 e. ZZ )
697 4 nnzd 
 |-  ( ph -> M e. ZZ )
698 4 nngt0d 
 |-  ( ph -> 0 < M )
699 fzolb 
 |-  ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
700 696 697 698 699 syl3anbrc 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
701 ne0i 
 |-  ( 0 e. ( 0 ..^ M ) -> ( 0 ..^ M ) =/= (/) )
702 700 701 syl 
 |-  ( ph -> ( 0 ..^ M ) =/= (/) )
703 702 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ r e. ( n (,) +oo ) ) -> ( 0 ..^ M ) =/= (/) )
704 703 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 ) =/= (/) )
705 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 )
706 705 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 )
707 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 )
708 706 707 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 ) )
709 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 ) )
710 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 ) )
711 eleq1w 
 |-  ( i = j -> ( i e. ( 0 ..^ M ) <-> j e. ( 0 ..^ M ) ) )
712 711 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 ) ) ) )
713 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
714 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
715 714 fveq2d 
 |-  ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
716 713 715 oveq12d 
 |-  ( i = j -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) )
717 716 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 )
718 717 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 ) )
719 712 718 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 ) ) )
720 719 677 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 )
721 708 709 710 720 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 )
722 721 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 )
723 352 rpred 
 |-  ( ( ph /\ e e. RR+ ) -> ( e / M ) e. RR )
724 723 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 )
725 724 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 )
726 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 ) )
727 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 ) )
728 727 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 ) )
729 717 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 ) )
730 729 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 ) ) )
731 730 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 ) )
732 728 731 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 ) )
733 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 ) )
734 732 733 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 ) )
735 726 709 710 734 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 ) )
736 695 704 722 725 735 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 ) )
737 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
738 oveq1 
 |-  ( j = i -> ( j + 1 ) = ( i + 1 ) )
739 738 fveq2d 
 |-  ( j = i -> ( Q ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) )
740 737 739 oveq12d 
 |-  ( j = i -> ( ( Q ` j ) [,] ( Q ` ( j + 1 ) ) ) = ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
741 740 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 )
742 741 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 ) )
743 742 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 )
744 743 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 ) )
745 352 rpcnd 
 |-  ( ( ph /\ e e. RR+ ) -> ( e / M ) e. CC )
746 fsumconst 
 |-  ( ( ( 0 ..^ M ) e. Fin /\ ( e / M ) e. CC ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) )
747 505 745 746 sylancr 
 |-  ( ( ph /\ e e. RR+ ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) )
748 4 nnnn0d 
 |-  ( ph -> M e. NN0 )
749 hashfzo0 
 |-  ( M e. NN0 -> ( # ` ( 0 ..^ M ) ) = M )
750 748 749 syl 
 |-  ( ph -> ( # ` ( 0 ..^ M ) ) = M )
751 750 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) = ( M x. ( e / M ) ) )
752 751 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> ( ( # ` ( 0 ..^ M ) ) x. ( e / M ) ) = ( M x. ( e / M ) ) )
753 349 rpcnd 
 |-  ( ( ph /\ e e. RR+ ) -> e e. CC )
754 351 rpcnd 
 |-  ( ( ph /\ e e. RR+ ) -> M e. CC )
755 351 rpne0d 
 |-  ( ( ph /\ e e. RR+ ) -> M =/= 0 )
756 753 754 755 divcan2d 
 |-  ( ( ph /\ e e. RR+ ) -> ( M x. ( e / M ) ) = e )
757 747 752 756 3eqtrd 
 |-  ( ( ph /\ e e. RR+ ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = e )
758 757 adantr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ r e. ( n (,) +oo ) ) -> sum_ j e. ( 0 ..^ M ) ( e / M ) = e )
759 758 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 )
760 736 744 759 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 )
761 682 686 689 694 760 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 )
762 761 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 ) )
763 518 762 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 )
764 763 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 ) ) )
765 764 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 ) ) )
766 515 765 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 ) )
767 512 766 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 )
768 511 767 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 )
769 768 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 ) )
770 769 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 ) )
771 493 770 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 )