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