Metamath Proof Explorer

Theorem dnibndlem6

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem6.1 ⊢ φ → A ∈ ℝ
2 dnibndlem6.2 ⊢ φ → B ∈ ℝ
3 2 dnicld1 ⊢ φ → B + 1 2 − B ∈ ℝ
4 3 recnd ⊢ φ → B + 1 2 − B ∈ ℂ
5 1 dnicld1 ⊢ φ → A + 1 2 − A ∈ ℝ
6 5 recnd ⊢ φ → A + 1 2 − A ∈ ℂ
7 4 6 subcld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℂ
8 7 abscld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℝ
9 halfcn ⊢ 1 2 ∈ ℂ
10 9 a1i ⊢ φ → 1 2 ∈ ℂ
11 4 10 subcld ⊢ φ → B + 1 2 − B − 1 2 ∈ ℂ
12 11 abscld ⊢ φ → B + 1 2 − B − 1 2 ∈ ℝ
13 10 6 subcld ⊢ φ → 1 2 − A + 1 2 − A ∈ ℂ
14 13 abscld ⊢ φ → 1 2 − A + 1 2 − A ∈ ℝ
15 12 14 readdcld ⊢ φ → B + 1 2 − B − 1 2 + 1 2 − A + 1 2 − A ∈ ℝ
16 halfre ⊢ 1 2 ∈ ℝ
17 16 a1i ⊢ φ → 1 2 ∈ ℝ
18 17 3 jca ⊢ φ → 1 2 ∈ ℝ ∧ B + 1 2 − B ∈ ℝ
19 resubcl ⊢ 1 2 ∈ ℝ ∧ B + 1 2 − B ∈ ℝ → 1 2 − B + 1 2 − B ∈ ℝ
20 18 19 syl ⊢ φ → 1 2 − B + 1 2 − B ∈ ℝ
21 17 5 jca ⊢ φ → 1 2 ∈ ℝ ∧ A + 1 2 − A ∈ ℝ
22 resubcl ⊢ 1 2 ∈ ℝ ∧ A + 1 2 − A ∈ ℝ → 1 2 − A + 1 2 − A ∈ ℝ
23 21 22 syl ⊢ φ → 1 2 − A + 1 2 − A ∈ ℝ
24 20 23 readdcld ⊢ φ → 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A ∈ ℝ
25 4 6 10 3jca ⊢ φ → B + 1 2 − B ∈ ℂ ∧ A + 1 2 − A ∈ ℂ ∧ 1 2 ∈ ℂ
26 abs3dif ⊢ B + 1 2 − B ∈ ℂ ∧ A + 1 2 − A ∈ ℂ ∧ 1 2 ∈ ℂ → B + 1 2 − B − A + 1 2 − A ≤ B + 1 2 − B − 1 2 + 1 2 − A + 1 2 − A
27 25 26 syl ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ B + 1 2 − B − 1 2 + 1 2 − A + 1 2 − A
28 4 10 abssubd ⊢ φ → B + 1 2 − B − 1 2 = 1 2 − B + 1 2 − B
29 rddif2 ⊢ B ∈ ℝ → 0 ≤ 1 2 − B + 1 2 − B
30 2 29 syl ⊢ φ → 0 ≤ 1 2 − B + 1 2 − B
31 20 30 absidd ⊢ φ → 1 2 − B + 1 2 − B = 1 2 − B + 1 2 − B
32 28 31 eqtrd ⊢ φ → B + 1 2 − B − 1 2 = 1 2 − B + 1 2 − B
33 rddif2 ⊢ A ∈ ℝ → 0 ≤ 1 2 − A + 1 2 − A
34 1 33 syl ⊢ φ → 0 ≤ 1 2 − A + 1 2 − A
35 23 34 absidd ⊢ φ → 1 2 − A + 1 2 − A = 1 2 − A + 1 2 − A
36 32 35 oveq12d ⊢ φ → B + 1 2 − B − 1 2 + 1 2 − A + 1 2 − A = 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A
37 15 36 eqled ⊢ φ → B + 1 2 − B − 1 2 + 1 2 − A + 1 2 − A ≤ 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A
38 8 15 24 27 37 letrd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A