Metamath Proof Explorer

Theorem dvdivbd

Description: A sufficient condition for the derivative to be bounded, for the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvdivbd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvdivbd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvdivbd.adv ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
dvdivbd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
dvdivbd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
dvdivbd.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
dvdivbd.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
dvdivbd.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
dvdivbd.q ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
dvdivbd.cbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐶 ) ≤ 𝑈 )
dvdivbd.bbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ≤ 𝑅 )
dvdivbd.dbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐷 ) ≤ 𝑇 )
dvdivbd.abd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ≤ 𝑄 )
dvdivbd.bdv ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
dvdivbd.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ℂ )
dvdivbd.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
dvdivbd.ele ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐸 ≤ ( abs ‘ 𝐵 ) )
dvdivbd.f ⊢ 𝐹 = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) )
Assertion dvdivbd ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )

Proof

Step Hyp Ref Expression
1 dvdivbd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvdivbd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 dvdivbd.adv ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
4 dvdivbd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
5 dvdivbd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
6 dvdivbd.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
7 dvdivbd.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
8 dvdivbd.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
9 dvdivbd.q ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
10 dvdivbd.cbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐶 ) ≤ 𝑈 )
11 dvdivbd.bbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ≤ 𝑅 )
12 dvdivbd.dbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐷 ) ≤ 𝑇 )
13 dvdivbd.abd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ≤ 𝑄 )
14 dvdivbd.bdv ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
15 dvdivbd.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ℂ )
16 dvdivbd.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
17 dvdivbd.ele ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐸 ≤ ( abs ‘ 𝐵 ) )
18 dvdivbd.f ⊢ 𝐹 = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) )
19 6 7 remulcld ⊢ ( 𝜑 → ( 𝑈 · 𝑅 ) ∈ ℝ )
20 8 9 remulcld ⊢ ( 𝜑 → ( 𝑇 · 𝑄 ) ∈ ℝ )
21 19 20 readdcld ⊢ ( 𝜑 → ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) ∈ ℝ )
22 16 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
23 22 resqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
24 16 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
25 16 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
26 25 gt0ne0d ⊢ ( 𝜑 → 𝐸 ≠ 0 )
27 2z ⊢ 2 ∈ ℤ
28 27 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
29 24 26 28 expne0d ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ≠ 0 )
30 21 23 29 redivcld ⊢ ( 𝜑 → ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) ∈ ℝ )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → 𝐵 = 0 )
32 31 abs00bd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → ( abs ‘ 𝐵 ) = 0 )
33 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℝ )
34 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ ℝ )
35 5 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
36 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 < 𝐸 )
37 17 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ≤ ( abs ‘ 𝐵 ) )
38 33 34 35 36 37 ltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 < ( abs ‘ 𝐵 ) )
39 38 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ≠ 0 )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → ( abs ‘ 𝐵 ) ≠ 0 )
41 40 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → ¬ ( abs ‘ 𝐵 ) = 0 )
42 32 41 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ¬ 𝐵 = 0 )
43 42 neqned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ≠ 0 )
44 eldifsn ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
45 5 43 44 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
46 1 2 4 3 45 15 14 dvmptdiv ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) )
47 18 46 eqtrid ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) )
48 4 5 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
49 15 2 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐷 · 𝐴 ) ∈ ℂ )
50 48 49 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ∈ ℂ )
51 5 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
52 sqne0 ⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 ↑ 2 ) ≠ 0 ↔ 𝐵 ≠ 0 ) )
53 5 52 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐵 ↑ 2 ) ≠ 0 ↔ 𝐵 ≠ 0 ) )
54 43 53 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 ↑ 2 ) ≠ 0 )
55 50 51 54 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ∈ ℂ )
56 47 55 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) )
58 50 51 54 absdivd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) = ( ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) / ( abs ‘ ( 𝐵 ↑ 2 ) ) ) )
59 50 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) ∈ ℝ )
60 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) ∈ ℝ )
61 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ ℝ+ )
62 27 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 2 ∈ ℤ )
63 61 62 rpexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
64 51 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐵 ↑ 2 ) ) ∈ ℝ )
65 50 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) )
66 48 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℝ )
67 49 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐷 · 𝐴 ) ) ∈ ℝ )
68 66 67 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) + ( abs ‘ ( 𝐷 · 𝐴 ) ) ) ∈ ℝ )
69 48 49 abs2dif2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) ≤ ( ( abs ‘ ( 𝐶 · 𝐵 ) ) + ( abs ‘ ( 𝐷 · 𝐴 ) ) ) )
70 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑈 · 𝑅 ) ∈ ℝ )
71 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 · 𝑄 ) ∈ ℝ )
72 4 5 absmuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) = ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) )
73 4 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐶 ) ∈ ℝ )
74 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑈 ∈ ℝ )
75 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ )
76 4 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐶 ) )
77 5 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐵 ) )
78 73 74 35 75 76 77 10 11 lemul12ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) ≤ ( 𝑈 · 𝑅 ) )
79 72 78 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ≤ ( 𝑈 · 𝑅 ) )
80 15 2 absmuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐷 · 𝐴 ) ) = ( ( abs ‘ 𝐷 ) · ( abs ‘ 𝐴 ) ) )
81 15 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐷 ) ∈ ℝ )
82 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑇 ∈ ℝ )
83 2 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
84 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑄 ∈ ℝ )
85 15 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐷 ) )
86 2 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐴 ) )
87 81 82 83 84 85 86 12 13 lemul12ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐷 ) · ( abs ‘ 𝐴 ) ) ≤ ( 𝑇 · 𝑄 ) )
88 80 87 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐷 · 𝐴 ) ) ≤ ( 𝑇 · 𝑄 ) )
89 66 67 70 71 79 88 le2addd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) + ( abs ‘ ( 𝐷 · 𝐴 ) ) ) ≤ ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) )
90 59 68 60 69 89 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) ≤ ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) )
91 2nn0 ⊢ 2 ∈ ℕ0
92 91 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 2 ∈ ℕ0 )
93 33 34 36 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ 𝐸 )
94 leexp1a ⊢ ( ( ( 𝐸 ∈ ℝ ∧ ( abs ‘ 𝐵 ) ∈ ℝ ∧ 2 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐸 ∧ 𝐸 ≤ ( abs ‘ 𝐵 ) ) ) → ( 𝐸 ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) )
95 34 35 92 93 37 94 syl32anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) )
96 5 92 absexpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐵 ↑ 2 ) ) = ( ( abs ‘ 𝐵 ) ↑ 2 ) )
97 95 96 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ↑ 2 ) ≤ ( abs ‘ ( 𝐵 ↑ 2 ) ) )
98 59 60 63 64 65 90 97 lediv12ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) / ( abs ‘ ( 𝐵 ↑ 2 ) ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
99 58 98 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
100 57 99 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
101 100 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
102 brralrspcev ⊢ ( ( ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
103 30 101 102 syl2anc ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )