Metamath Proof Explorer

Theorem dnibndlem12

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

Ref Expression
Hypotheses dnibndlem12.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
dnibndlem12.2 ⊢ φ → A ∈ ℝ
dnibndlem12.3 ⊢ φ → B ∈ ℝ
dnibndlem12.4 ⊢ φ → A + 1 2 + 2 ≤ B + 1 2
Assertion dnibndlem12 ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A

Proof

Step Hyp Ref Expression
1 dnibndlem12.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 dnibndlem12.2 ⊢ φ → A ∈ ℝ
3 dnibndlem12.3 ⊢ φ → B ∈ ℝ
4 dnibndlem12.4 ⊢ φ → A + 1 2 + 2 ≤ B + 1 2
5 3 dnicld1 ⊢ φ → B + 1 2 − B ∈ ℝ
6 2 dnicld1 ⊢ φ → A + 1 2 − A ∈ ℝ
7 5 6 resubcld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℝ
8 7 recnd ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℂ
9 8 abscld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℝ
10 1red ⊢ φ → 1 ∈ ℝ
11 3 2 resubcld ⊢ φ → B − A ∈ ℝ
12 11 recnd ⊢ φ → B − A ∈ ℂ
13 12 abscld ⊢ φ → B − A ∈ ℝ
14 10 rehalfcld ⊢ φ → 1 2 ∈ ℝ
15 2 3 dnibndlem11 ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ 1 2
16 halflt1 ⊢ 1 2 < 1
17 halfre ⊢ 1 2 ∈ ℝ
18 1re ⊢ 1 ∈ ℝ
19 17 18 pm3.2i ⊢ 1 2 ∈ ℝ ∧ 1 ∈ ℝ
20 ltle ⊢ 1 2 ∈ ℝ ∧ 1 ∈ ℝ → 1 2 < 1 → 1 2 ≤ 1
21 19 20 ax-mp ⊢ 1 2 < 1 → 1 2 ≤ 1
22 16 21 ax-mp ⊢ 1 2 ≤ 1
23 22 a1i ⊢ φ → 1 2 ≤ 1
24 9 14 10 15 23 letrd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ 1
25 2 3 4 dnibndlem10 ⊢ φ → 1 ≤ B − A
26 11 leabsd ⊢ φ → B − A ≤ B − A
27 10 11 13 25 26 letrd ⊢ φ → 1 ≤ B − A
28 9 10 13 24 27 letrd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ B − A
29 1 2 3 dnibndlem1 ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A ↔ B + 1 2 − B − A + 1 2 − A ≤ B − A
30 28 29 mpbird ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A