Metamath Proof Explorer

Theorem dnibndlem13

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

Ref Expression
Hypotheses dnibndlem13.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
dnibndlem13.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dnibndlem13.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dnibndlem13.4 ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) )
Assertion dnibndlem13 ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )

Proof

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