Metamath Proof Explorer

Theorem dnibndlem9

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem9.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 dnibndlem9.2 ⊢ φ → A ∈ ℝ
3 dnibndlem9.3 ⊢ φ → B ∈ ℝ
4 dnibndlem9.4 ⊢ φ → B + 1 2 = A + 1 2 + 1
5 3 dnicld1 ⊢ φ → B + 1 2 − B ∈ ℝ
6 5 recnd ⊢ φ → B + 1 2 − B ∈ ℂ
7 2 dnicld1 ⊢ φ → A + 1 2 − A ∈ ℝ
8 7 recnd ⊢ φ → A + 1 2 − A ∈ ℂ
9 6 8 subcld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℂ
10 9 abscld ⊢ φ → B + 1 2 − B − A + 1 2 − A ∈ ℝ
11 halfre ⊢ 1 2 ∈ ℝ
12 11 a1i ⊢ φ → 1 2 ∈ ℝ
13 12 5 jca ⊢ φ → 1 2 ∈ ℝ ∧ B + 1 2 − B ∈ ℝ
14 resubcl ⊢ 1 2 ∈ ℝ ∧ B + 1 2 − B ∈ ℝ → 1 2 − B + 1 2 − B ∈ ℝ
15 13 14 syl ⊢ φ → 1 2 − B + 1 2 − B ∈ ℝ
16 12 7 jca ⊢ φ → 1 2 ∈ ℝ ∧ A + 1 2 − A ∈ ℝ
17 resubcl ⊢ 1 2 ∈ ℝ ∧ A + 1 2 − A ∈ ℝ → 1 2 − A + 1 2 − A ∈ ℝ
18 16 17 syl ⊢ φ → 1 2 − A + 1 2 − A ∈ ℝ
19 15 18 readdcld ⊢ φ → 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A ∈ ℝ
20 3 recnd ⊢ φ → B ∈ ℂ
21 3 12 readdcld ⊢ φ → B + 1 2 ∈ ℝ
22 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
23 21 22 syl ⊢ φ → B + 1 2 ∈ ℝ
24 23 recnd ⊢ φ → B + 1 2 ∈ ℂ
25 12 recnd ⊢ φ → 1 2 ∈ ℂ
26 24 25 subcld ⊢ φ → B + 1 2 − 1 2 ∈ ℂ
27 20 26 subcld ⊢ φ → B − B + 1 2 − 1 2 ∈ ℂ
28 2 12 readdcld ⊢ φ → A + 1 2 ∈ ℝ
29 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
30 28 29 syl ⊢ φ → A + 1 2 ∈ ℝ
31 30 recnd ⊢ φ → A + 1 2 ∈ ℂ
32 31 25 addcld ⊢ φ → A + 1 2 + 1 2 ∈ ℂ
33 2 recnd ⊢ φ → A ∈ ℂ
34 32 33 subcld ⊢ φ → A + 1 2 + 1 2 - A ∈ ℂ
35 27 34 addcld ⊢ φ → B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A ∈ ℂ
36 35 abscld ⊢ φ → B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A ∈ ℝ
37 2 3 dnibndlem6 ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A
38 23 12 jca ⊢ φ → B + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ
39 resubcl ⊢ B + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ → B + 1 2 − 1 2 ∈ ℝ
40 38 39 syl ⊢ φ → B + 1 2 − 1 2 ∈ ℝ
41 3 40 jca ⊢ φ → B ∈ ℝ ∧ B + 1 2 − 1 2 ∈ ℝ
42 resubcl ⊢ B ∈ ℝ ∧ B + 1 2 − 1 2 ∈ ℝ → B − B + 1 2 − 1 2 ∈ ℝ
43 41 42 syl ⊢ φ → B − B + 1 2 − 1 2 ∈ ℝ
44 30 12 readdcld ⊢ φ → A + 1 2 + 1 2 ∈ ℝ
45 44 2 jca ⊢ φ → A + 1 2 + 1 2 ∈ ℝ ∧ A ∈ ℝ
46 resubcl ⊢ A + 1 2 + 1 2 ∈ ℝ ∧ A ∈ ℝ → A + 1 2 + 1 2 - A ∈ ℝ
47 45 46 syl ⊢ φ → A + 1 2 + 1 2 - A ∈ ℝ
48 3 dnibndlem7 ⊢ φ → 1 2 − B + 1 2 − B ≤ B − B + 1 2 − 1 2
49 2 dnibndlem8 ⊢ φ → 1 2 − A + 1 2 − A ≤ A + 1 2 + 1 2 - A
50 15 18 43 47 48 49 le2addd ⊢ φ → 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A ≤ B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
51 43 47 readdcld ⊢ φ → B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A ∈ ℝ
52 dnibndlem4 ⊢ B ∈ ℝ → 0 ≤ B − B + 1 2 − 1 2
53 3 52 syl ⊢ φ → 0 ≤ B − B + 1 2 − 1 2
54 0red ⊢ φ → 0 ∈ ℝ
55 dnibndlem5 ⊢ A ∈ ℝ → 0 < A + 1 2 + 1 2 - A
56 2 55 syl ⊢ φ → 0 < A + 1 2 + 1 2 - A
57 54 47 56 ltled ⊢ φ → 0 ≤ A + 1 2 + 1 2 - A
58 43 47 53 57 addge0d ⊢ φ → 0 ≤ B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
59 51 58 absidd ⊢ φ → B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A = B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
60 59 eqcomd ⊢ φ → B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A = B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
61 50 60 breqtrd ⊢ φ → 1 2 − B + 1 2 − B + 1 2 - A + 1 2 − A ≤ B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
62 10 19 36 37 61 letrd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
63 1 2 3 4 dnibndlem3 ⊢ φ → B − A = B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
64 63 eqcomd ⊢ φ → B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A = B − A
65 62 64 breqtrd ⊢ φ → B + 1 2 − B − A + 1 2 − A ≤ B − A
66 1 2 3 dnibndlem1 ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A ↔ B + 1 2 − B − A + 1 2 − A ≤ B − A
67 65 66 mpbird ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A