Metamath Proof Explorer

Theorem dnibndlem7

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

Ref Expression
Hypothesis dnibndlem7.1 ⊢ φ → B ∈ ℝ
Assertion dnibndlem7 ⊢ φ → 1 2 − B + 1 2 − B ≤ B − B + 1 2 − 1 2

Proof

Step Hyp Ref Expression
1 dnibndlem7.1 ⊢ φ → B ∈ ℝ
2 halfre ⊢ 1 2 ∈ ℝ
3 2 a1i ⊢ φ → 1 2 ∈ ℝ
4 1 3 jca ⊢ φ → B ∈ ℝ ∧ 1 2 ∈ ℝ
5 readdcl ⊢ B ∈ ℝ ∧ 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
6 4 5 syl ⊢ φ → B + 1 2 ∈ ℝ
7 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
8 6 7 syl ⊢ φ → B + 1 2 ∈ ℝ
9 8 1 jca ⊢ φ → B + 1 2 ∈ ℝ ∧ B ∈ ℝ
10 resubcl ⊢ B + 1 2 ∈ ℝ ∧ B ∈ ℝ → B + 1 2 − B ∈ ℝ
11 9 10 syl ⊢ φ → B + 1 2 − B ∈ ℝ
12 1 dnicld1 ⊢ φ → B + 1 2 − B ∈ ℝ
13 11 leabsd ⊢ φ → B + 1 2 − B ≤ B + 1 2 − B
14 11 12 3 13 lesub2dd ⊢ φ → 1 2 − B + 1 2 − B ≤ 1 2 − B + 1 2 − B
15 3 recnd ⊢ φ → 1 2 ∈ ℂ
16 8 recnd ⊢ φ → B + 1 2 ∈ ℂ
17 1 recnd ⊢ φ → B ∈ ℂ
18 15 16 17 subsub3d ⊢ φ → 1 2 − B + 1 2 − B = 1 2 + B - B + 1 2
19 15 17 addcomd ⊢ φ → 1 2 + B = B + 1 2
20 19 oveq1d ⊢ φ → 1 2 + B - B + 1 2 = B + 1 2 - B + 1 2
21 17 16 15 subsub3d ⊢ φ → B − B + 1 2 − 1 2 = B + 1 2 - B + 1 2
22 21 eqcomd ⊢ φ → B + 1 2 - B + 1 2 = B − B + 1 2 − 1 2
23 18 20 22 3eqtrd ⊢ φ → 1 2 − B + 1 2 − B = B − B + 1 2 − 1 2
24 14 23 breqtrd ⊢ φ → 1 2 − B + 1 2 − B ≤ B − B + 1 2 − 1 2