Metamath Proof Explorer

Theorem dnibndlem4

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

Ref Expression
Assertion dnibndlem4 ⊢ B ∈ ℝ → 0 ≤ B − B + 1 2 − 1 2

Proof

Step Hyp Ref Expression
1 id ⊢ B ∈ ℝ → B ∈ ℝ
2 halfre ⊢ 1 2 ∈ ℝ
3 2 a1i ⊢ B ∈ ℝ → 1 2 ∈ ℝ
4 1 3 readdcld ⊢ B ∈ ℝ → B + 1 2 ∈ ℝ
5 flle ⊢ B + 1 2 ∈ ℝ → B + 1 2 ≤ B + 1 2
6 4 5 syl ⊢ B ∈ ℝ → B + 1 2 ≤ B + 1 2
7 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
8 4 7 syl ⊢ B ∈ ℝ → B + 1 2 ∈ ℝ
9 8 3 1 lesubaddd ⊢ B ∈ ℝ → B + 1 2 − 1 2 ≤ B ↔ B + 1 2 ≤ B + 1 2
10 6 9 mpbird ⊢ B ∈ ℝ → B + 1 2 − 1 2 ≤ B
11 8 3 jca ⊢ B ∈ ℝ → B + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ
12 resubcl ⊢ B + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ → B + 1 2 − 1 2 ∈ ℝ
13 11 12 syl ⊢ B ∈ ℝ → B + 1 2 − 1 2 ∈ ℝ
14 1 13 subge0d ⊢ B ∈ ℝ → 0 ≤ B − B + 1 2 − 1 2 ↔ B + 1 2 − 1 2 ≤ B
15 10 14 mpbird ⊢ B ∈ ℝ → 0 ≤ B − B + 1 2 − 1 2