Metamath Proof Explorer

Theorem dnibndlem10

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypotheses dnibndlem10.1 ⊢ φ → A ∈ ℝ
dnibndlem10.2 ⊢ φ → B ∈ ℝ
dnibndlem10.3 ⊢ φ → A + 1 2 + 2 ≤ B + 1 2
Assertion dnibndlem10 ⊢ φ → 1 ≤ B − A

Proof

Step Hyp Ref Expression
1 dnibndlem10.1 ⊢ φ → A ∈ ℝ
2 dnibndlem10.2 ⊢ φ → B ∈ ℝ
3 dnibndlem10.3 ⊢ φ → A + 1 2 + 2 ≤ B + 1 2
4 1red ⊢ φ → 1 ∈ ℝ
5 halfre ⊢ 1 2 ∈ ℝ
6 5 a1i ⊢ φ → 1 2 ∈ ℝ
7 2 6 readdcld ⊢ φ → B + 1 2 ∈ ℝ
8 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
9 7 8 syl ⊢ φ → B + 1 2 ∈ ℝ
10 9 6 jca ⊢ φ → B + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ
11 resubcl ⊢ B + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ → B + 1 2 − 1 2 ∈ ℝ
12 10 11 syl ⊢ φ → B + 1 2 − 1 2 ∈ ℝ
13 1 6 readdcld ⊢ φ → A + 1 2 ∈ ℝ
14 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
15 13 14 syl ⊢ φ → A + 1 2 ∈ ℝ
16 15 6 readdcld ⊢ φ → A + 1 2 + 1 2 ∈ ℝ
17 12 16 jca ⊢ φ → B + 1 2 − 1 2 ∈ ℝ ∧ A + 1 2 + 1 2 ∈ ℝ
18 resubcl ⊢ B + 1 2 − 1 2 ∈ ℝ ∧ A + 1 2 + 1 2 ∈ ℝ → B + 1 2 - 1 2 - A + 1 2 + 1 2 ∈ ℝ
19 17 18 syl ⊢ φ → B + 1 2 - 1 2 - A + 1 2 + 1 2 ∈ ℝ
20 2 1 resubcld ⊢ φ → B − A ∈ ℝ
21 15 recnd ⊢ φ → A + 1 2 ∈ ℂ
22 2cnd ⊢ φ → 2 ∈ ℂ
23 6 recnd ⊢ φ → 1 2 ∈ ℂ
24 21 22 23 addsubassd ⊢ φ → A + 1 2 + 2 - 1 2 = A + 1 2 + 2 - 1 2
25 24 oveq1d ⊢ φ → A + 1 2 + 2 - 1 2 - A + 1 2 + 1 2 = A + 1 2 + 2 − 1 2 - A + 1 2 + 1 2
26 22 23 subcld ⊢ φ → 2 − 1 2 ∈ ℂ
27 21 26 23 pnpcand ⊢ φ → A + 1 2 + 2 − 1 2 - A + 1 2 + 1 2 = 2 - 1 2 - 1 2
28 22 23 23 subsub4d ⊢ φ → 2 - 1 2 - 1 2 = 2 − 1 2 + 1 2
29 ax-1cn ⊢ 1 ∈ ℂ
30 2halves ⊢ 1 ∈ ℂ → 1 2 + 1 2 = 1
31 29 30 ax-mp ⊢ 1 2 + 1 2 = 1
32 31 a1i ⊢ φ → 1 2 + 1 2 = 1
33 32 oveq2d ⊢ φ → 2 − 1 2 + 1 2 = 2 − 1
34 2m1e1 ⊢ 2 − 1 = 1
35 34 a1i ⊢ φ → 2 − 1 = 1
36 28 33 35 3eqtrd ⊢ φ → 2 - 1 2 - 1 2 = 1
37 25 27 36 3eqtrd ⊢ φ → A + 1 2 + 2 - 1 2 - A + 1 2 + 1 2 = 1
38 37 eqcomd ⊢ φ → 1 = A + 1 2 + 2 - 1 2 - A + 1 2 + 1 2
39 2re ⊢ 2 ∈ ℝ
40 39 a1i ⊢ φ → 2 ∈ ℝ
41 15 40 readdcld ⊢ φ → A + 1 2 + 2 ∈ ℝ
42 41 6 jca ⊢ φ → A + 1 2 + 2 ∈ ℝ ∧ 1 2 ∈ ℝ
43 resubcl ⊢ A + 1 2 + 2 ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 + 2 - 1 2 ∈ ℝ
44 42 43 syl ⊢ φ → A + 1 2 + 2 - 1 2 ∈ ℝ
45 41 9 6 3 lesub1dd ⊢ φ → A + 1 2 + 2 - 1 2 ≤ B + 1 2 − 1 2
46 44 12 16 45 lesub1dd ⊢ φ → A + 1 2 + 2 - 1 2 - A + 1 2 + 1 2 ≤ B + 1 2 - 1 2 - A + 1 2 + 1 2
47 38 46 eqbrtrd ⊢ φ → 1 ≤ B + 1 2 - 1 2 - A + 1 2 + 1 2
48 flle ⊢ B + 1 2 ∈ ℝ → B + 1 2 ≤ B + 1 2
49 7 48 syl ⊢ φ → B + 1 2 ≤ B + 1 2
50 9 6 2 lesubaddd ⊢ φ → B + 1 2 − 1 2 ≤ B ↔ B + 1 2 ≤ B + 1 2
51 49 50 mpbird ⊢ φ → B + 1 2 − 1 2 ≤ B
52 fllep1 ⊢ A + 1 2 ∈ ℝ → A + 1 2 ≤ A + 1 2 + 1
53 13 52 syl ⊢ φ → A + 1 2 ≤ A + 1 2 + 1
54 21 23 23 addassd ⊢ φ → A + 1 2 + 1 2 + 1 2 = A + 1 2 + 1 2 + 1 2
55 32 oveq2d ⊢ φ → A + 1 2 + 1 2 + 1 2 = A + 1 2 + 1
56 54 55 eqtrd ⊢ φ → A + 1 2 + 1 2 + 1 2 = A + 1 2 + 1
57 56 eqcomd ⊢ φ → A + 1 2 + 1 = A + 1 2 + 1 2 + 1 2
58 53 57 breqtrd ⊢ φ → A + 1 2 ≤ A + 1 2 + 1 2 + 1 2
59 1 16 6 leadd1d ⊢ φ → A ≤ A + 1 2 + 1 2 ↔ A + 1 2 ≤ A + 1 2 + 1 2 + 1 2
60 58 59 mpbird ⊢ φ → A ≤ A + 1 2 + 1 2
61 12 1 2 16 51 60 le2subd ⊢ φ → B + 1 2 - 1 2 - A + 1 2 + 1 2 ≤ B − A
62 4 19 20 47 61 letrd ⊢ φ → 1 ≤ B − A