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 ‘ ( 𝐹𝑥 ) ) ≤ 𝑏 )