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