Metamath Proof Explorer

Theorem dnibndlem2

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem2.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 dnibndlem2.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 dnibndlem2.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 dnibndlem2.4 ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) = ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) )
5 halfre ⊢ ( 1 / 2 ) ∈ ℝ
6 5 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
7 3 6 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
8 readdcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
9 7 8 syl ⊢ ( 𝜑 → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
10 reflcl ⊢ ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
11 9 10 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
12 11 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℂ )
13 3 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
14 12 13 subcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ∈ ℂ )
15 14 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ )
16 15 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℂ )
17 4 12 eqeltrrd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ )
18 2 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
19 17 18 subcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ∈ ℂ )
20 19 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
21 20 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℂ )
22 16 21 subcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℂ )
23 22 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ∈ ℝ )
24 14 19 subcld ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℂ )
25 24 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℝ )
26 13 18 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
27 26 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ )
28 14 19 abs2difabsd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )
29 12 18 13 nnncan1d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
30 29 eqcomd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) )
31 30 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) )
32 4 oveq1d ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐴 ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) )
33 32 oveq1d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) = ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) )
34 33 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) = ( abs ‘ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) )
35 19 14 abssubd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) = ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )
36 31 34 35 3eqtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )
37 27 leidd ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
38 36 37 eqbrtrrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
39 23 25 27 28 38 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
40 1 2 3 dnibndlem1 ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) ↔ ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
41 39 40 mpbird ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )