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 − B D
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 − B D
8 1 2 subcld ⊢ φ → A − B ∈ ℂ
9 8 4 6 absdivd ⊢ φ → A − B D = A − B D
10 9 adantr ⊢ φ ∧ ¬ E ⁢ D ≤ A − C ∨ E ⁢ D ≤ B − C → A − B D = A − B D
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 − B D < 2 ⁢ E ↔ A − B < 2 ⁢ E ⁢ D
64 62 63 syl ⊢ φ → A − B D < 2 ⁢ E ↔ A − B < 2 ⁢ E ⁢ D
65 64 adantr ⊢ φ ∧ ¬ E ⁢ D ≤ A − C ∨ E ⁢ D ≤ B − C → A − B D < 2 ⁢ E ↔ A − B < 2 ⁢ E ⁢ D
66 57 65 mpbird ⊢ φ ∧ ¬ E ⁢ D ≤ A − C ∨ E ⁢ D ≤ B − C → A − B D < 2 ⁢ E
67 10 66 eqbrtrd ⊢ φ ∧ ¬ E ⁢ D ≤ A − C ∨ E ⁢ D ≤ B − C → A − B D < 2 ⁢ E
68 8 4 6 divcld ⊢ φ → A − B D ∈ ℂ
69 68 abscld ⊢ φ → A − B D ∈ ℝ
70 22 69 lenltd ⊢ φ → 2 ⁢ E ≤ A − B D ↔ ¬ A − B D < 2 ⁢ E
71 7 70 mpbid ⊢ φ → ¬ A − B D < 2 ⁢ E
72 71 adantr ⊢ φ ∧ ¬ E ⁢ D ≤ A − C ∨ E ⁢ D ≤ B − C → ¬ A − B D < 2 ⁢ E
73 67 72 condan ⊢ φ → E ⁢ D ≤ A − C ∨ E ⁢ D ≤ B − C