Metamath Proof Explorer

Theorem fourierdlem87

Description: The integral of G goes uniformly ( with respect to n ) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem87.f 
|- ( ph -> F : RR --> RR )
fourierdlem87.x 
|- ( ph -> X e. RR )
fourierdlem87.y 
|- ( ph -> Y e. RR )
fourierdlem87.w 
|- ( ph -> W e. RR )
fourierdlem87.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem87.k 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem87.u 
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem87.s 
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
fourierdlem87.g 
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
fourierdlem87.10 
|- ( ph -> E. x e. RR A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ x )
fourierdlem87.gibl 
|- ( ( ph /\ n e. NN ) -> G e. L^1 )
fourierdlem87.d 
|- D = ( ( e / 3 ) / a )
fourierdlem87.ch 
|- ( ch <-> ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) )
Assertion fourierdlem87 
|- ( ( ph /\ e e. RR+ ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem87.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem87.x 
 |-  ( ph -> X e. RR )
3 fourierdlem87.y 
 |-  ( ph -> Y e. RR )
4 fourierdlem87.w 
 |-  ( ph -> W e. RR )
5 fourierdlem87.h 
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
6 fourierdlem87.k 
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
7 fourierdlem87.u 
 |-  U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
8 fourierdlem87.s 
 |-  S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
9 fourierdlem87.g 
 |-  G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
10 fourierdlem87.10 
 |-  ( ph -> E. x e. RR A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ x )
11 fourierdlem87.gibl 
 |-  ( ( ph /\ n e. NN ) -> G e. L^1 )
12 fourierdlem87.d 
 |-  D = ( ( e / 3 ) / a )
13 fourierdlem87.ch 
 |-  ( ch <-> ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) )
14 1 2 3 4 5 6 7 10 fourierdlem77 
 |-  ( ph -> E. a e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a )
15 nfv 
 |-  F/ s ( ph /\ a e. RR+ )
16 nfra1 
 |-  F/ s A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a
17 15 16 nfan 
 |-  F/ s ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a )
18 nfv 
 |-  F/ s n e. NN
19 17 18 nfan 
 |-  F/ s ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN )
20 simp-4l 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ph )
21 simp-4r 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> a e. RR+ )
22 simplr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> n e. NN )
23 20 21 22 jca31 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( ph /\ a e. RR+ ) /\ n e. NN ) )
24 simpr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( -u _pi [,] _pi ) )
25 simpllr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a )
26 rspa 
 |-  ( ( A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) <_ a )
27 25 24 26 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) <_ a )
28 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( -u _pi [,] _pi ) )
29 1 2 3 4 5 6 7 fourierdlem55 
 |-  ( ph -> U : ( -u _pi [,] _pi ) --> RR )
30 29 ffvelrnda 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) e. RR )
31 30 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) e. RR )
32 nnre 
 |-  ( n e. NN -> n e. RR )
33 8 fourierdlem5 
 |-  ( n e. RR -> S : ( -u _pi [,] _pi ) --> RR )
34 32 33 syl 
 |-  ( n e. NN -> S : ( -u _pi [,] _pi ) --> RR )
35 34 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> S : ( -u _pi [,] _pi ) --> RR )
36 35 28 ffvelrnd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( S ` s ) e. RR )
37 31 36 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( U ` s ) x. ( S ` s ) ) e. RR )
38 9 fvmpt2 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ ( ( U ` s ) x. ( S ` s ) ) e. RR ) -> ( G ` s ) = ( ( U ` s ) x. ( S ` s ) ) )
39 28 37 38 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( G ` s ) = ( ( U ` s ) x. ( S ` s ) ) )
40 simpr 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( -u _pi [,] _pi ) )
41 halfre 
 |-  ( 1 / 2 ) e. RR
42 41 a1i 
 |-  ( n e. NN -> ( 1 / 2 ) e. RR )
43 32 42 readdcld 
 |-  ( n e. NN -> ( n + ( 1 / 2 ) ) e. RR )
44 43 adantr 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> ( n + ( 1 / 2 ) ) e. RR )
45 pire 
 |-  _pi e. RR
46 45 renegcli 
 |-  -u _pi e. RR
47 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
48 46 45 47 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
49 48 sseli 
 |-  ( s e. ( -u _pi [,] _pi ) -> s e. RR )
50 49 adantl 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> s e. RR )
51 44 50 remulcld 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> ( ( n + ( 1 / 2 ) ) x. s ) e. RR )
52 51 resincld 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) e. RR )
53 8 fvmpt2 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) e. RR ) -> ( S ` s ) = ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
54 40 52 53 syl2anc 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> ( S ` s ) = ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
55 54 oveq2d 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> ( ( U ` s ) x. ( S ` s ) ) = ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) )
56 55 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( U ` s ) x. ( S ` s ) ) = ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) )
57 39 56 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( G ` s ) = ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) )
58 57 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( G ` s ) ) = ( abs ` ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) )
59 31 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) e. CC )
60 52 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) e. RR )
61 60 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) e. CC )
62 59 61 absmuld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) = ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) )
63 58 62 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( G ` s ) ) = ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) )
64 63 adantllr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( G ` s ) ) = ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) )
65 64 adantr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> ( abs ` ( G ` s ) ) = ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) )
66 59 abscld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) e. RR )
67 61 abscld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) e. RR )
68 66 67 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) e. RR )
69 68 adantllr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) e. RR )
70 69 adantr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) e. RR )
71 66 adantllr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) e. RR )
72 71 adantr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> ( abs ` ( U ` s ) ) e. RR )
73 rpre 
 |-  ( a e. RR+ -> a e. RR )
74 73 ad4antlr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> a e. RR )
75 1red 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> 1 e. RR )
76 59 absge0d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> 0 <_ ( abs ` ( U ` s ) ) )
77 51 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( n + ( 1 / 2 ) ) x. s ) e. RR )
78 abssinbd 
 |-  ( ( ( n + ( 1 / 2 ) ) x. s ) e. RR -> ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) <_ 1 )
79 77 78 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) <_ 1 )
80 67 75 66 76 79 lemul2ad 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) <_ ( ( abs ` ( U ` s ) ) x. 1 ) )
81 66 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) e. CC )
82 81 mulid1d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( U ` s ) ) x. 1 ) = ( abs ` ( U ` s ) ) )
83 80 82 breqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) <_ ( abs ` ( U ` s ) ) )
84 83 adantllr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) <_ ( abs ` ( U ` s ) ) )
85 84 adantr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) <_ ( abs ` ( U ` s ) ) )
86 simpr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> ( abs ` ( U ` s ) ) <_ a )
87 70 72 74 85 86 letrd 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> ( ( abs ` ( U ` s ) ) x. ( abs ` ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) ) <_ a )
88 65 87 eqbrtrd 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( U ` s ) ) <_ a ) -> ( abs ` ( G ` s ) ) <_ a )
89 23 24 27 88 syl21anc 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( G ` s ) ) <_ a )
90 89 ex 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) -> ( s e. ( -u _pi [,] _pi ) -> ( abs ` ( G ` s ) ) <_ a ) )
91 19 90 ralrimi 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) /\ n e. NN ) -> A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
92 91 ralrimiva 
 |-  ( ( ( ph /\ a e. RR+ ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a ) -> A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
93 92 ex 
 |-  ( ( ph /\ a e. RR+ ) -> ( A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a -> A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) )
94 93 reximdva 
 |-  ( ph -> ( E. a e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ a -> E. a e. RR+ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) )
95 14 94 mpd 
 |-  ( ph -> E. a e. RR+ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
96 95 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> E. a e. RR+ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
97 id 
 |-  ( e e. RR+ -> e e. RR+ )
98 3rp 
 |-  3 e. RR+
99 98 a1i 
 |-  ( e e. RR+ -> 3 e. RR+ )
100 97 99 rpdivcld 
 |-  ( e e. RR+ -> ( e / 3 ) e. RR+ )
101 100 adantr 
 |-  ( ( e e. RR+ /\ a e. RR+ ) -> ( e / 3 ) e. RR+ )
102 simpr 
 |-  ( ( e e. RR+ /\ a e. RR+ ) -> a e. RR+ )
103 101 102 rpdivcld 
 |-  ( ( e e. RR+ /\ a e. RR+ ) -> ( ( e / 3 ) / a ) e. RR+ )
104 12 103 eqeltrid 
 |-  ( ( e e. RR+ /\ a e. RR+ ) -> D e. RR+ )
105 104 adantll 
 |-  ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ ) -> D e. RR+ )
106 105 3adant3 
 |-  ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) -> D e. RR+ )
107 nfv 
 |-  F/ n ( ph /\ e e. RR+ )
108 nfv 
 |-  F/ n a e. RR+
109 nfra1 
 |-  F/ n A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a
110 107 108 109 nf3an 
 |-  F/ n ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
111 nfv 
 |-  F/ n u e. dom vol
112 110 111 nfan 
 |-  F/ n ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol )
113 nfv 
 |-  F/ n ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D )
114 112 113 nfan 
 |-  F/ n ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) )
115 simpl1l 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) -> ph )
116 115 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> ph )
117 13 116 sylbi 
 |-  ( ch -> ph )
118 117 1 syl 
 |-  ( ch -> F : RR --> RR )
119 117 2 syl 
 |-  ( ch -> X e. RR )
120 117 3 syl 
 |-  ( ch -> Y e. RR )
121 117 4 syl 
 |-  ( ch -> W e. RR )
122 32 adantl 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> n e. RR )
123 13 122 sylbi 
 |-  ( ch -> n e. RR )
124 118 119 120 121 5 6 7 123 8 9 fourierdlem67 
 |-  ( ch -> G : ( -u _pi [,] _pi ) --> RR )
125 124 adantr 
 |-  ( ( ch /\ s e. u ) -> G : ( -u _pi [,] _pi ) --> RR )
126 simplrl 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> u C_ ( -u _pi [,] _pi ) )
127 13 126 sylbi 
 |-  ( ch -> u C_ ( -u _pi [,] _pi ) )
128 127 sselda 
 |-  ( ( ch /\ s e. u ) -> s e. ( -u _pi [,] _pi ) )
129 125 128 ffvelrnd 
 |-  ( ( ch /\ s e. u ) -> ( G ` s ) e. RR )
130 simpllr 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> u e. dom vol )
131 13 130 sylbi 
 |-  ( ch -> u e. dom vol )
132 124 ffvelrnda 
 |-  ( ( ch /\ s e. ( -u _pi [,] _pi ) ) -> ( G ` s ) e. RR )
133 124 feqmptd 
 |-  ( ch -> G = ( s e. ( -u _pi [,] _pi ) |-> ( G ` s ) ) )
134 13 simprbi 
 |-  ( ch -> n e. NN )
135 117 134 11 syl2anc 
 |-  ( ch -> G e. L^1 )
136 133 135 eqeltrrd 
 |-  ( ch -> ( s e. ( -u _pi [,] _pi ) |-> ( G ` s ) ) e. L^1 )
137 127 131 132 136 iblss 
 |-  ( ch -> ( s e. u |-> ( G ` s ) ) e. L^1 )
138 129 137 itgcl 
 |-  ( ch -> S. u ( G ` s ) _d s e. CC )
139 138 abscld 
 |-  ( ch -> ( abs ` S. u ( G ` s ) _d s ) e. RR )
140 129 recnd 
 |-  ( ( ch /\ s e. u ) -> ( G ` s ) e. CC )
141 140 abscld 
 |-  ( ( ch /\ s e. u ) -> ( abs ` ( G ` s ) ) e. RR )
142 129 137 iblabs 
 |-  ( ch -> ( s e. u |-> ( abs ` ( G ` s ) ) ) e. L^1 )
143 141 142 itgrecl 
 |-  ( ch -> S. u ( abs ` ( G ` s ) ) _d s e. RR )
144 simpl1r 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) -> e e. RR+ )
145 144 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> e e. RR+ )
146 13 145 sylbi 
 |-  ( ch -> e e. RR+ )
147 146 rpred 
 |-  ( ch -> e e. RR )
148 147 rehalfcld 
 |-  ( ch -> ( e / 2 ) e. RR )
149 129 137 itgabs 
 |-  ( ch -> ( abs ` S. u ( G ` s ) _d s ) <_ S. u ( abs ` ( G ` s ) ) _d s )
150 simpl2 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) -> a e. RR+ )
151 150 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> a e. RR+ )
152 13 151 sylbi 
 |-  ( ch -> a e. RR+ )
153 152 rpred 
 |-  ( ch -> a e. RR )
154 153 adantr 
 |-  ( ( ch /\ s e. u ) -> a e. RR )
155 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
156 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
157 156 a1i 
 |-  ( ch -> vol : dom vol --> ( 0 [,] +oo ) )
158 157 131 ffvelrnd 
 |-  ( ch -> ( vol ` u ) e. ( 0 [,] +oo ) )
159 155 158 sselid 
 |-  ( ch -> ( vol ` u ) e. RR* )
160 iccvolcl 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( vol ` ( -u _pi [,] _pi ) ) e. RR )
161 46 45 160 mp2an 
 |-  ( vol ` ( -u _pi [,] _pi ) ) e. RR
162 161 a1i 
 |-  ( ch -> ( vol ` ( -u _pi [,] _pi ) ) e. RR )
163 mnfxr 
 |-  -oo e. RR*
164 163 a1i 
 |-  ( ch -> -oo e. RR* )
165 0xr 
 |-  0 e. RR*
166 165 a1i 
 |-  ( ch -> 0 e. RR* )
167 mnflt0 
 |-  -oo < 0
168 167 a1i 
 |-  ( ch -> -oo < 0 )
169 volge0 
 |-  ( u e. dom vol -> 0 <_ ( vol ` u ) )
170 131 169 syl 
 |-  ( ch -> 0 <_ ( vol ` u ) )
171 164 166 159 168 170 xrltletrd 
 |-  ( ch -> -oo < ( vol ` u ) )
172 iccmbl 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) e. dom vol )
173 46 45 172 mp2an 
 |-  ( -u _pi [,] _pi ) e. dom vol
174 173 a1i 
 |-  ( ch -> ( -u _pi [,] _pi ) e. dom vol )
175 volss 
 |-  ( ( u e. dom vol /\ ( -u _pi [,] _pi ) e. dom vol /\ u C_ ( -u _pi [,] _pi ) ) -> ( vol ` u ) <_ ( vol ` ( -u _pi [,] _pi ) ) )
176 131 174 127 175 syl3anc 
 |-  ( ch -> ( vol ` u ) <_ ( vol ` ( -u _pi [,] _pi ) ) )
177 xrre 
 |-  ( ( ( ( vol ` u ) e. RR* /\ ( vol ` ( -u _pi [,] _pi ) ) e. RR ) /\ ( -oo < ( vol ` u ) /\ ( vol ` u ) <_ ( vol ` ( -u _pi [,] _pi ) ) ) ) -> ( vol ` u ) e. RR )
178 159 162 171 176 177 syl22anc 
 |-  ( ch -> ( vol ` u ) e. RR )
179 152 rpcnd 
 |-  ( ch -> a e. CC )
180 iblconstmpt 
 |-  ( ( u e. dom vol /\ ( vol ` u ) e. RR /\ a e. CC ) -> ( s e. u |-> a ) e. L^1 )
181 131 178 179 180 syl3anc 
 |-  ( ch -> ( s e. u |-> a ) e. L^1 )
182 154 181 itgrecl 
 |-  ( ch -> S. u a _d s e. RR )
183 simpl3 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) -> A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
184 183 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
185 13 184 sylbi 
 |-  ( ch -> A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
186 rspa 
 |-  ( ( A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a /\ n e. NN ) -> A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
187 185 134 186 syl2anc 
 |-  ( ch -> A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
188 187 adantr 
 |-  ( ( ch /\ s e. u ) -> A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a )
189 rspa 
 |-  ( ( A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( G ` s ) ) <_ a )
190 188 128 189 syl2anc 
 |-  ( ( ch /\ s e. u ) -> ( abs ` ( G ` s ) ) <_ a )
191 142 181 141 154 190 itgle 
 |-  ( ch -> S. u ( abs ` ( G ` s ) ) _d s <_ S. u a _d s )
192 itgconst 
 |-  ( ( u e. dom vol /\ ( vol ` u ) e. RR /\ a e. CC ) -> S. u a _d s = ( a x. ( vol ` u ) ) )
193 131 178 179 192 syl3anc 
 |-  ( ch -> S. u a _d s = ( a x. ( vol ` u ) ) )
194 153 178 remulcld 
 |-  ( ch -> ( a x. ( vol ` u ) ) e. RR )
195 3re 
 |-  3 e. RR
196 195 a1i 
 |-  ( ch -> 3 e. RR )
197 3ne0 
 |-  3 =/= 0
198 197 a1i 
 |-  ( ch -> 3 =/= 0 )
199 147 196 198 redivcld 
 |-  ( ch -> ( e / 3 ) e. RR )
200 152 rpne0d 
 |-  ( ch -> a =/= 0 )
201 199 153 200 redivcld 
 |-  ( ch -> ( ( e / 3 ) / a ) e. RR )
202 12 201 eqeltrid 
 |-  ( ch -> D e. RR )
203 153 202 remulcld 
 |-  ( ch -> ( a x. D ) e. RR )
204 152 rpge0d 
 |-  ( ch -> 0 <_ a )
205 simplrr 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> ( vol ` u ) <_ D )
206 13 205 sylbi 
 |-  ( ch -> ( vol ` u ) <_ D )
207 178 202 153 204 206 lemul2ad 
 |-  ( ch -> ( a x. ( vol ` u ) ) <_ ( a x. D ) )
208 12 oveq2i 
 |-  ( a x. D ) = ( a x. ( ( e / 3 ) / a ) )
209 199 recnd 
 |-  ( ch -> ( e / 3 ) e. CC )
210 209 179 200 divcan2d 
 |-  ( ch -> ( a x. ( ( e / 3 ) / a ) ) = ( e / 3 ) )
211 208 210 eqtrid 
 |-  ( ch -> ( a x. D ) = ( e / 3 ) )
212 2rp 
 |-  2 e. RR+
213 212 a1i 
 |-  ( ch -> 2 e. RR+ )
214 98 a1i 
 |-  ( ch -> 3 e. RR+ )
215 2lt3 
 |-  2 < 3
216 215 a1i 
 |-  ( ch -> 2 < 3 )
217 213 214 146 216 ltdiv2dd 
 |-  ( ch -> ( e / 3 ) < ( e / 2 ) )
218 211 217 eqbrtrd 
 |-  ( ch -> ( a x. D ) < ( e / 2 ) )
219 194 203 148 207 218 lelttrd 
 |-  ( ch -> ( a x. ( vol ` u ) ) < ( e / 2 ) )
220 193 219 eqbrtrd 
 |-  ( ch -> S. u a _d s < ( e / 2 ) )
221 143 182 148 191 220 lelttrd 
 |-  ( ch -> S. u ( abs ` ( G ` s ) ) _d s < ( e / 2 ) )
222 139 143 148 149 221 lelttrd 
 |-  ( ch -> ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) )
223 13 222 sylbir 
 |-  ( ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) -> ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) )
224 223 ex 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) -> ( n e. NN -> ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) )
225 114 224 ralrimi 
 |-  ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) )
226 225 ex 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) -> ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) )
227 226 ralrimiva 
 |-  ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) -> A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) )
228 breq2 
 |-  ( d = D -> ( ( vol ` u ) <_ d <-> ( vol ` u ) <_ D ) )
229 228 anbi2d 
 |-  ( d = D -> ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) <-> ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) ) )
230 229 rspceaimv 
 |-  ( ( D e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ D ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) )
231 106 227 230 syl2anc 
 |-  ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) )
232 231 rexlimdv3a 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. a e. RR+ A. n e. NN A. s e. ( -u _pi [,] _pi ) ( abs ` ( G ` s ) ) <_ a -> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) ) )
233 96 232 mpd 
 |-  ( ( ph /\ e e. RR+ ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) )
234 simplll 
 |-  ( ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) /\ s e. u ) -> ph )
235 simplr 
 |-  ( ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) /\ s e. u ) -> n e. NN )
236 simpllr 
 |-  ( ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) /\ s e. u ) -> u C_ ( -u _pi [,] _pi ) )
237 simpr 
 |-  ( ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) /\ s e. u ) -> s e. u )
238 236 237 sseldd 
 |-  ( ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) /\ s e. u ) -> s e. ( -u _pi [,] _pi ) )
239 234 235 238 57 syl21anc 
 |-  ( ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) /\ s e. u ) -> ( G ` s ) = ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) )
240 239 itgeq2dv 
 |-  ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) -> S. u ( G ` s ) _d s = S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s )
241 240 fveq2d 
 |-  ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) -> ( abs ` S. u ( G ` s ) _d s ) = ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s ) )
242 241 breq1d 
 |-  ( ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) /\ n e. NN ) -> ( ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) <-> ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
243 242 ralbidva 
 |-  ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) -> ( A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) <-> A. n e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
244 oveq1 
 |-  ( n = k -> ( n + ( 1 / 2 ) ) = ( k + ( 1 / 2 ) ) )
245 244 oveq1d 
 |-  ( n = k -> ( ( n + ( 1 / 2 ) ) x. s ) = ( ( k + ( 1 / 2 ) ) x. s ) )
246 245 fveq2d 
 |-  ( n = k -> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) )
247 246 oveq2d 
 |-  ( n = k -> ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) = ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) )
248 247 adantr 
 |-  ( ( n = k /\ s e. u ) -> ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) = ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) )
249 248 itgeq2dv 
 |-  ( n = k -> S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s = S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s )
250 249 fveq2d 
 |-  ( n = k -> ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s ) = ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) )
251 250 breq1d 
 |-  ( n = k -> ( ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) <-> ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
252 251 cbvralvw 
 |-  ( A. n e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) <-> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) )
253 243 252 bitrdi 
 |-  ( ( ph /\ u C_ ( -u _pi [,] _pi ) ) -> ( A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) <-> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
254 253 adantrr 
 |-  ( ( ph /\ ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) ) -> ( A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) <-> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
255 254 pm5.74da 
 |-  ( ph -> ( ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) <-> ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) )
256 255 rexralbidv 
 |-  ( ph -> ( E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) <-> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) )
257 256 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. n e. NN ( abs ` S. u ( G ` s ) _d s ) < ( e / 2 ) ) <-> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) )
258 233 257 mpbid 
 |-  ( ( ph /\ e e. RR+ ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )