Metamath Proof Explorer

Theorem dnibndlem13

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem13.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 dnibndlem13.2 ⊢ φ → A ∈ ℝ
3 dnibndlem13.3 ⊢ φ → B ∈ ℝ
4 dnibndlem13.4 ⊢ φ → A + 1 2 ≤ B + 1 2
5 2 ad2antrr ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 2 ≤ B + 1 2 → A ∈ ℝ
6 3 ad2antrr ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 2 ≤ B + 1 2 → B ∈ ℝ
7 simpr ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 2 ≤ B + 1 2 → A + 1 2 + 2 ≤ B + 1 2
8 1 5 6 7 dnibndlem12 ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 2 ≤ B + 1 2 → T ⁡ B − T ⁡ A ≤ B − A
9 2 ad2antrr ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 1 = B + 1 2 → A ∈ ℝ
10 3 ad2antrr ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 1 = B + 1 2 → B ∈ ℝ
11 simpr ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 1 = B + 1 2 → A + 1 2 + 1 = B + 1 2
12 11 eqcomd ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 1 = B + 1 2 → B + 1 2 = A + 1 2 + 1
13 1 9 10 12 dnibndlem9 ⊢ φ ∧ A + 1 2 < B + 1 2 ∧ A + 1 2 + 1 = B + 1 2 → T ⁡ B − T ⁡ A ≤ B − A
14 simpr ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 < B + 1 2
15 halfre ⊢ 1 2 ∈ ℝ
16 15 a1i ⊢ φ → 1 2 ∈ ℝ
17 2 16 readdcld ⊢ φ → A + 1 2 ∈ ℝ
18 17 flcld ⊢ φ → A + 1 2 ∈ ℤ
19 3 16 readdcld ⊢ φ → B + 1 2 ∈ ℝ
20 19 flcld ⊢ φ → B + 1 2 ∈ ℤ
21 18 20 jca ⊢ φ → A + 1 2 ∈ ℤ ∧ B + 1 2 ∈ ℤ
22 21 adantr ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 ∈ ℤ ∧ B + 1 2 ∈ ℤ
23 zltp1le ⊢ A + 1 2 ∈ ℤ ∧ B + 1 2 ∈ ℤ → A + 1 2 < B + 1 2 ↔ A + 1 2 + 1 ≤ B + 1 2
24 22 23 syl ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 < B + 1 2 ↔ A + 1 2 + 1 ≤ B + 1 2
25 14 24 mpbid ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 + 1 ≤ B + 1 2
26 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
27 17 26 syl ⊢ φ → A + 1 2 ∈ ℝ
28 peano2re ⊢ A + 1 2 ∈ ℝ → A + 1 2 + 1 ∈ ℝ
29 27 28 syl ⊢ φ → A + 1 2 + 1 ∈ ℝ
30 29 adantr ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 + 1 ∈ ℝ
31 20 zred ⊢ φ → B + 1 2 ∈ ℝ
32 31 adantr ⊢ φ ∧ A + 1 2 < B + 1 2 → B + 1 2 ∈ ℝ
33 30 32 leloed ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 + 1 ≤ B + 1 2 ↔ A + 1 2 + 1 < B + 1 2 ∨ A + 1 2 + 1 = B + 1 2
34 25 33 mpbid ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 + 1 < B + 1 2 ∨ A + 1 2 + 1 = B + 1 2
35 18 peano2zd ⊢ φ → A + 1 2 + 1 ∈ ℤ
36 35 20 jca ⊢ φ → A + 1 2 + 1 ∈ ℤ ∧ B + 1 2 ∈ ℤ
37 zltp1le ⊢ A + 1 2 + 1 ∈ ℤ ∧ B + 1 2 ∈ ℤ → A + 1 2 + 1 < B + 1 2 ↔ A + 1 2 + 1 + 1 ≤ B + 1 2
38 36 37 syl ⊢ φ → A + 1 2 + 1 < B + 1 2 ↔ A + 1 2 + 1 + 1 ≤ B + 1 2
39 27 recnd ⊢ φ → A + 1 2 ∈ ℂ
40 1cnd ⊢ φ → 1 ∈ ℂ
41 39 40 40 addassd ⊢ φ → A + 1 2 + 1 + 1 = A + 1 2 + 1 + 1
42 1p1e2 ⊢ 1 + 1 = 2
43 42 a1i ⊢ φ → 1 + 1 = 2
44 43 oveq2d ⊢ φ → A + 1 2 + 1 + 1 = A + 1 2 + 2
45 41 44 eqtrd ⊢ φ → A + 1 2 + 1 + 1 = A + 1 2 + 2
46 45 breq1d ⊢ φ → A + 1 2 + 1 + 1 ≤ B + 1 2 ↔ A + 1 2 + 2 ≤ B + 1 2
47 38 46 bitrd ⊢ φ → A + 1 2 + 1 < B + 1 2 ↔ A + 1 2 + 2 ≤ B + 1 2
48 47 biimpd ⊢ φ → A + 1 2 + 1 < B + 1 2 → A + 1 2 + 2 ≤ B + 1 2
49 48 adantr ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 + 1 < B + 1 2 → A + 1 2 + 2 ≤ B + 1 2
50 49 orim1d ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 + 1 < B + 1 2 ∨ A + 1 2 + 1 = B + 1 2 → A + 1 2 + 2 ≤ B + 1 2 ∨ A + 1 2 + 1 = B + 1 2
51 34 50 mpd ⊢ φ ∧ A + 1 2 < B + 1 2 → A + 1 2 + 2 ≤ B + 1 2 ∨ A + 1 2 + 1 = B + 1 2
52 8 13 51 mpjaodan ⊢ φ ∧ A + 1 2 < B + 1 2 → T ⁡ B − T ⁡ A ≤ B − A
53 2 adantr ⊢ φ ∧ A + 1 2 = B + 1 2 → A ∈ ℝ
54 3 adantr ⊢ φ ∧ A + 1 2 = B + 1 2 → B ∈ ℝ
55 simpr ⊢ φ ∧ A + 1 2 = B + 1 2 → A + 1 2 = B + 1 2
56 55 eqcomd ⊢ φ ∧ A + 1 2 = B + 1 2 → B + 1 2 = A + 1 2
57 1 53 54 56 dnibndlem2 ⊢ φ ∧ A + 1 2 = B + 1 2 → T ⁡ B − T ⁡ A ≤ B − A
58 27 31 leloed ⊢ φ → A + 1 2 ≤ B + 1 2 ↔ A + 1 2 < B + 1 2 ∨ A + 1 2 = B + 1 2
59 4 58 mpbid ⊢ φ → A + 1 2 < B + 1 2 ∨ A + 1 2 = B + 1 2
60 52 57 59 mpjaodan ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A