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	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem87.x	$⊢ φ \to X \in ℝ$
	fourierdlem87.y	$⊢ φ \to Y \in ℝ$
	fourierdlem87.w	$⊢ φ \to W \in ℝ$
	fourierdlem87.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
	fourierdlem87.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem87.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
	fourierdlem87.s	$⊢ S = (s \in [- π, π] ⟼ \sin (n + (\frac{1}{2})) s)$
	fourierdlem87.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
	fourierdlem87.10	$⊢ φ \to \exists x \in ℝ \forall s \in [- π, π] \|H (s)\| \leq x$
	fourierdlem87.gibl	$⊢ (φ \land n \in ℕ) \to G \in 𝐿^{1}$
	fourierdlem87.d	$⊢ D = \frac{\frac{e}{3}}{a}$
	fourierdlem87.ch	$⊢ χ \leftrightarrow (((((φ \land e \in ℝ^{+}) \land a \in ℝ^{+} \land \forall n \in ℕ \forall s \in [- π, π] \|G (s)\| \leq a) \land u \in dom vol) \land (u \subseteq [- π, π] \land vol (u) \leq D)) \land n \in ℕ)$
Assertion	fourierdlem87	$⊢ (φ \land e \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall u \in dom vol ((u \subseteq [- π, π] \land vol (u) \leq d) \to \forall k \in ℕ \|\int_{u} U (s) \sin (k + (\frac{1}{2})) s d s\| < \frac{e}{2})$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem87

Proof