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 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem87.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem87.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
fourierdlem87.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
fourierdlem87.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem87.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem87.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
fourierdlem87.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
fourierdlem87.g ⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
fourierdlem87.10 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑥 )
fourierdlem87.gibl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 ∈ 𝐿1 )
fourierdlem87.d ⊢ 𝐷 = ( ( 𝑒 / 3 ) / 𝑎 )
fourierdlem87.ch ⊢ ( 𝜒 ↔ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ∧ ∀ 𝑛 ∈ ℕ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐺 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑢 ∈ dom vol ) ∧ ( 𝑢 ⊆ ( - π [,] π ) ∧ ( vol ‘ 𝑢 ) ≤ 𝐷 ) ) ∧ 𝑛 ∈ ℕ ) )
Assertion fourierdlem87 ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ ( - π [,] π ) ∧ ( vol ‘ 𝑢 ) ≤ 𝑑 ) → ∀ 𝑘 ∈ ℕ ( abs ‘ ∫ 𝑢 ( ( 𝑈 ‘ 𝑠 ) · ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑠 ) ) ) d 𝑠 ) < ( 𝑒 / 2 ) ) )

Proof

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 syl5eq ⊢ ( 𝜒 → ( 𝑎 · 𝐷 ) = ( 𝑒 / 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 ) ) )