Metamath Proof Explorer

Theorem dnibndlem11

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem11.1 ⊢ φ → A ∈ ℝ
2 dnibndlem11.2 ⊢ φ → B ∈ ℝ
3 2 dnicld1 ⊢ φ → B + 1 2 − B ∈ ℝ
4 1 dnicld1 ⊢ φ → A + 1 2 − A ∈ ℝ
5 3 4 resubcld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℝ
6 halfre ⊢ 1 2 ∈ ℝ
7 6 a1i ⊢ φ → 1 2 ∈ ℝ
8 3 recnd ⊢ φ → B + 1 2 − B ∈ ℂ
9 4 recnd ⊢ φ → A + 1 2 − A ∈ ℂ
10 8 9 negsubdi2d ⊢ φ → − B + 1 2 − B − A + 1 2 − A = A + 1 2 − A − B + 1 2 − B
11 4 3 resubcld ⊢ φ → A + 1 2 − A − B + 1 2 − B ∈ ℝ
12 2 7 readdcld ⊢ φ → B + 1 2 ∈ ℝ
13 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
14 12 13 syl ⊢ φ → B + 1 2 ∈ ℝ
15 14 recnd ⊢ φ → B + 1 2 ∈ ℂ
16 2 recnd ⊢ φ → B ∈ ℂ
17 15 16 subcld ⊢ φ → B + 1 2 − B ∈ ℂ
18 17 absge0d ⊢ φ → 0 ≤ B + 1 2 − B
19 4 3 subge02d ⊢ φ → 0 ≤ B + 1 2 − B ↔ A + 1 2 − A − B + 1 2 − B ≤ A + 1 2 − A
20 18 19 mpbid ⊢ φ → A + 1 2 − A − B + 1 2 − B ≤ A + 1 2 − A
21 rddif ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1 2
22 1 21 syl ⊢ φ → A + 1 2 − A ≤ 1 2
23 11 4 7 20 22 letrd ⊢ φ → A + 1 2 − A − B + 1 2 − B ≤ 1 2
24 10 23 eqbrtrd ⊢ φ → − B + 1 2 − B − A + 1 2 − A ≤ 1 2
25 5 7 24 lenegcon1d ⊢ φ → − 1 2 ≤ B + 1 2 − B − A + 1 2 − A
26 1 7 readdcld ⊢ φ → A + 1 2 ∈ ℝ
27 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
28 26 27 syl ⊢ φ → A + 1 2 ∈ ℝ
29 28 recnd ⊢ φ → A + 1 2 ∈ ℂ
30 1 recnd ⊢ φ → A ∈ ℂ
31 29 30 subcld ⊢ φ → A + 1 2 − A ∈ ℂ
32 31 absge0d ⊢ φ → 0 ≤ A + 1 2 − A
33 3 4 subge02d ⊢ φ → 0 ≤ A + 1 2 − A ↔ B + 1 2 − B − A + 1 2 − A ≤ B + 1 2 − B
34 32 33 mpbid ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ B + 1 2 − B
35 rddif ⊢ B ∈ ℝ → B + 1 2 − B ≤ 1 2
36 2 35 syl ⊢ φ → B + 1 2 − B ≤ 1 2
37 5 3 7 34 36 letrd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ 1 2
38 25 37 jca ⊢ φ → − 1 2 ≤ B + 1 2 − B − A + 1 2 − A ∧ B + 1 2 − B − A + 1 2 − A ≤ 1 2
39 5 7 absled ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ 1 2 ↔ − 1 2 ≤ B + 1 2 − B − A + 1 2 − A ∧ B + 1 2 − B − A + 1 2 − A ≤ 1 2
40 38 39 mpbird ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ 1 2