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	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 ∈ 𝐿¹ )
	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	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 ∈ 𝐿¹ )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ )
32		nnre	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
33	8	fourierdlem5	⊢ ( 𝑛 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ )
34	32 33	syl	⊢ ( 𝑛 ∈ ℕ → 𝑆 : ( - π [,] π ) ⟶ ℝ )
35	34	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
36	35 28	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℝ )
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	mulridd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 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	ffvelcdmd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ 𝑢 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
130		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ⁺ ∧ ∀ 𝑛 ∈ ℕ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐺 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑢 ∈ dom vol ) ∧ ( 𝑢 ⊆ ( - π [,] π ) ∧ ( vol ‘ 𝑢 ) ≤ 𝐷 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑢 ∈ dom vol )
131	13 130	sylbi	⊢ ( 𝜒 → 𝑢 ∈ dom vol )
132	124	ffvelcdmda	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
133	124	feqmptd	⊢ ( 𝜒 → 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
134	13	simprbi	⊢ ( 𝜒 → 𝑛 ∈ ℕ )
135	117 134 11	syl2anc	⊢ ( 𝜒 → 𝐺 ∈ 𝐿¹ )
136	133 135	eqeltrrd	⊢ ( 𝜒 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝐺 ‘ 𝑠 ) ) ∈ 𝐿¹ )
137	127 131 132 136	iblss	⊢ ( 𝜒 → ( 𝑠 ∈ 𝑢 ↦ ( 𝐺 ‘ 𝑠 ) ) ∈ 𝐿¹ )
138	129 137	itgcl	⊢ ( 𝜒 → ∫ 𝑢 ( 𝐺 ‘ 𝑠 ) d 𝑠 ∈ ℂ )
139	138	abscld	⊢ ( 𝜒 → ( abs ‘ ∫ 𝑢 ( 𝐺 ‘ 𝑠 ) d 𝑠 ) ∈ ℝ )
140	129	recnd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ 𝑢 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℂ )
141	140	abscld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ 𝑢 ) → ( abs ‘ ( 𝐺 ‘ 𝑠 ) ) ∈ ℝ )
142	129 137	iblabs	⊢ ( 𝜒 → ( 𝑠 ∈ 𝑢 ↦ ( abs ‘ ( 𝐺 ‘ 𝑠 ) ) ) ∈ 𝐿¹ )
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	ffvelcdmd	⊢ ( 𝜒 → ( 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 ‘ 𝑢 ) ∈ ℝ ∧ 𝑎 ∈ ℂ ) → ( 𝑠 ∈ 𝑢 ↦ 𝑎 ) ∈ 𝐿¹ )
181	131 178 179 180	syl3anc	⊢ ( 𝜒 → ( 𝑠 ∈ 𝑢 ↦ 𝑎 ) ∈ 𝐿¹ )
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 ) ) )

Metamath Proof Explorer

Theorem fourierdlem87

Proof