fourierdlem77

Description: If H is bounded, then U is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem77.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem77.x	$⊢ φ \to X \in ℝ$
	fourierdlem77.y	$⊢ φ \to Y \in ℝ$
	fourierdlem77.w	$⊢ φ \to W \in ℝ$
	fourierdlem77.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
	fourierdlem77.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem77.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
	fourierdlem77.bd	$⊢ φ \to \exists a \in ℝ \forall s \in [- π, π] \|H (s)\| \leq a$
Assertion	fourierdlem77	$⊢ φ \to \exists b \in ℝ^{+} \forall s \in [- π, π] \|U (s)\| \leq b$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem77.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem77.x	$⊢ φ \to X \in ℝ$
3		fourierdlem77.y	$⊢ φ \to Y \in ℝ$
4		fourierdlem77.w	$⊢ φ \to W \in ℝ$
5		fourierdlem77.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
6		fourierdlem77.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
7		fourierdlem77.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
8		fourierdlem77.bd	$⊢ φ \to \exists a \in ℝ \forall s \in [- π, π] \|H (s)\| \leq a$
9		pire	$⊢ π \in ℝ$
10	9	renegcli	$⊢ - π \in ℝ$
11	10	a1i	$⊢ ⊤ \to - π \in ℝ$
12	9	a1i	$⊢ ⊤ \to π \in ℝ$
13		pirp	$⊢ π \in ℝ^{+}$
14		neglt	$⊢ π \in ℝ^{+} \to - π < π$
15	13 14	ax-mp	$⊢ - π < π$
16	10 9 15	ltleii	$⊢ - π \leq π$
17	16	a1i	$⊢ ⊤ \to - π \leq π$
18	6	fourierdlem62	$⊢ K : [- π, π] \underset{cn}{⟶} ℝ$
19	18	a1i	$⊢ ⊤ \to K : [- π, π] \underset{cn}{⟶} ℝ$
20	11 12 17 19	evthiccabs	$⊢ ⊤ \to (\exists c \in [- π, π] \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\| \land \exists x \in [- π, π] \forall y \in [- π, π] \|K (x)\| \leq \|K (y)\|)$
21	20	mptru	$⊢ (\exists c \in [- π, π] \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\| \land \exists x \in [- π, π] \forall y \in [- π, π] \|K (x)\| \leq \|K (y)\|)$
22	21	simpli	$⊢ \exists c \in [- π, π] \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|$
23	22	a1i	$⊢ (φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \to \exists c \in [- π, π] \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|$
24		simpl	$⊢ (a \in ℝ \land c \in [- π, π]) \to a \in ℝ$
25	6	fourierdlem43	$⊢ K : [- π, π] ⟶ ℝ$
26	25	ffvelcdmi	$⊢ c \in [- π, π] \to K (c) \in ℝ$
27	26	adantl	$⊢ (a \in ℝ \land c \in [- π, π]) \to K (c) \in ℝ$
28	24 27	remulcld	$⊢ (a \in ℝ \land c \in [- π, π]) \to a K (c) \in ℝ$
29	28	recnd	$⊢ (a \in ℝ \land c \in [- π, π]) \to a K (c) \in ℂ$
30	29	abscld	$⊢ (a \in ℝ \land c \in [- π, π]) \to \|a K (c)\| \in ℝ$
31	29	absge0d	$⊢ (a \in ℝ \land c \in [- π, π]) \to 0 \leq \|a K (c)\|$
32	30 31	ge0p1rpd	$⊢ (a \in ℝ \land c \in [- π, π]) \to \|a K (c)\| + 1 \in ℝ^{+}$
33	32	3ad2antl2	$⊢ ((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π]) \to \|a K (c)\| + 1 \in ℝ^{+}$
34	33	3adant3	$⊢ ((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \to \|a K (c)\| + 1 \in ℝ^{+}$
35		nfv	$⊢ Ⅎ s φ$
36		nfv	$⊢ Ⅎ s a \in ℝ$
37		nfra1	$⊢ Ⅎ s \forall s \in [- π, π] \|H (s)\| \leq a$
38	35 36 37	nf3an	$⊢ Ⅎ s (φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a)$
39		nfv	$⊢ Ⅎ s c \in [- π, π]$
40		nfra1	$⊢ Ⅎ s \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|$
41	38 39 40	nf3an	$⊢ Ⅎ s ((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|)$
42		simpl11	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to φ$
43		simpl12	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to a \in ℝ$
44	42 43	jca	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to (φ \land a \in ℝ)$
45		simpl13	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \forall s \in [- π, π] \|H (s)\| \leq a$
46		rspa	$⊢ (\forall s \in [- π, π] \|H (s)\| \leq a \land s \in [- π, π]) \to \|H (s)\| \leq a$
47	45 46	sylancom	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|H (s)\| \leq a$
48		simpl2	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to c \in [- π, π]$
49	44 47 48	jca31	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to (((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π])$
50		rspa	$⊢ (\forall s \in [- π, π] \|K (s)\| \leq \|K (c)\| \land s \in [- π, π]) \to \|K (s)\| \leq \|K (c)\|$
51	50	3ad2antl3	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|K (s)\| \leq \|K (c)\|$
52		simpr	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to s \in [- π, π]$
53		simp-5l	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to φ$
54		simpr	$⊢ (φ \land s \in [- π, π]) \to s \in [- π, π]$
55	1 2 3 4 5	fourierdlem9	$⊢ φ \to H : [- π, π] ⟶ ℝ$
56	55	ffvelcdmda	$⊢ (φ \land s \in [- π, π]) \to H (s) \in ℝ$
57	25	ffvelcdmi	$⊢ s \in [- π, π] \to K (s) \in ℝ$
58	57	adantl	$⊢ (φ \land s \in [- π, π]) \to K (s) \in ℝ$
59	56 58	remulcld	$⊢ (φ \land s \in [- π, π]) \to H (s) K (s) \in ℝ$
60	7	fvmpt2	$⊢ (s \in [- π, π] \land H (s) K (s) \in ℝ) \to U (s) = H (s) K (s)$
61	54 59 60	syl2anc	$⊢ (φ \land s \in [- π, π]) \to U (s) = H (s) K (s)$
62	61 59	eqeltrd	$⊢ (φ \land s \in [- π, π]) \to U (s) \in ℝ$
63	62	recnd	$⊢ (φ \land s \in [- π, π]) \to U (s) \in ℂ$
64	63	abscld	$⊢ (φ \land s \in [- π, π]) \to \|U (s)\| \in ℝ$
65	53 64	sylancom	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|U (s)\| \in ℝ$
66		simp-5r	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to a \in ℝ$
67		simpllr	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to c \in [- π, π]$
68	66 67 30	syl2anc	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|a K (c)\| \in ℝ$
69		peano2re	$⊢ \|a K (c)\| \in ℝ \to \|a K (c)\| + 1 \in ℝ$
70	68 69	syl	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|a K (c)\| + 1 \in ℝ$
71	61	fveq2d	$⊢ (φ \land s \in [- π, π]) \to \|U (s)\| = \|H (s) K (s)\|$
72	53 71	sylancom	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|U (s)\| = \|H (s) K (s)\|$
73	56	recnd	$⊢ (φ \land s \in [- π, π]) \to H (s) \in ℂ$
74	73	abscld	$⊢ (φ \land s \in [- π, π]) \to \|H (s)\| \in ℝ$
75	53 74	sylancom	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|H (s)\| \in ℝ$
76		recn	$⊢ a \in ℝ \to a \in ℂ$
77	76	abscld	$⊢ a \in ℝ \to \|a\| \in ℝ$
78	66 77	syl	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|a\| \in ℝ$
79	57	recnd	$⊢ s \in [- π, π] \to K (s) \in ℂ$
80	79	abscld	$⊢ s \in [- π, π] \to \|K (s)\| \in ℝ$
81	80	adantl	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|K (s)\| \in ℝ$
82	26	recnd	$⊢ c \in [- π, π] \to K (c) \in ℂ$
83	82	abscld	$⊢ c \in [- π, π] \to \|K (c)\| \in ℝ$
84	67 83	syl	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|K (c)\| \in ℝ$
85	73	absge0d	$⊢ (φ \land s \in [- π, π]) \to 0 \leq \|H (s)\|$
86	53 85	sylancom	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to 0 \leq \|H (s)\|$
87	82	absge0d	$⊢ c \in [- π, π] \to 0 \leq \|K (c)\|$
88	67 87	syl	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to 0 \leq \|K (c)\|$
89	74	ad4ant14	$⊢ (((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land s \in [- π, π]) \to \|H (s)\| \in ℝ$
90		simpllr	$⊢ (((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land s \in [- π, π]) \to a \in ℝ$
91	77	ad3antlr	$⊢ (((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land s \in [- π, π]) \to \|a\| \in ℝ$
92		simplr	$⊢ (((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land s \in [- π, π]) \to \|H (s)\| \leq a$
93	90	leabsd	$⊢ (((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land s \in [- π, π]) \to a \leq \|a\|$
94	89 90 91 92 93	letrd	$⊢ (((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land s \in [- π, π]) \to \|H (s)\| \leq \|a\|$
95	94	ad4ant14	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|H (s)\| \leq \|a\|$
96		simplr	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|K (s)\| \leq \|K (c)\|$
97	75 78 81 84 86 88 95 96	lemul12bd	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|H (s)\| \|K (s)\| \leq \|a\| \|K (c)\|$
98	58	recnd	$⊢ (φ \land s \in [- π, π]) \to K (s) \in ℂ$
99	73 98	absmuld	$⊢ (φ \land s \in [- π, π]) \to \|H (s) K (s)\| = \|H (s)\| \|K (s)\|$
100	53 99	sylancom	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|H (s) K (s)\| = \|H (s)\| \|K (s)\|$
101	76	adantr	$⊢ (a \in ℝ \land c \in [- π, π]) \to a \in ℂ$
102	27	recnd	$⊢ (a \in ℝ \land c \in [- π, π]) \to K (c) \in ℂ$
103	101 102	absmuld	$⊢ (a \in ℝ \land c \in [- π, π]) \to \|a K (c)\| = \|a\| \|K (c)\|$
104	66 67 103	syl2anc	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|a K (c)\| = \|a\| \|K (c)\|$
105	97 100 104	3brtr4d	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|H (s) K (s)\| \leq \|a K (c)\|$
106	72 105	eqbrtrd	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|U (s)\| \leq \|a K (c)\|$
107	68	ltp1d	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|a K (c)\| < \|a K (c)\| + 1$
108	65 68 70 106 107	lelttrd	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|U (s)\| < \|a K (c)\| + 1$
109	65 70 108	ltled	$⊢ (((((φ \land a \in ℝ) \land \|H (s)\| \leq a) \land c \in [- π, π]) \land \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|U (s)\| \leq \|a K (c)\| + 1$
110	49 51 52 109	syl21anc	$⊢ (((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \land s \in [- π, π]) \to \|U (s)\| \leq \|a K (c)\| + 1$
111	110	ex	$⊢ ((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \to (s \in [- π, π] \to \|U (s)\| \leq \|a K (c)\| + 1)$
112	41 111	ralrimi	$⊢ ((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \to \forall s \in [- π, π] \|U (s)\| \leq \|a K (c)\| + 1$
113		breq2	$⊢ b = \|a K (c)\| + 1 \to (\|U (s)\| \leq b \leftrightarrow \|U (s)\| \leq \|a K (c)\| + 1)$
114	113	ralbidv	$⊢ b = \|a K (c)\| + 1 \to (\forall s \in [- π, π] \|U (s)\| \leq b \leftrightarrow \forall s \in [- π, π] \|U (s)\| \leq \|a K (c)\| + 1)$
115	114	rspcev	$⊢ (\|a K (c)\| + 1 \in ℝ^{+} \land \forall s \in [- π, π] \|U (s)\| \leq \|a K (c)\| + 1) \to \exists b \in ℝ^{+} \forall s \in [- π, π] \|U (s)\| \leq b$
116	34 112 115	syl2anc	$⊢ ((φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \land c \in [- π, π] \land \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\|) \to \exists b \in ℝ^{+} \forall s \in [- π, π] \|U (s)\| \leq b$
117	116	rexlimdv3a	$⊢ (φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \to (\exists c \in [- π, π] \forall s \in [- π, π] \|K (s)\| \leq \|K (c)\| \to \exists b \in ℝ^{+} \forall s \in [- π, π] \|U (s)\| \leq b)$
118	23 117	mpd	$⊢ (φ \land a \in ℝ \land \forall s \in [- π, π] \|H (s)\| \leq a) \to \exists b \in ℝ^{+} \forall s \in [- π, π] \|U (s)\| \leq b$
119	118	rexlimdv3a	$⊢ φ \to (\exists a \in ℝ \forall s \in [- π, π] \|H (s)\| \leq a \to \exists b \in ℝ^{+} \forall s \in [- π, π] \|U (s)\| \leq b)$
120	8 119	mpd	$⊢ φ \to \exists b \in ℝ^{+} \forall s \in [- π, π] \|U (s)\| \leq b$

Metamath Proof Explorer

Theorem fourierdlem77

Proof