Metamath Proof Explorer

Theorem dnibndlem8

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

Ref Expression
Hypothesis dnibndlem8.1 ⊢ φ → A ∈ ℝ
Assertion dnibndlem8 ⊢ φ → 1 2 − A + 1 2 − A ≤ A + 1 2 + 1 2 - A

Proof

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