This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem77.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem77.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
fourierdlem77.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
fourierdlem77.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem77.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem77.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
fourierdlem77.bd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 )
Assertion fourierdlem77 ( 𝜑 → ∃ 𝑏 ∈ ℝ+ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 )

Proof

Step Hyp Ref Expression
1 fourierdlem77.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem77.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem77.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
4 fourierdlem77.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
5 fourierdlem77.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
6 fourierdlem77.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
7 fourierdlem77.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
8 fourierdlem77.bd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 )
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 ⊢ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ )
19 18 a1i ⊢ ( ⊤ → 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ ) )
20 11 12 17 19 evthiccabs ⊢ ( ⊤ → ( ∃ 𝑐 ∈ ( - π [,] π ) ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ∧ ∃ 𝑥 ∈ ( - π [,] π ) ∀ 𝑦 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑥 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑦 ) ) ) )
21 20 mptru ⊢ ( ∃ 𝑐 ∈ ( - π [,] π ) ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ∧ ∃ 𝑥 ∈ ( - π [,] π ) ∀ 𝑦 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑥 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑦 ) ) )
22 21 simpli ⊢ ∃ 𝑐 ∈ ( - π [,] π ) ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) )
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) → ∃ 𝑐 ∈ ( - π [,] π ) ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) )
24 simpl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → 𝑎 ∈ ℝ )
25 6 fourierdlem43 ⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ
26 25 ffvelcdmi ⊢ ( 𝑐 ∈ ( - π [,] π ) → ( 𝐾 ‘ 𝑐 ) ∈ ℝ )
27 26 adantl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → ( 𝐾 ‘ 𝑐 ) ∈ ℝ )
28 24 27 remulcld ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ∈ ℝ )
29 28 recnd ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ∈ ℂ )
30 29 abscld ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) ∈ ℝ )
31 29 absge0d ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → 0 ≤ ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) )
32 30 31 ge0p1rpd ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ∈ ℝ+ )
33 32 3ad2antl2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) → ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ∈ ℝ+ )
34 33 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) → ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ∈ ℝ+ )
35 nfv ⊢ Ⅎ 𝑠 𝜑
36 nfv ⊢ Ⅎ 𝑠 𝑎 ∈ ℝ
37 nfra1 ⊢ Ⅎ 𝑠 ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎
38 35 36 37 nf3an ⊢ Ⅎ 𝑠 ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 )
39 nfv ⊢ Ⅎ 𝑠 𝑐 ∈ ( - π [,] π )
40 nfra1 ⊢ Ⅎ 𝑠 ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) )
41 38 39 40 nf3an ⊢ Ⅎ 𝑠 ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) )
42 simpl11 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝜑 )
43 simpl12 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑎 ∈ ℝ )
44 42 43 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝜑 ∧ 𝑎 ∈ ℝ ) )
45 simpl13 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 )
46 rspa ⊢ ( ( ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 )
47 45 46 sylancom ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 )
48 simpl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑐 ∈ ( - π [,] π ) )
49 44 47 48 jca31 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) )
50 rspa ⊢ ( ( ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) )
51 50 3ad2antl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) )
52 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ( - π [,] π ) )
53 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝜑 )
54 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ( - π [,] π ) )
55 1 2 3 4 5 fourierdlem9 ⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )
56 55 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐻 ‘ 𝑠 ) ∈ ℝ )
57 25 ffvelcdmi ⊢ ( 𝑠 ∈ ( - π [,] π ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
59 56 58 remulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ )
60 7 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
61 54 59 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
62 61 59 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ )
63 62 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℂ )
64 63 abscld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ∈ ℝ )
65 53 64 sylancom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ∈ ℝ )
66 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑎 ∈ ℝ )
67 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑐 ∈ ( - π [,] π ) )
68 66 67 30 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) ∈ ℝ )
69 peano2re ⊢ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) ∈ ℝ → ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ∈ ℝ )
70 68 69 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ∈ ℝ )
71 61 fveq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) = ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) )
72 53 71 sylancom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) = ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) )
73 56 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐻 ‘ 𝑠 ) ∈ ℂ )
74 73 abscld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ∈ ℝ )
75 53 74 sylancom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ∈ ℝ )
76 recn ⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℂ )
77 76 abscld ⊢ ( 𝑎 ∈ ℝ → ( abs ‘ 𝑎 ) ∈ ℝ )
78 66 77 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ 𝑎 ) ∈ ℝ )
79 57 recnd ⊢ ( 𝑠 ∈ ( - π [,] π ) → ( 𝐾 ‘ 𝑠 ) ∈ ℂ )
80 79 abscld ⊢ ( 𝑠 ∈ ( - π [,] π ) → ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ )
81 80 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ )
82 26 recnd ⊢ ( 𝑐 ∈ ( - π [,] π ) → ( 𝐾 ‘ 𝑐 ) ∈ ℂ )
83 82 abscld ⊢ ( 𝑐 ∈ ( - π [,] π ) → ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ∈ ℝ )
84 67 83 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ∈ ℝ )
85 73 absge0d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → 0 ≤ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) )
86 53 85 sylancom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 0 ≤ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) )
87 82 absge0d ⊢ ( 𝑐 ∈ ( - π [,] π ) → 0 ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) )
88 67 87 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 0 ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) )
89 74 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ∈ ℝ )
90 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑎 ∈ ℝ )
91 77 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ 𝑎 ) ∈ ℝ )
92 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 )
93 90 leabsd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑎 ≤ ( abs ‘ 𝑎 ) )
94 89 90 91 92 93 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ ( abs ‘ 𝑎 ) )
95 94 ad4ant14 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ ( abs ‘ 𝑎 ) )
96 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) )
97 75 78 81 84 86 88 95 96 lemul12bd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) · ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) )
98 58 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℂ )
99 73 98 absmuld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) = ( ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) · ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ) )
100 53 99 sylancom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) = ( ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) · ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ) )
101 76 adantr ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → 𝑎 ∈ ℂ )
102 27 recnd ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → ( 𝐾 ‘ 𝑐 ) ∈ ℂ )
103 101 102 absmuld ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) = ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) )
104 66 67 103 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) = ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) )
105 97 100 104 3brtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) ≤ ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) )
106 72 105 eqbrtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) )
107 68 ltp1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) < ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) )
108 65 68 70 106 107 lelttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) < ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) )
109 65 70 108 ltled ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ) ∧ ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) )
110 49 51 52 109 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) )
111 110 ex ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) → ( 𝑠 ∈ ( - π [,] π ) → ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ) )
112 41 111 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) → ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) )
113 breq2 ⊢ ( 𝑏 = ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) → ( ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ) )
114 113 ralbidv ⊢ ( 𝑏 = ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) → ( ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ) )
115 114 rspcev ⊢ ( ( ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ∈ ℝ+ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ ( ( abs ‘ ( 𝑎 · ( 𝐾 ‘ 𝑐 ) ) ) + 1 ) ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 )
116 34 112 115 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) ∧ 𝑐 ∈ ( - π [,] π ) ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 )
117 116 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) → ( ∃ 𝑐 ∈ ( - π [,] π ) ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐾 ‘ 𝑠 ) ) ≤ ( abs ‘ ( 𝐾 ‘ 𝑐 ) ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 ) )
118 23 117 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ∧ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 )
119 118 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝐻 ‘ 𝑠 ) ) ≤ 𝑎 → ∃ 𝑏 ∈ ℝ+ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 ) )
120 8 119 mpd ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ+ ∀ 𝑠 ∈ ( - π [,] π ) ( abs ‘ ( 𝑈 ‘ 𝑠 ) ) ≤ 𝑏 )