Metamath Proof Explorer

Theorem dnibndlem9

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem9.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 dnibndlem9.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 dnibndlem9.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 dnibndlem9.4 ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
5 3 dnicld1 ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ )
6 5 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℂ )
7 2 dnicld1 ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
8 7 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℂ )
9 6 8 subcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℂ )
10 9 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ∈ ℝ )
11 halfre ⊢ ( 1 / 2 ) ∈ ℝ
12 11 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
13 12 5 jca ⊢ ( 𝜑 → ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ ) )
14 resubcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ ) → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ∈ ℝ )
15 13 14 syl ⊢ ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ∈ ℝ )
16 12 7 jca ⊢ ( 𝜑 → ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ ) )
17 resubcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ ) → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℝ )
18 16 17 syl ⊢ ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℝ )
19 15 18 readdcld ⊢ ( 𝜑 → ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ∈ ℝ )
20 3 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
21 3 12 readdcld ⊢ ( 𝜑 → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
22 reflcl ⊢ ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
23 21 22 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
24 23 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℂ )
25 12 recnd ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
26 24 25 subcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℂ )
27 20 26 subcld ⊢ ( 𝜑 → ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) ∈ ℂ )
28 2 12 readdcld ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
29 reflcl ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
30 28 29 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
31 30 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ )
32 31 25 addcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℂ )
33 2 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
34 32 33 subcld ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ∈ ℂ )
35 27 34 addcld ⊢ ( 𝜑 → ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ∈ ℂ )
36 35 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) ∈ ℝ )
37 2 3 dnibndlem6 ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) )
38 23 12 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
39 resubcl ⊢ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ )
40 38 39 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ )
41 3 40 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ ) )
42 resubcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ ) → ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) ∈ ℝ )
43 41 42 syl ⊢ ( 𝜑 → ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) ∈ ℝ )
44 30 12 readdcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ )
45 44 2 jca ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
46 resubcl ⊢ ( ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ∈ ℝ )
47 45 46 syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ∈ ℝ )
48 3 dnibndlem7 ⊢ ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )
49 2 dnibndlem8 ⊢ ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ≤ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) )
50 15 18 43 47 48 49 le2addd ⊢ ( 𝜑 → ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) )
51 43 47 readdcld ⊢ ( 𝜑 → ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ∈ ℝ )
52 dnibndlem4 ⊢ ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )
53 3 52 syl ⊢ ( 𝜑 → 0 ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )
54 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
55 dnibndlem5 ⊢ ( 𝐴 ∈ ℝ → 0 < ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) )
56 2 55 syl ⊢ ( 𝜑 → 0 < ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) )
57 54 47 56 ltled ⊢ ( 𝜑 → 0 ≤ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) )
58 43 47 53 57 addge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) )
59 51 58 absidd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) = ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) )
60 59 eqcomd ⊢ ( 𝜑 → ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) = ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) )
61 50 60 breqtrd ⊢ ( 𝜑 → ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) )
62 10 19 36 37 61 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) )
63 1 2 3 4 dnibndlem3 ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) )
64 63 eqcomd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
65 62 64 breqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )
66 1 2 3 dnibndlem1 ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) ↔ ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
67 65 66 mpbird ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝐵 ) − ( 𝑇 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝐵 − 𝐴 ) ) )