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
|- ( ph -> S e. { RR , CC } )
dvdivbd.a
|- ( ( ph /\ x e. X ) -> A e. CC )
dvdivbd.adv
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> C ) )
dvdivbd.c
|- ( ( ph /\ x e. X ) -> C e. CC )
dvdivbd.b
|- ( ( ph /\ x e. X ) -> B e. CC )
dvdivbd.u
|- ( ph -> U e. RR )
dvdivbd.r
|- ( ph -> R e. RR )
dvdivbd.t
|- ( ph -> T e. RR )
dvdivbd.q
|- ( ph -> Q e. RR )
dvdivbd.cbd
|- ( ( ph /\ x e. X ) -> ( abs ` C ) <_ U )
dvdivbd.bbd
|- ( ( ph /\ x e. X ) -> ( abs ` B ) <_ R )
dvdivbd.dbd
|- ( ( ph /\ x e. X ) -> ( abs ` D ) <_ T )
dvdivbd.abd
|- ( ( ph /\ x e. X ) -> ( abs ` A ) <_ Q )
dvdivbd.bdv
|- ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> D ) )
dvdivbd.d
|- ( ( ph /\ x e. X ) -> D e. CC )
dvdivbd.e
|- ( ph -> E e. RR+ )
dvdivbd.ele
|- ( ph -> A. x e. X E <_ ( abs ` B ) )
dvdivbd.f
|- F = ( S _D ( x e. X |-> ( A / B ) ) )
Assertion dvdivbd
|- ( ph -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b )

Proof

Step Hyp Ref Expression
1 dvdivbd.s
 |-  ( ph -> S e. { RR , CC } )
2 dvdivbd.a
 |-  ( ( ph /\ x e. X ) -> A e. CC )
3 dvdivbd.adv
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> C ) )
4 dvdivbd.c
 |-  ( ( ph /\ x e. X ) -> C e. CC )
5 dvdivbd.b
 |-  ( ( ph /\ x e. X ) -> B e. CC )
6 dvdivbd.u
 |-  ( ph -> U e. RR )
7 dvdivbd.r
 |-  ( ph -> R e. RR )
8 dvdivbd.t
 |-  ( ph -> T e. RR )
9 dvdivbd.q
 |-  ( ph -> Q e. RR )
10 dvdivbd.cbd
 |-  ( ( ph /\ x e. X ) -> ( abs ` C ) <_ U )
11 dvdivbd.bbd
 |-  ( ( ph /\ x e. X ) -> ( abs ` B ) <_ R )
12 dvdivbd.dbd
 |-  ( ( ph /\ x e. X ) -> ( abs ` D ) <_ T )
13 dvdivbd.abd
 |-  ( ( ph /\ x e. X ) -> ( abs ` A ) <_ Q )
14 dvdivbd.bdv
 |-  ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> D ) )
15 dvdivbd.d
 |-  ( ( ph /\ x e. X ) -> D e. CC )
16 dvdivbd.e
 |-  ( ph -> E e. RR+ )
17 dvdivbd.ele
 |-  ( ph -> A. x e. X E <_ ( abs ` B ) )
18 dvdivbd.f
 |-  F = ( S _D ( x e. X |-> ( A / B ) ) )
19 6 7 remulcld
 |-  ( ph -> ( U x. R ) e. RR )
20 8 9 remulcld
 |-  ( ph -> ( T x. Q ) e. RR )
21 19 20 readdcld
 |-  ( ph -> ( ( U x. R ) + ( T x. Q ) ) e. RR )
22 16 rpred
 |-  ( ph -> E e. RR )
23 22 resqcld
 |-  ( ph -> ( E ^ 2 ) e. RR )
24 16 rpcnd
 |-  ( ph -> E e. CC )
25 16 rpgt0d
 |-  ( ph -> 0 < E )
26 25 gt0ne0d
 |-  ( ph -> E =/= 0 )
27 2z
 |-  2 e. ZZ
28 27 a1i
 |-  ( ph -> 2 e. ZZ )
29 24 26 28 expne0d
 |-  ( ph -> ( E ^ 2 ) =/= 0 )
30 21 23 29 redivcld
 |-  ( ph -> ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) e. RR )
31 simpr
 |-  ( ( ( ph /\ x e. X ) /\ B = 0 ) -> B = 0 )
32 31 abs00bd
 |-  ( ( ( ph /\ x e. X ) /\ B = 0 ) -> ( abs ` B ) = 0 )
33 0red
 |-  ( ( ph /\ x e. X ) -> 0 e. RR )
34 22 adantr
 |-  ( ( ph /\ x e. X ) -> E e. RR )
35 5 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` B ) e. RR )
36 25 adantr
 |-  ( ( ph /\ x e. X ) -> 0 < E )
37 17 r19.21bi
 |-  ( ( ph /\ x e. X ) -> E <_ ( abs ` B ) )
38 33 34 35 36 37 ltletrd
 |-  ( ( ph /\ x e. X ) -> 0 < ( abs ` B ) )
39 38 gt0ne0d
 |-  ( ( ph /\ x e. X ) -> ( abs ` B ) =/= 0 )
40 39 adantr
 |-  ( ( ( ph /\ x e. X ) /\ B = 0 ) -> ( abs ` B ) =/= 0 )
41 40 neneqd
 |-  ( ( ( ph /\ x e. X ) /\ B = 0 ) -> -. ( abs ` B ) = 0 )
42 32 41 pm2.65da
 |-  ( ( ph /\ x e. X ) -> -. B = 0 )
43 42 neqned
 |-  ( ( ph /\ x e. X ) -> B =/= 0 )
44 eldifsn
 |-  ( B e. ( CC \ { 0 } ) <-> ( B e. CC /\ B =/= 0 ) )
45 5 43 44 sylanbrc
 |-  ( ( ph /\ x e. X ) -> B e. ( CC \ { 0 } ) )
46 1 2 4 3 45 15 14 dvmptdiv
 |-  ( ph -> ( S _D ( x e. X |-> ( A / B ) ) ) = ( x e. X |-> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) )
47 18 46 syl5eq
 |-  ( ph -> F = ( x e. X |-> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) )
48 4 5 mulcld
 |-  ( ( ph /\ x e. X ) -> ( C x. B ) e. CC )
49 15 2 mulcld
 |-  ( ( ph /\ x e. X ) -> ( D x. A ) e. CC )
50 48 49 subcld
 |-  ( ( ph /\ x e. X ) -> ( ( C x. B ) - ( D x. A ) ) e. CC )
51 5 sqcld
 |-  ( ( ph /\ x e. X ) -> ( B ^ 2 ) e. CC )
52 sqne0
 |-  ( B e. CC -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) )
53 5 52 syl
 |-  ( ( ph /\ x e. X ) -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) )
54 43 53 mpbird
 |-  ( ( ph /\ x e. X ) -> ( B ^ 2 ) =/= 0 )
55 50 51 54 divcld
 |-  ( ( ph /\ x e. X ) -> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) e. CC )
56 47 55 fvmpt2d
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) = ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) )
57 56 fveq2d
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( F ` x ) ) = ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) )
58 50 51 54 absdivd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) = ( ( abs ` ( ( C x. B ) - ( D x. A ) ) ) / ( abs ` ( B ^ 2 ) ) ) )
59 50 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) e. RR )
60 21 adantr
 |-  ( ( ph /\ x e. X ) -> ( ( U x. R ) + ( T x. Q ) ) e. RR )
61 16 adantr
 |-  ( ( ph /\ x e. X ) -> E e. RR+ )
62 27 a1i
 |-  ( ( ph /\ x e. X ) -> 2 e. ZZ )
63 61 62 rpexpcld
 |-  ( ( ph /\ x e. X ) -> ( E ^ 2 ) e. RR+ )
64 51 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( B ^ 2 ) ) e. RR )
65 50 absge0d
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( abs ` ( ( C x. B ) - ( D x. A ) ) ) )
66 48 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) e. RR )
67 49 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) e. RR )
68 66 67 readdcld
 |-  ( ( ph /\ x e. X ) -> ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) e. RR )
69 48 49 abs2dif2d
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) <_ ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) )
70 19 adantr
 |-  ( ( ph /\ x e. X ) -> ( U x. R ) e. RR )
71 20 adantr
 |-  ( ( ph /\ x e. X ) -> ( T x. Q ) e. RR )
72 4 5 absmuld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) = ( ( abs ` C ) x. ( abs ` B ) ) )
73 4 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` C ) e. RR )
74 6 adantr
 |-  ( ( ph /\ x e. X ) -> U e. RR )
75 7 adantr
 |-  ( ( ph /\ x e. X ) -> R e. RR )
76 4 absge0d
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( abs ` C ) )
77 5 absge0d
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( abs ` B ) )
78 73 74 35 75 76 77 10 11 lemul12ad
 |-  ( ( ph /\ x e. X ) -> ( ( abs ` C ) x. ( abs ` B ) ) <_ ( U x. R ) )
79 72 78 eqbrtrd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) <_ ( U x. R ) )
80 15 2 absmuld
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) = ( ( abs ` D ) x. ( abs ` A ) ) )
81 15 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` D ) e. RR )
82 8 adantr
 |-  ( ( ph /\ x e. X ) -> T e. RR )
83 2 abscld
 |-  ( ( ph /\ x e. X ) -> ( abs ` A ) e. RR )
84 9 adantr
 |-  ( ( ph /\ x e. X ) -> Q e. RR )
85 15 absge0d
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( abs ` D ) )
86 2 absge0d
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( abs ` A ) )
87 81 82 83 84 85 86 12 13 lemul12ad
 |-  ( ( ph /\ x e. X ) -> ( ( abs ` D ) x. ( abs ` A ) ) <_ ( T x. Q ) )
88 80 87 eqbrtrd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) <_ ( T x. Q ) )
89 66 67 70 71 79 88 le2addd
 |-  ( ( ph /\ x e. X ) -> ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) <_ ( ( U x. R ) + ( T x. Q ) ) )
90 59 68 60 69 89 letrd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) <_ ( ( U x. R ) + ( T x. Q ) ) )
91 2nn0
 |-  2 e. NN0
92 91 a1i
 |-  ( ( ph /\ x e. X ) -> 2 e. NN0 )
93 33 34 36 ltled
 |-  ( ( ph /\ x e. X ) -> 0 <_ E )
94 leexp1a
 |-  ( ( ( E e. RR /\ ( abs ` B ) e. RR /\ 2 e. NN0 ) /\ ( 0 <_ E /\ E <_ ( abs ` B ) ) ) -> ( E ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) )
95 34 35 92 93 37 94 syl32anc
 |-  ( ( ph /\ x e. X ) -> ( E ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) )
96 5 92 absexpd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( B ^ 2 ) ) = ( ( abs ` B ) ^ 2 ) )
97 95 96 breqtrrd
 |-  ( ( ph /\ x e. X ) -> ( E ^ 2 ) <_ ( abs ` ( B ^ 2 ) ) )
98 59 60 63 64 65 90 97 lediv12ad
 |-  ( ( ph /\ x e. X ) -> ( ( abs ` ( ( C x. B ) - ( D x. A ) ) ) / ( abs ` ( B ^ 2 ) ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
99 58 98 eqbrtrd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
100 57 99 eqbrtrd
 |-  ( ( ph /\ x e. X ) -> ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
101 100 ralrimiva
 |-  ( ph -> A. x e. X ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) )
102 brralrspcev
 |-  ( ( ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) e. RR /\ A. x e. X ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b )
103 30 101 102 syl2anc
 |-  ( ph -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b )