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 eqtrid 
 |-  ( 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 )