Metamath Proof Explorer

Theorem fourierdlem77

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

Ref Expression
Hypotheses fourierdlem77.f ⊢φ→F:ℝ⟶ℝ
fourierdlem77.x ⊢φ→X∈ℝ
fourierdlem77.y ⊢φ→Y∈ℝ
fourierdlem77.w ⊢φ→W∈ℝ
fourierdlem77.h ⊢H=s∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
fourierdlem77.k ⊢K=s∈−ππ⟼ifs=01s2⁢sin⁡s2
fourierdlem77.u ⊢U=s∈−ππ⟼H⁡s⁢K⁡s
fourierdlem77.bd ⊢φ→∃a∈ℝ∀s∈−ππH⁡s≤a
Assertion fourierdlem77 ⊢φ→∃b∈ℝ+∀s∈−ππU⁡s≤b

Proof

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