Metamath Proof Explorer

Theorem dnibnd

Description: The "distance to nearest integer" function is 1-Lipschitz continuous, i.e., is a short map. (Contributed by Asger C. Ipsen, 4-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 dnibnd.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 dnibnd.2 ⊢ φ → A ∈ ℝ
3 dnibnd.3 ⊢ φ → B ∈ ℝ
4 2 adantr ⊢ φ ∧ A + 1 2 ≤ B + 1 2 → A ∈ ℝ
5 3 adantr ⊢ φ ∧ A + 1 2 ≤ B + 1 2 → B ∈ ℝ
6 simpr ⊢ φ ∧ A + 1 2 ≤ B + 1 2 → A + 1 2 ≤ B + 1 2
7 1 4 5 6 dnibndlem13 ⊢ φ ∧ A + 1 2 ≤ B + 1 2 → T ⁡ B − T ⁡ A ≤ B − A
8 1 3 dnicld2 ⊢ φ → T ⁡ B ∈ ℝ
9 8 recnd ⊢ φ → T ⁡ B ∈ ℂ
10 1 2 dnicld2 ⊢ φ → T ⁡ A ∈ ℝ
11 10 recnd ⊢ φ → T ⁡ A ∈ ℂ
12 9 11 abssubd ⊢ φ → T ⁡ B − T ⁡ A = T ⁡ A − T ⁡ B
13 12 adantr ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → T ⁡ B − T ⁡ A = T ⁡ A − T ⁡ B
14 3 adantr ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → B ∈ ℝ
15 2 adantr ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → A ∈ ℝ
16 simpr ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → B + 1 2 ≤ A + 1 2
17 1 14 15 16 dnibndlem13 ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → T ⁡ A − T ⁡ B ≤ A − B
18 2 recnd ⊢ φ → A ∈ ℂ
19 3 recnd ⊢ φ → B ∈ ℂ
20 18 19 abssubd ⊢ φ → A − B = B − A
21 20 adantr ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → A − B = B − A
22 17 21 breqtrd ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → T ⁡ A − T ⁡ B ≤ B − A
23 13 22 eqbrtrd ⊢ φ ∧ B + 1 2 ≤ A + 1 2 → T ⁡ B − T ⁡ A ≤ B − A
24 halfre ⊢ 1 2 ∈ ℝ
25 24 a1i ⊢ φ → 1 2 ∈ ℝ
26 2 25 readdcld ⊢ φ → A + 1 2 ∈ ℝ
27 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
28 26 27 syl ⊢ φ → A + 1 2 ∈ ℝ
29 3 25 readdcld ⊢ φ → B + 1 2 ∈ ℝ
30 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
31 29 30 syl ⊢ φ → B + 1 2 ∈ ℝ
32 28 31 letrid ⊢ φ → A + 1 2 ≤ B + 1 2 ∨ B + 1 2 ≤ A + 1 2
33 7 23 32 mpjaodan ⊢ φ → T ⁡ B − T ⁡ A ≤ B − A