Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem87 Structured version   Visualization version   GIF version

Theorem fourierdlem87 41204
 Description: The integral of 𝐺 goes uniformly ( with respect to 𝑛) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
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
Ref Expression
fourierdlem87 ((𝜑𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)))
Distinct variable groups:   𝐷,𝑑,𝑛,𝑢   𝐺,𝑎,𝑑,𝑠,𝑢   𝐾,𝑎,𝑠   𝑈,𝑎,𝑛   𝑈,𝑘,𝑛   𝑥,𝑈,𝑎   𝑒,𝑎,𝑑,𝑛,𝑢   𝜑,𝑎,𝑑,𝑛,𝑠,𝑢   𝜒,𝑠   𝑒,𝑘,𝑢   𝑘,𝑠   𝜑,𝑥,𝑠
Allowed substitution hints:   𝜑(𝑒,𝑘)   𝜒(𝑥,𝑢,𝑒,𝑘,𝑛,𝑎,𝑑)   𝐷(𝑥,𝑒,𝑘,𝑠,𝑎)   𝑆(𝑥,𝑢,𝑒,𝑘,𝑛,𝑠,𝑎,𝑑)   𝑈(𝑢,𝑒,𝑠,𝑑)   𝐹(𝑥,𝑢,𝑒,𝑘,𝑛,𝑠,𝑎,𝑑)   𝐺(𝑥,𝑒,𝑘,𝑛)   𝐻(𝑥,𝑢,𝑒,𝑘,𝑛,𝑠,𝑎,𝑑)   𝐾(𝑥,𝑢,𝑒,𝑘,𝑛,𝑑)   𝑊(𝑥,𝑢,𝑒,𝑘,𝑛,𝑠,𝑎,𝑑)   𝑋(𝑥,𝑢,𝑒,𝑘,𝑛,𝑠,𝑎,𝑑)   𝑌(𝑥,𝑢,𝑒,𝑘,𝑛,𝑠,𝑎,𝑑)

Proof of Theorem fourierdlem87
StepHypRef Expression
1 fourierdlem87.f . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
2 fourierdlem87.x . . . . . 6 (𝜑𝑋 ∈ ℝ)
3 fourierdlem87.y . . . . . 6 (𝜑𝑌 ∈ ℝ)
4 fourierdlem87.w . . . . . 6 (𝜑𝑊 ∈ ℝ)
5 fourierdlem87.h . . . . . 6 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6 fourierdlem87.k . . . . . 6 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
7 fourierdlem87.u . . . . . 6 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻𝑠) · (𝐾𝑠)))
8 fourierdlem87.10 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐻𝑠)) ≤ 𝑥)
91, 2, 3, 4, 5, 6, 7, 8fourierdlem77 41194 . . . . 5 (𝜑 → ∃𝑎 ∈ ℝ+𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎)
10 nfv 2015 . . . . . . . . . . 11 𝑠(𝜑𝑎 ∈ ℝ+)
11 nfra1 3150 . . . . . . . . . . 11 𝑠𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎
1210, 11nfan 2004 . . . . . . . . . 10 𝑠((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎)
13 nfv 2015 . . . . . . . . . 10 𝑠 𝑛 ∈ ℕ
1412, 13nfan 2004 . . . . . . . . 9 𝑠(((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ)
15 simp-4l 803 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 𝜑)
16 simp-4r 805 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 𝑎 ∈ ℝ+)
17 simplr 787 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 𝑛 ∈ ℕ)
1815, 16, 17jca31 512 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ))
19 simpr 479 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (-π[,]π))
20 simpllr 795 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎)
21 rspa 3139 . . . . . . . . . . . 12 ((∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎𝑠 ∈ (-π[,]π)) → (abs‘(𝑈𝑠)) ≤ 𝑎)
2220, 19, 21syl2anc 581 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝑈𝑠)) ≤ 𝑎)
23 simpr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (-π[,]π))
241, 2, 3, 4, 5, 6, 7fourierdlem55 41172 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:(-π[,]π)⟶ℝ)
2524ffvelrnda 6608 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑠 ∈ (-π[,]π)) → (𝑈𝑠) ∈ ℝ)
2625adantlr 708 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (𝑈𝑠) ∈ ℝ)
27 nnre 11358 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
28 fourierdlem87.s . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠)))
2928fourierdlem5 41123 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℝ → 𝑆:(-π[,]π)⟶ℝ)
3027, 29syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑆:(-π[,]π)⟶ℝ)
3130ad2antlr 720 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 𝑆:(-π[,]π)⟶ℝ)
3231, 23ffvelrnd 6609 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (𝑆𝑠) ∈ ℝ)
3326, 32remulcld 10387 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((𝑈𝑠) · (𝑆𝑠)) ∈ ℝ)
34 fourierdlem87.g . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠)))
3534fvmpt2 6538 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π[,]π) ∧ ((𝑈𝑠) · (𝑆𝑠)) ∈ ℝ) → (𝐺𝑠) = ((𝑈𝑠) · (𝑆𝑠)))
3623, 33, 35syl2anc 581 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (𝐺𝑠) = ((𝑈𝑠) · (𝑆𝑠)))
37 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (-π[,]π))
38 halfre 11572 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 / 2) ∈ ℝ
3938a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → (1 / 2) ∈ ℝ)
4027, 39readdcld 10386 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ → (𝑛 + (1 / 2)) ∈ ℝ)
4140adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) → (𝑛 + (1 / 2)) ∈ ℝ)
42 pire 24610 . . . . . . . . . . . . . . . . . . . . . . . . . 26 π ∈ ℝ
4342renegcli 10663 . . . . . . . . . . . . . . . . . . . . . . . . 25 -π ∈ ℝ
44 iccssre 12543 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
4543, 42, 44mp2an 685 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π[,]π) ⊆ ℝ
4645sseli 3823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (-π[,]π) → 𝑠 ∈ ℝ)
4746adantl 475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ℝ)
4841, 47remulcld 10387 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) → ((𝑛 + (1 / 2)) · 𝑠) ∈ ℝ)
4948resincld 15245 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℝ)
5028fvmpt2 6538 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π[,]π) ∧ (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℝ) → (𝑆𝑠) = (sin‘((𝑛 + (1 / 2)) · 𝑠)))
5137, 49, 50syl2anc 581 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) → (𝑆𝑠) = (sin‘((𝑛 + (1 / 2)) · 𝑠)))
5251oveq2d 6921 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) → ((𝑈𝑠) · (𝑆𝑠)) = ((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))))
5352adantll 707 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((𝑈𝑠) · (𝑆𝑠)) = ((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))))
5436, 53eqtrd 2861 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (𝐺𝑠) = ((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))))
5554fveq2d 6437 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝐺𝑠)) = (abs‘((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠)))))
5626recnd 10385 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (𝑈𝑠) ∈ ℂ)
5749adantll 707 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℝ)
5857recnd 10385 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℂ)
5956, 58absmuld 14570 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠)))) = ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))))
6055, 59eqtrd 2861 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝐺𝑠)) = ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))))
6160adantllr 712 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝐺𝑠)) = ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))))
6261adantr 474 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → (abs‘(𝐺𝑠)) = ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))))
6356abscld 14552 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝑈𝑠)) ∈ ℝ)
6458abscld 14552 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠))) ∈ ℝ)
6563, 64remulcld 10387 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ∈ ℝ)
6665adantllr 712 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ∈ ℝ)
6766adantr 474 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ∈ ℝ)
6863adantllr 712 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝑈𝑠)) ∈ ℝ)
6968adantr 474 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → (abs‘(𝑈𝑠)) ∈ ℝ)
70 rpre 12120 . . . . . . . . . . . . . 14 (𝑎 ∈ ℝ+𝑎 ∈ ℝ)
7170ad4antlr 728 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → 𝑎 ∈ ℝ)
72 1red 10357 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 1 ∈ ℝ)
7356absge0d 14560 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → 0 ≤ (abs‘(𝑈𝑠)))
7448adantll 707 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((𝑛 + (1 / 2)) · 𝑠) ∈ ℝ)
75 abssinbd 40307 . . . . . . . . . . . . . . . . . 18 (((𝑛 + (1 / 2)) · 𝑠) ∈ ℝ → (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠))) ≤ 1)
7674, 75syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠))) ≤ 1)
7764, 72, 63, 73, 76lemul2ad 11294 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ≤ ((abs‘(𝑈𝑠)) · 1))
7863recnd 10385 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝑈𝑠)) ∈ ℂ)
7978mulid1d 10374 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((abs‘(𝑈𝑠)) · 1) = (abs‘(𝑈𝑠)))
8077, 79breqtrd 4899 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ≤ (abs‘(𝑈𝑠)))
8180adantllr 712 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ≤ (abs‘(𝑈𝑠)))
8281adantr 474 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ≤ (abs‘(𝑈𝑠)))
83 simpr 479 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → (abs‘(𝑈𝑠)) ≤ 𝑎)
8467, 69, 71, 82, 83letrd 10513 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → ((abs‘(𝑈𝑠)) · (abs‘(sin‘((𝑛 + (1 / 2)) · 𝑠)))) ≤ 𝑎)
8562, 84eqbrtrd 4895 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) ∧ (abs‘(𝑈𝑠)) ≤ 𝑎) → (abs‘(𝐺𝑠)) ≤ 𝑎)
8618, 19, 22, 85syl21anc 873 . . . . . . . . . 10 (((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (abs‘(𝐺𝑠)) ≤ 𝑎)
8786ex 403 . . . . . . . . 9 ((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ (-π[,]π) → (abs‘(𝐺𝑠)) ≤ 𝑎))
8814, 87ralrimi 3166 . . . . . . . 8 ((((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) ∧ 𝑛 ∈ ℕ) → ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
8988ralrimiva 3175 . . . . . . 7 (((𝜑𝑎 ∈ ℝ+) ∧ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎) → ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
9089ex 403 . . . . . 6 ((𝜑𝑎 ∈ ℝ+) → (∀𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎 → ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎))
9190reximdva 3225 . . . . 5 (𝜑 → (∃𝑎 ∈ ℝ+𝑠 ∈ (-π[,]π)(abs‘(𝑈𝑠)) ≤ 𝑎 → ∃𝑎 ∈ ℝ+𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎))
929, 91mpd 15 . . . 4 (𝜑 → ∃𝑎 ∈ ℝ+𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
9392adantr 474 . . 3 ((𝜑𝑒 ∈ ℝ+) → ∃𝑎 ∈ ℝ+𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
94 fourierdlem87.d . . . . . . . 8 𝐷 = ((𝑒 / 3) / 𝑎)
95 id 22 . . . . . . . . . . 11 (𝑒 ∈ ℝ+𝑒 ∈ ℝ+)
96 3rp 12118 . . . . . . . . . . . 12 3 ∈ ℝ+
9796a1i 11 . . . . . . . . . . 11 (𝑒 ∈ ℝ+ → 3 ∈ ℝ+)
9895, 97rpdivcld 12173 . . . . . . . . . 10 (𝑒 ∈ ℝ+ → (𝑒 / 3) ∈ ℝ+)
9998adantr 474 . . . . . . . . 9 ((𝑒 ∈ ℝ+𝑎 ∈ ℝ+) → (𝑒 / 3) ∈ ℝ+)
100 simpr 479 . . . . . . . . 9 ((𝑒 ∈ ℝ+𝑎 ∈ ℝ+) → 𝑎 ∈ ℝ+)
10199, 100rpdivcld 12173 . . . . . . . 8 ((𝑒 ∈ ℝ+𝑎 ∈ ℝ+) → ((𝑒 / 3) / 𝑎) ∈ ℝ+)
10294, 101syl5eqel 2910 . . . . . . 7 ((𝑒 ∈ ℝ+𝑎 ∈ ℝ+) → 𝐷 ∈ ℝ+)
103102adantll 707 . . . . . 6 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+) → 𝐷 ∈ ℝ+)
1041033adant3 1168 . . . . 5 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) → 𝐷 ∈ ℝ+)
105 nfv 2015 . . . . . . . . . . 11 𝑛(𝜑𝑒 ∈ ℝ+)
106 nfv 2015 . . . . . . . . . . 11 𝑛 𝑎 ∈ ℝ+
107 nfra1 3150 . . . . . . . . . . 11 𝑛𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎
108105, 106, 107nf3an 2006 . . . . . . . . . 10 𝑛((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
109 nfv 2015 . . . . . . . . . 10 𝑛 𝑢 ∈ dom vol
110108, 109nfan 2004 . . . . . . . . 9 𝑛(((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol)
111 nfv 2015 . . . . . . . . 9 𝑛(𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)
112110, 111nfan 2004 . . . . . . . 8 𝑛((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷))
113 fourierdlem87.ch . . . . . . . . . 10 (𝜒 ↔ (((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ))
114 simpl1l 1299 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) → 𝜑)
115114ad2antrr 719 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → 𝜑)
116113, 115sylbi 209 . . . . . . . . . . . . . . . . 17 (𝜒𝜑)
117116, 1syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝐹:ℝ⟶ℝ)
118116, 2syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑋 ∈ ℝ)
119116, 3syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑌 ∈ ℝ)
120116, 4syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑊 ∈ ℝ)
12127adantl 475 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
122113, 121sylbi 209 . . . . . . . . . . . . . . . 16 (𝜒𝑛 ∈ ℝ)
123117, 118, 119, 120, 5, 6, 7, 122, 28, 34fourierdlem67 41184 . . . . . . . . . . . . . . 15 (𝜒𝐺:(-π[,]π)⟶ℝ)
124123adantr 474 . . . . . . . . . . . . . 14 ((𝜒𝑠𝑢) → 𝐺:(-π[,]π)⟶ℝ)
125 simplrl 797 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → 𝑢 ⊆ (-π[,]π))
126113, 125sylbi 209 . . . . . . . . . . . . . . 15 (𝜒𝑢 ⊆ (-π[,]π))
127126sselda 3827 . . . . . . . . . . . . . 14 ((𝜒𝑠𝑢) → 𝑠 ∈ (-π[,]π))
128124, 127ffvelrnd 6609 . . . . . . . . . . . . 13 ((𝜒𝑠𝑢) → (𝐺𝑠) ∈ ℝ)
129 simpllr 795 . . . . . . . . . . . . . . 15 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → 𝑢 ∈ dom vol)
130113, 129sylbi 209 . . . . . . . . . . . . . 14 (𝜒𝑢 ∈ dom vol)
131123ffvelrnda 6608 . . . . . . . . . . . . . 14 ((𝜒𝑠 ∈ (-π[,]π)) → (𝐺𝑠) ∈ ℝ)
132123feqmptd 6496 . . . . . . . . . . . . . . 15 (𝜒𝐺 = (𝑠 ∈ (-π[,]π) ↦ (𝐺𝑠)))
133113simprbi 492 . . . . . . . . . . . . . . . 16 (𝜒𝑛 ∈ ℕ)
134 fourierdlem87.gibl . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐺 ∈ 𝐿1)
135116, 133, 134syl2anc 581 . . . . . . . . . . . . . . 15 (𝜒𝐺 ∈ 𝐿1)
136132, 135eqeltrrd 2907 . . . . . . . . . . . . . 14 (𝜒 → (𝑠 ∈ (-π[,]π) ↦ (𝐺𝑠)) ∈ 𝐿1)
137126, 130, 131, 136iblss 23970 . . . . . . . . . . . . 13 (𝜒 → (𝑠𝑢 ↦ (𝐺𝑠)) ∈ 𝐿1)
138128, 137itgcl 23949 . . . . . . . . . . . 12 (𝜒 → ∫𝑢(𝐺𝑠) d𝑠 ∈ ℂ)
139138abscld 14552 . . . . . . . . . . 11 (𝜒 → (abs‘∫𝑢(𝐺𝑠) d𝑠) ∈ ℝ)
140128recnd 10385 . . . . . . . . . . . . 13 ((𝜒𝑠𝑢) → (𝐺𝑠) ∈ ℂ)
141140abscld 14552 . . . . . . . . . . . 12 ((𝜒𝑠𝑢) → (abs‘(𝐺𝑠)) ∈ ℝ)
142128, 137iblabs 23994 . . . . . . . . . . . 12 (𝜒 → (𝑠𝑢 ↦ (abs‘(𝐺𝑠))) ∈ 𝐿1)
143141, 142itgrecl 23963 . . . . . . . . . . 11 (𝜒 → ∫𝑢(abs‘(𝐺𝑠)) d𝑠 ∈ ℝ)
144 simpl1r 1301 . . . . . . . . . . . . . . 15 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) → 𝑒 ∈ ℝ+)
145144ad2antrr 719 . . . . . . . . . . . . . 14 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → 𝑒 ∈ ℝ+)
146113, 145sylbi 209 . . . . . . . . . . . . 13 (𝜒𝑒 ∈ ℝ+)
147146rpred 12156 . . . . . . . . . . . 12 (𝜒𝑒 ∈ ℝ)
148147rehalfcld 11605 . . . . . . . . . . 11 (𝜒 → (𝑒 / 2) ∈ ℝ)
149128, 137itgabs 24000 . . . . . . . . . . 11 (𝜒 → (abs‘∫𝑢(𝐺𝑠) d𝑠) ≤ ∫𝑢(abs‘(𝐺𝑠)) d𝑠)
150 simpl2 1250 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) → 𝑎 ∈ ℝ+)
151150ad2antrr 719 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → 𝑎 ∈ ℝ+)
152113, 151sylbi 209 . . . . . . . . . . . . . . 15 (𝜒𝑎 ∈ ℝ+)
153152rpred 12156 . . . . . . . . . . . . . 14 (𝜒𝑎 ∈ ℝ)
154153adantr 474 . . . . . . . . . . . . 13 ((𝜒𝑠𝑢) → 𝑎 ∈ ℝ)
155 iccssxr 12544 . . . . . . . . . . . . . . . 16 (0[,]+∞) ⊆ ℝ*
156 volf 23695 . . . . . . . . . . . . . . . . . 18 vol:dom vol⟶(0[,]+∞)
157156a1i 11 . . . . . . . . . . . . . . . . 17 (𝜒 → vol:dom vol⟶(0[,]+∞))
158157, 130ffvelrnd 6609 . . . . . . . . . . . . . . . 16 (𝜒 → (vol‘𝑢) ∈ (0[,]+∞))
159155, 158sseldi 3825 . . . . . . . . . . . . . . 15 (𝜒 → (vol‘𝑢) ∈ ℝ*)
160 iccvolcl 23733 . . . . . . . . . . . . . . . . 17 ((-π ∈ ℝ ∧ π ∈ ℝ) → (vol‘(-π[,]π)) ∈ ℝ)
16143, 42, 160mp2an 685 . . . . . . . . . . . . . . . 16 (vol‘(-π[,]π)) ∈ ℝ
162161a1i 11 . . . . . . . . . . . . . . 15 (𝜒 → (vol‘(-π[,]π)) ∈ ℝ)
163 mnfxr 10414 . . . . . . . . . . . . . . . . 17 -∞ ∈ ℝ*
164163a1i 11 . . . . . . . . . . . . . . . 16 (𝜒 → -∞ ∈ ℝ*)
165 0xr 10403 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
166165a1i 11 . . . . . . . . . . . . . . . 16 (𝜒 → 0 ∈ ℝ*)
167 mnflt0 12245 . . . . . . . . . . . . . . . . 17 -∞ < 0
168167a1i 11 . . . . . . . . . . . . . . . 16 (𝜒 → -∞ < 0)
169 volge0 40971 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ dom vol → 0 ≤ (vol‘𝑢))
170130, 169syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → 0 ≤ (vol‘𝑢))
171164, 166, 159, 168, 170xrltletrd 12280 . . . . . . . . . . . . . . 15 (𝜒 → -∞ < (vol‘𝑢))
172 iccmbl 23732 . . . . . . . . . . . . . . . . . 18 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ∈ dom vol)
17343, 42, 172mp2an 685 . . . . . . . . . . . . . . . . 17 (-π[,]π) ∈ dom vol
174173a1i 11 . . . . . . . . . . . . . . . 16 (𝜒 → (-π[,]π) ∈ dom vol)
175 volss 23699 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ dom vol ∧ (-π[,]π) ∈ dom vol ∧ 𝑢 ⊆ (-π[,]π)) → (vol‘𝑢) ≤ (vol‘(-π[,]π)))
176130, 174, 126, 175syl3anc 1496 . . . . . . . . . . . . . . 15 (𝜒 → (vol‘𝑢) ≤ (vol‘(-π[,]π)))
177 xrre 12288 . . . . . . . . . . . . . . 15 ((((vol‘𝑢) ∈ ℝ* ∧ (vol‘(-π[,]π)) ∈ ℝ) ∧ (-∞ < (vol‘𝑢) ∧ (vol‘𝑢) ≤ (vol‘(-π[,]π)))) → (vol‘𝑢) ∈ ℝ)
178159, 162, 171, 176, 177syl22anc 874 . . . . . . . . . . . . . 14 (𝜒 → (vol‘𝑢) ∈ ℝ)
179152rpcnd 12158 . . . . . . . . . . . . . 14 (𝜒𝑎 ∈ ℂ)
180 iblconstmpt 40966 . . . . . . . . . . . . . 14 ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑎 ∈ ℂ) → (𝑠𝑢𝑎) ∈ 𝐿1)
181130, 178, 179, 180syl3anc 1496 . . . . . . . . . . . . 13 (𝜒 → (𝑠𝑢𝑎) ∈ 𝐿1)
182154, 181itgrecl 23963 . . . . . . . . . . . 12 (𝜒 → ∫𝑢𝑎 d𝑠 ∈ ℝ)
183 simpl3 1252 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) → ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
184183ad2antrr 719 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
185113, 184sylbi 209 . . . . . . . . . . . . . . . 16 (𝜒 → ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
186 rspa 3139 . . . . . . . . . . . . . . . 16 ((∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎𝑛 ∈ ℕ) → ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
187185, 133, 186syl2anc 581 . . . . . . . . . . . . . . 15 (𝜒 → ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
188187adantr 474 . . . . . . . . . . . . . 14 ((𝜒𝑠𝑢) → ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎)
189 rspa 3139 . . . . . . . . . . . . . 14 ((∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎𝑠 ∈ (-π[,]π)) → (abs‘(𝐺𝑠)) ≤ 𝑎)
190188, 127, 189syl2anc 581 . . . . . . . . . . . . 13 ((𝜒𝑠𝑢) → (abs‘(𝐺𝑠)) ≤ 𝑎)
191142, 181, 141, 154, 190itgle 23975 . . . . . . . . . . . 12 (𝜒 → ∫𝑢(abs‘(𝐺𝑠)) d𝑠 ≤ ∫𝑢𝑎 d𝑠)
192 itgconst 23984 . . . . . . . . . . . . . 14 ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑎 ∈ ℂ) → ∫𝑢𝑎 d𝑠 = (𝑎 · (vol‘𝑢)))
193130, 178, 179, 192syl3anc 1496 . . . . . . . . . . . . 13 (𝜒 → ∫𝑢𝑎 d𝑠 = (𝑎 · (vol‘𝑢)))
194153, 178remulcld 10387 . . . . . . . . . . . . . 14 (𝜒 → (𝑎 · (vol‘𝑢)) ∈ ℝ)
195 3re 11431 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℝ
196195a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜒 → 3 ∈ ℝ)
197 3ne0 11464 . . . . . . . . . . . . . . . . . . 19 3 ≠ 0
198197a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜒 → 3 ≠ 0)
199147, 196, 198redivcld 11179 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑒 / 3) ∈ ℝ)
200152rpne0d 12161 . . . . . . . . . . . . . . . . 17 (𝜒𝑎 ≠ 0)
201199, 153, 200redivcld 11179 . . . . . . . . . . . . . . . 16 (𝜒 → ((𝑒 / 3) / 𝑎) ∈ ℝ)
20294, 201syl5eqel 2910 . . . . . . . . . . . . . . 15 (𝜒𝐷 ∈ ℝ)
203153, 202remulcld 10387 . . . . . . . . . . . . . 14 (𝜒 → (𝑎 · 𝐷) ∈ ℝ)
204152rpge0d 12160 . . . . . . . . . . . . . . 15 (𝜒 → 0 ≤ 𝑎)
205 simplrr 798 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → (vol‘𝑢) ≤ 𝐷)
206113, 205sylbi 209 . . . . . . . . . . . . . . 15 (𝜒 → (vol‘𝑢) ≤ 𝐷)
207178, 202, 153, 204, 206lemul2ad 11294 . . . . . . . . . . . . . 14 (𝜒 → (𝑎 · (vol‘𝑢)) ≤ (𝑎 · 𝐷))
20894oveq2i 6916 . . . . . . . . . . . . . . . 16 (𝑎 · 𝐷) = (𝑎 · ((𝑒 / 3) / 𝑎))
209199recnd 10385 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑒 / 3) ∈ ℂ)
210209, 179, 200divcan2d 11129 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑎 · ((𝑒 / 3) / 𝑎)) = (𝑒 / 3))
211208, 210syl5eq 2873 . . . . . . . . . . . . . . 15 (𝜒 → (𝑎 · 𝐷) = (𝑒 / 3))
212 2rp 12117 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
213212a1i 11 . . . . . . . . . . . . . . . 16 (𝜒 → 2 ∈ ℝ+)
21496a1i 11 . . . . . . . . . . . . . . . 16 (𝜒 → 3 ∈ ℝ+)
215 2lt3 11530 . . . . . . . . . . . . . . . . 17 2 < 3
216215a1i 11 . . . . . . . . . . . . . . . 16 (𝜒 → 2 < 3)
217213, 214, 146, 216ltdiv2dd 40306 . . . . . . . . . . . . . . 15 (𝜒 → (𝑒 / 3) < (𝑒 / 2))
218211, 217eqbrtrd 4895 . . . . . . . . . . . . . 14 (𝜒 → (𝑎 · 𝐷) < (𝑒 / 2))
219194, 203, 148, 207, 218lelttrd 10514 . . . . . . . . . . . . 13 (𝜒 → (𝑎 · (vol‘𝑢)) < (𝑒 / 2))
220193, 219eqbrtrd 4895 . . . . . . . . . . . 12 (𝜒 → ∫𝑢𝑎 d𝑠 < (𝑒 / 2))
221143, 182, 148, 191, 220lelttrd 10514 . . . . . . . . . . 11 (𝜒 → ∫𝑢(abs‘(𝐺𝑠)) d𝑠 < (𝑒 / 2))
222139, 143, 148, 149, 221lelttrd 10514 . . . . . . . . . 10 (𝜒 → (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2))
223113, 222sylbir 227 . . . . . . . . 9 ((((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ) → (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2))
224223ex 403 . . . . . . . 8 (((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) → (𝑛 ∈ ℕ → (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)))
225112, 224ralrimi 3166 . . . . . . 7 (((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2))
226225ex 403 . . . . . 6 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) → ((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)))
227226ralrimiva 3175 . . . . 5 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) → ∀𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)))
228 breq2 4877 . . . . . . 7 (𝑑 = 𝐷 → ((vol‘𝑢) ≤ 𝑑 ↔ (vol‘𝑢) ≤ 𝐷))
229228anbi2d 624 . . . . . 6 (𝑑 = 𝐷 → ((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) ↔ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)))
230229rspceaimv 3534 . . . . 5 ((𝐷 ∈ ℝ+ ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2))) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)))
231104, 227, 230syl2anc 581 . . . 4 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)))
232231rexlimdv3a 3242 . . 3 ((𝜑𝑒 ∈ ℝ+) → (∃𝑎 ∈ ℝ+𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺𝑠)) ≤ 𝑎 → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2))))
23393, 232mpd 15 . 2 ((𝜑𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)))
234 simplll 793 . . . . . . . . . . . 12 ((((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) ∧ 𝑠𝑢) → 𝜑)
235 simplr 787 . . . . . . . . . . . 12 ((((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) ∧ 𝑠𝑢) → 𝑛 ∈ ℕ)
236 simpllr 795 . . . . . . . . . . . . 13 ((((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) ∧ 𝑠𝑢) → 𝑢 ⊆ (-π[,]π))
237 simpr 479 . . . . . . . . . . . . 13 ((((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) ∧ 𝑠𝑢) → 𝑠𝑢)
238236, 237sseldd 3828 . . . . . . . . . . . 12 ((((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) ∧ 𝑠𝑢) → 𝑠 ∈ (-π[,]π))
239234, 235, 238, 54syl21anc 873 . . . . . . . . . . 11 ((((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) ∧ 𝑠𝑢) → (𝐺𝑠) = ((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))))
240239itgeq2dv 23947 . . . . . . . . . 10 (((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) → ∫𝑢(𝐺𝑠) d𝑠 = ∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠)
241240fveq2d 6437 . . . . . . . . 9 (((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) → (abs‘∫𝑢(𝐺𝑠) d𝑠) = (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠))
242241breq1d 4883 . . . . . . . 8 (((𝜑𝑢 ⊆ (-π[,]π)) ∧ 𝑛 ∈ ℕ) → ((abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2) ↔ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)))
243242ralbidva 3194 . . . . . . 7 ((𝜑𝑢 ⊆ (-π[,]π)) → (∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2) ↔ ∀𝑛 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)))
244 oveq1 6912 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (𝑛 + (1 / 2)) = (𝑘 + (1 / 2)))
245244oveq1d 6920 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → ((𝑛 + (1 / 2)) · 𝑠) = ((𝑘 + (1 / 2)) · 𝑠))
246245fveq2d 6437 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (sin‘((𝑛 + (1 / 2)) · 𝑠)) = (sin‘((𝑘 + (1 / 2)) · 𝑠)))
247246oveq2d 6921 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) = ((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))))
248247adantr 474 . . . . . . . . . . 11 ((𝑛 = 𝑘𝑠𝑢) → ((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) = ((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))))
249248itgeq2dv 23947 . . . . . . . . . 10 (𝑛 = 𝑘 → ∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠 = ∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠)
250249fveq2d 6437 . . . . . . . . 9 (𝑛 = 𝑘 → (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠) = (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠))
251250breq1d 4883 . . . . . . . 8 (𝑛 = 𝑘 → ((abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2) ↔ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)))
252251cbvralv 3383 . . . . . . 7 (∀𝑛 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2) ↔ ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))
253243, 252syl6bb 279 . . . . . 6 ((𝜑𝑢 ⊆ (-π[,]π)) → (∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2) ↔ ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)))
254253adantrr 710 . . . . 5 ((𝜑 ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑)) → (∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2) ↔ ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)))
255254pm5.74da 840 . . . 4 (𝜑 → (((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)) ↔ ((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))))
256255rexralbidv 3268 . . 3 (𝜑 → (∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)) ↔ ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))))
257256adantr 474 . 2 ((𝜑𝑒 ∈ ℝ+) → (∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑛 ∈ ℕ (abs‘∫𝑢(𝐺𝑠) d𝑠) < (𝑒 / 2)) ↔ ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))))
258233, 257mpbid 224 1 ((𝜑𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166   ≠ wne 2999  ∀wral 3117  ∃wrex 3118   ⊆ wss 3798  ifcif 4306   class class class wbr 4873   ↦ cmpt 4952  dom cdm 5342  ⟶wf 6119  ‘cfv 6123  (class class class)co 6905  ℂcc 10250  ℝcr 10251  0cc0 10252  1c1 10253   + caddc 10255   · cmul 10257  +∞cpnf 10388  -∞cmnf 10389  ℝ*cxr 10390   < clt 10391   ≤ cle 10392   − cmin 10585  -cneg 10586   / cdiv 11009  ℕcn 11350  2c2 11406  3c3 11407  ℝ+crp 12112  [,]cicc 12466  abscabs 14351  sincsin 15166  πcpi 15169  volcvol 23629  𝐿1cibl 23783  ∫citg 23784 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-cc 9572  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330  ax-addf 10331  ax-mulf 10332 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-disj 4842  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-of 7157  df-ofr 7158  df-om 7327  df-1st 7428  df-2nd 7429  df-supp 7560  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-omul 7831  df-er 8009  df-map 8124  df-pm 8125  df-ixp 8176  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-fsupp 8545  df-fi 8586  df-sup 8617  df-inf 8618  df-oi 8684  df-card 9078  df-acn 9081  df-cda 9305  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-n0 11619  df-z 11705  df-dec 11822  df-uz 11969  df-q 12072  df-rp 12113  df-xneg 12232  df-xadd 12233  df-xmul 12234  df-ioo 12467  df-ioc 12468  df-ico 12469  df-icc 12470  df-fz 12620  df-fzo 12761  df-fl 12888  df-mod 12964  df-seq 13096  df-exp 13155  df-fac 13354  df-bc 13383  df-hash 13411  df-shft 14184  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-limsup 14579  df-clim 14596  df-rlim 14597  df-sum 14794  df-ef 15170  df-sin 15172  df-cos 15173  df-pi 15175  df-struct 16224  df-ndx 16225  df-slot 16226  df-base 16228  df-sets 16229  df-ress 16230  df-plusg 16318  df-mulr 16319  df-starv 16320  df-sca 16321  df-vsca 16322  df-ip 16323  df-tset 16324  df-ple 16325  df-ds 16327  df-unif 16328  df-hom 16329  df-cco 16330  df-rest 16436  df-topn 16437  df-0g 16455  df-gsum 16456  df-topgen 16457  df-pt 16458  df-prds 16461  df-xrs 16515  df-qtop 16520  df-imas 16521  df-xps 16523  df-mre 16599  df-mrc 16600  df-acs 16602  df-mgm 17595  df-sgrp 17637  df-mnd 17648  df-submnd 17689  df-mulg 17895  df-cntz 18100  df-cmn 18548  df-psmet 20098  df-xmet 20099  df-met 20100  df-bl 20101  df-mopn 20102  df-fbas 20103  df-fg 20104  df-cnfld 20107  df-top 21069  df-topon 21086  df-topsp 21108  df-bases 21121  df-cld 21194  df-ntr 21195  df-cls 21196  df-nei 21273  df-lp 21311  df-perf 21312  df-cn 21402  df-cnp 21403  df-t1 21489  df-haus 21490  df-cmp 21561  df-tx 21736  df-hmeo 21929  df-fil 22020  df-fm 22112  df-flim 22113  df-flf 22114  df-xms 22495  df-ms 22496  df-tms 22497  df-cncf 23051  df-ovol 23630  df-vol 23631  df-mbf 23785  df-itg1 23786  df-itg2 23787  df-ibl 23788  df-itg 23789  df-0p 23836  df-limc 24029  df-dv 24030 This theorem is referenced by:  fourierdlem103  41220  fourierdlem104  41221
 Copyright terms: Public domain W3C validator