Metamath Proof Explorer

Theorem unbdqndv2lem1

Description: Lemma for unbdqndv2 . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv2lem1.a 
|- ( ph -> A e. CC )
unbdqndv2lem1.b 
|- ( ph -> B e. CC )
unbdqndv2lem1.c 
|- ( ph -> C e. CC )
unbdqndv2lem1.d 
|- ( ph -> D e. CC )
unbdqndv2lem1.e 
|- ( ph -> E e. RR+ )
unbdqndv2lem1.1 
|- ( ph -> D =/= 0 )
unbdqndv2lem1.2 
|- ( ph -> ( 2 x. E ) <_ ( abs ` ( ( A - B ) / D ) ) )
Assertion unbdqndv2lem1 
|- ( ph -> ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) )

Proof

Step Hyp Ref Expression
1 unbdqndv2lem1.a 
 |-  ( ph -> A e. CC )
2 unbdqndv2lem1.b 
 |-  ( ph -> B e. CC )
3 unbdqndv2lem1.c 
 |-  ( ph -> C e. CC )
4 unbdqndv2lem1.d 
 |-  ( ph -> D e. CC )
5 unbdqndv2lem1.e 
 |-  ( ph -> E e. RR+ )
6 unbdqndv2lem1.1 
 |-  ( ph -> D =/= 0 )
7 unbdqndv2lem1.2 
 |-  ( ph -> ( 2 x. E ) <_ ( abs ` ( ( A - B ) / D ) ) )
8 1 2 subcld 
 |-  ( ph -> ( A - B ) e. CC )
9 8 4 6 absdivd 
 |-  ( ph -> ( abs ` ( ( A - B ) / D ) ) = ( ( abs ` ( A - B ) ) / ( abs ` D ) ) )
10 9 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( ( A - B ) / D ) ) = ( ( abs ` ( A - B ) ) / ( abs ` D ) ) )
11 8 abscld 
 |-  ( ph -> ( abs ` ( A - B ) ) e. RR )
12 11 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( A - B ) ) e. RR )
13 1 3 subcld 
 |-  ( ph -> ( A - C ) e. CC )
14 13 abscld 
 |-  ( ph -> ( abs ` ( A - C ) ) e. RR )
15 2 3 subcld 
 |-  ( ph -> ( B - C ) e. CC )
16 15 abscld 
 |-  ( ph -> ( abs ` ( B - C ) ) e. RR )
17 14 16 readdcld 
 |-  ( ph -> ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) e. RR )
18 17 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) e. RR )
19 2re 
 |-  2 e. RR
20 19 a1i 
 |-  ( ph -> 2 e. RR )
21 5 rpred 
 |-  ( ph -> E e. RR )
22 20 21 remulcld 
 |-  ( ph -> ( 2 x. E ) e. RR )
23 4 abscld 
 |-  ( ph -> ( abs ` D ) e. RR )
24 22 23 remulcld 
 |-  ( ph -> ( ( 2 x. E ) x. ( abs ` D ) ) e. RR )
25 24 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( 2 x. E ) x. ( abs ` D ) ) e. RR )
26 1 2 3 abs3difd 
 |-  ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
27 3 2 abssubd 
 |-  ( ph -> ( abs ` ( C - B ) ) = ( abs ` ( B - C ) ) )
28 27 oveq2d 
 |-  ( ph -> ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) = ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) )
29 26 28 breqtrd 
 |-  ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) )
30 29 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) )
31 14 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( A - C ) ) e. RR )
32 16 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( B - C ) ) e. RR )
33 21 23 remulcld 
 |-  ( ph -> ( E x. ( abs ` D ) ) e. RR )
34 33 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( E x. ( abs ` D ) ) e. RR )
35 pm2.45 
 |-  ( -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) -> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) )
36 35 adantl 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) )
37 14 33 ltnled 
 |-  ( ph -> ( ( abs ` ( A - C ) ) < ( E x. ( abs ` D ) ) <-> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) ) )
38 37 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( abs ` ( A - C ) ) < ( E x. ( abs ` D ) ) <-> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) ) )
39 36 38 mpbird 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( A - C ) ) < ( E x. ( abs ` D ) ) )
40 pm2.46 
 |-  ( -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) -> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) )
41 40 adantl 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) )
42 16 33 ltnled 
 |-  ( ph -> ( ( abs ` ( B - C ) ) < ( E x. ( abs ` D ) ) <-> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) )
43 42 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( abs ` ( B - C ) ) < ( E x. ( abs ` D ) ) <-> -. ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) )
44 41 43 mpbird 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( B - C ) ) < ( E x. ( abs ` D ) ) )
45 31 32 34 34 39 44 lt2addd 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) < ( ( E x. ( abs ` D ) ) + ( E x. ( abs ` D ) ) ) )
46 33 recnd 
 |-  ( ph -> ( E x. ( abs ` D ) ) e. CC )
47 46 2timesd 
 |-  ( ph -> ( 2 x. ( E x. ( abs ` D ) ) ) = ( ( E x. ( abs ` D ) ) + ( E x. ( abs ` D ) ) ) )
48 47 eqcomd 
 |-  ( ph -> ( ( E x. ( abs ` D ) ) + ( E x. ( abs ` D ) ) ) = ( 2 x. ( E x. ( abs ` D ) ) ) )
49 20 recnd 
 |-  ( ph -> 2 e. CC )
50 21 recnd 
 |-  ( ph -> E e. CC )
51 23 recnd 
 |-  ( ph -> ( abs ` D ) e. CC )
52 49 50 51 mulassd 
 |-  ( ph -> ( ( 2 x. E ) x. ( abs ` D ) ) = ( 2 x. ( E x. ( abs ` D ) ) ) )
53 52 eqcomd 
 |-  ( ph -> ( 2 x. ( E x. ( abs ` D ) ) ) = ( ( 2 x. E ) x. ( abs ` D ) ) )
54 48 53 eqtrd 
 |-  ( ph -> ( ( E x. ( abs ` D ) ) + ( E x. ( abs ` D ) ) ) = ( ( 2 x. E ) x. ( abs ` D ) ) )
55 54 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( E x. ( abs ` D ) ) + ( E x. ( abs ` D ) ) ) = ( ( 2 x. E ) x. ( abs ` D ) ) )
56 45 55 breqtrd 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) < ( ( 2 x. E ) x. ( abs ` D ) ) )
57 12 18 25 30 56 lelttrd 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( A - B ) ) < ( ( 2 x. E ) x. ( abs ` D ) ) )
58 absgt0 
 |-  ( D e. CC -> ( D =/= 0 <-> 0 < ( abs ` D ) ) )
59 4 58 syl 
 |-  ( ph -> ( D =/= 0 <-> 0 < ( abs ` D ) ) )
60 6 59 mpbid 
 |-  ( ph -> 0 < ( abs ` D ) )
61 23 60 jca 
 |-  ( ph -> ( ( abs ` D ) e. RR /\ 0 < ( abs ` D ) ) )
62 11 22 61 3jca 
 |-  ( ph -> ( ( abs ` ( A - B ) ) e. RR /\ ( 2 x. E ) e. RR /\ ( ( abs ` D ) e. RR /\ 0 < ( abs ` D ) ) ) )
63 ltdivmul2 
 |-  ( ( ( abs ` ( A - B ) ) e. RR /\ ( 2 x. E ) e. RR /\ ( ( abs ` D ) e. RR /\ 0 < ( abs ` D ) ) ) -> ( ( ( abs ` ( A - B ) ) / ( abs ` D ) ) < ( 2 x. E ) <-> ( abs ` ( A - B ) ) < ( ( 2 x. E ) x. ( abs ` D ) ) ) )
64 62 63 syl 
 |-  ( ph -> ( ( ( abs ` ( A - B ) ) / ( abs ` D ) ) < ( 2 x. E ) <-> ( abs ` ( A - B ) ) < ( ( 2 x. E ) x. ( abs ` D ) ) ) )
65 64 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( ( abs ` ( A - B ) ) / ( abs ` D ) ) < ( 2 x. E ) <-> ( abs ` ( A - B ) ) < ( ( 2 x. E ) x. ( abs ` D ) ) ) )
66 57 65 mpbird 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( ( abs ` ( A - B ) ) / ( abs ` D ) ) < ( 2 x. E ) )
67 10 66 eqbrtrd 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> ( abs ` ( ( A - B ) / D ) ) < ( 2 x. E ) )
68 8 4 6 divcld 
 |-  ( ph -> ( ( A - B ) / D ) e. CC )
69 68 abscld 
 |-  ( ph -> ( abs ` ( ( A - B ) / D ) ) e. RR )
70 22 69 lenltd 
 |-  ( ph -> ( ( 2 x. E ) <_ ( abs ` ( ( A - B ) / D ) ) <-> -. ( abs ` ( ( A - B ) / D ) ) < ( 2 x. E ) ) )
71 7 70 mpbid 
 |-  ( ph -> -. ( abs ` ( ( A - B ) / D ) ) < ( 2 x. E ) )
72 71 adantr 
 |-  ( ( ph /\ -. ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) ) -> -. ( abs ` ( ( A - B ) / D ) ) < ( 2 x. E ) )
73 67 72 condan 
 |-  ( ph -> ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) )