Metamath Proof Explorer

Theorem dnibndlem12

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem12.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 dnibndlem12.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 dnibndlem12.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 dnibndlem12.4 ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) )
5 3 dnicld1 ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ )
6 2 dnicld1 ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
7 5 6 resubcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℝ )
8 7 recnd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℂ )
9 8 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ∈ ℝ )
10 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
11 3 2 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
12 11 recnd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
13 12 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ )
14 10 rehalfcld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
15 2 3 dnibndlem11 ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( 1 / 2 ) )
16 halflt1 ⊢ ( 1 / 2 ) < 1
17 halfre ⊢ ( 1 / 2 ) ∈ ℝ
18 1re ⊢ 1 ∈ ℝ
19 17 18 pm3.2i ⊢ ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ )
20 ltle ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) < 1 → ( 1 / 2 ) ≤ 1 ) )
21 19 20 ax-mp ⊢ ( ( 1 / 2 ) < 1 → ( 1 / 2 ) ≤ 1 )
22 16 21 ax-mp ⊢ ( 1 / 2 ) ≤ 1
23 22 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ≤ 1 )
24 9 14 10 15 23 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ 1 )
25 2 3 4 dnibndlem10 ⊢ ( 𝜑 → 1 ≤ ( 𝐵 − 𝐴 ) )
26 11 leabsd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
27 10 11 13 25 26 letrd ⊢ ( 𝜑 → 1 ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
28 9 10 13 24 27 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
29 1 2 3 dnibndlem1 ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) ↔ ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
30 28 29 mpbird ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )