Metamath Proof Explorer

Theorem dnibndlem2

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem2.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 dnibndlem2.2 ⊢ φ → A ∈ ℝ
3 dnibndlem2.3 ⊢ φ → B ∈ ℝ
4 dnibndlem2.4 ⊢ φ → B + 1 2 = A + 1 2
5 halfre ⊢ 1 2 ∈ ℝ
6 5 a1i ⊢ φ → 1 2 ∈ ℝ
7 3 6 jca ⊢ φ → B ∈ ℝ ∧ 1 2 ∈ ℝ
8 readdcl ⊢ B ∈ ℝ ∧ 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
9 7 8 syl ⊢ φ → B + 1 2 ∈ ℝ
10 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
11 9 10 syl ⊢ φ → B + 1 2 ∈ ℝ
12 11 recnd ⊢ φ → B + 1 2 ∈ ℂ
13 3 recnd ⊢ φ → B ∈ ℂ
14 12 13 subcld ⊢ φ → B + 1 2 − B ∈ ℂ
15 14 abscld ⊢ φ → B + 1 2 − B ∈ ℝ
16 15 recnd ⊢ φ → B + 1 2 − B ∈ ℂ
17 4 12 eqeltrrd ⊢ φ → A + 1 2 ∈ ℂ
18 2 recnd ⊢ φ → A ∈ ℂ
19 17 18 subcld ⊢ φ → A + 1 2 − A ∈ ℂ
20 19 abscld ⊢ φ → A + 1 2 − A ∈ ℝ
21 20 recnd ⊢ φ → A + 1 2 − A ∈ ℂ
22 16 21 subcld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℂ
23 22 abscld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℝ
24 14 19 subcld ⊢ φ → B + 1 2 - B - A + 1 2 − A ∈ ℂ
25 24 abscld ⊢ φ → B + 1 2 - B - A + 1 2 − A ∈ ℝ
26 13 18 subcld ⊢ φ → B − A ∈ ℂ
27 26 abscld ⊢ φ → B − A ∈ ℝ
28 14 19 abs2difabsd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ B + 1 2 - B - A + 1 2 − A
29 12 18 13 nnncan1d ⊢ φ → B + 1 2 - A - B + 1 2 − B = B − A
30 29 eqcomd ⊢ φ → B − A = B + 1 2 - A - B + 1 2 − B
31 30 fveq2d ⊢ φ → B − A = B + 1 2 - A - B + 1 2 − B
32 4 oveq1d ⊢ φ → B + 1 2 − A = A + 1 2 − A
33 32 oveq1d ⊢ φ → B + 1 2 - A - B + 1 2 − B = A + 1 2 - A - B + 1 2 − B
34 33 fveq2d ⊢ φ → B + 1 2 - A - B + 1 2 − B = A + 1 2 - A - B + 1 2 − B
35 19 14 abssubd ⊢ φ → A + 1 2 - A - B + 1 2 − B = B + 1 2 - B - A + 1 2 − A
36 31 34 35 3eqtrd ⊢ φ → B − A = B + 1 2 - B - A + 1 2 − A
37 27 leidd ⊢ φ → B − A ≤ B − A
38 36 37 eqbrtrrd ⊢ φ → B + 1 2 - B - A + 1 2 − A ≤ B − A
39 23 25 27 28 38 letrd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ B − A
40 1 2 3 dnibndlem1 ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A ↔ B + 1 2 − B − A + 1 2 − A ≤ B − A
41 39 40 mpbird ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A