Metamath Proof Explorer

Theorem unbdqndv2lem1

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

Ref Expression
Hypotheses unbdqndv2lem1.a ⊢φ→A∈ℂ
unbdqndv2lem1.b ⊢φ→B∈ℂ
unbdqndv2lem1.c ⊢φ→C∈ℂ
unbdqndv2lem1.d ⊢φ→D∈ℂ
unbdqndv2lem1.e ⊢φ→E∈ℝ+
unbdqndv2lem1.1 ⊢φ→D≠0
unbdqndv2lem1.2 ⊢φ→2⁢E≤A−BD
Assertion unbdqndv2lem1 ⊢φ→E⁢D≤A−C∨E⁢D≤B−C

Proof

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