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
|
sseldi |
|- ( 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
|
syl5eq |
|- ( 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
|
syl6bb |
|- ( ( 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 ) ) ) |