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 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
dnibnd.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dnibnd.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion dnibnd ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 dnibnd.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 dnibnd.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 dnibnd.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 2 adantr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) → 𝐴 ∈ ℝ )
5 3 adantr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) → 𝐵 ∈ ℝ )
6 simpr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) )
7 1 4 5 6 dnibndlem13 ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
8 1 3 dnicld2 ⊢ ( 𝜑 → ( 𝑇 ‘ 𝐵 ) ∈ ℝ )
9 8 recnd ⊢ ( 𝜑 → ( 𝑇 ‘ 𝐵 ) ∈ ℂ )
10 1 2 dnicld2 ⊢ ( 𝜑 → ( 𝑇 ‘ 𝐴 ) ∈ ℝ )
11 10 recnd ⊢ ( 𝜑 → ( 𝑇 ‘ 𝐴 ) ∈ ℂ )
12 9 11 abssubd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) = ( abs ‘ ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) = ( abs ‘ ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) ) )
14 3 adantr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → 𝐵 ∈ ℝ )
15 2 adantr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → 𝐴 ∈ ℝ )
16 simpr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) )
17 1 14 15 16 dnibndlem13 ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝐵 ) ) )
18 2 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
19 3 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
20 18 19 abssubd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
22 17 21 breqtrd ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
23 13 22 eqbrtrd ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
24 halfre ⊢ ( 1 / 2 ) ∈ ℝ
25 24 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
26 2 25 readdcld ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
27 reflcl ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
28 26 27 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
29 3 25 readdcld ⊢ ( 𝜑 → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
30 reflcl ⊢ ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
31 29 30 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
32 28 31 letrid ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∨ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) )
33 7 23 32 mpjaodan ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )