Metamath Proof Explorer


Theorem dnibndlem7

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

Ref Expression
Hypothesis dnibndlem7.1 ( 𝜑𝐵 ∈ ℝ )
Assertion dnibndlem7 ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 dnibndlem7.1 ( 𝜑𝐵 ∈ ℝ )
2 halfre ( 1 / 2 ) ∈ ℝ
3 2 a1i ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
4 1 3 jca ( 𝜑 → ( 𝐵 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
5 readdcl ( ( 𝐵 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
6 4 5 syl ( 𝜑 → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
7 reflcl ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
8 6 7 syl ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
9 8 1 jca ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
10 resubcl ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ∈ ℝ )
11 9 10 syl ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ∈ ℝ )
12 1 dnicld1 ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ )
13 11 leabsd ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ≤ ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) )
14 11 12 3 13 lesub2dd ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ≤ ( ( 1 / 2 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) )
15 3 recnd ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
16 8 recnd ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℂ )
17 1 recnd ( 𝜑𝐵 ∈ ℂ )
18 15 16 17 subsub3d ( 𝜑 → ( ( 1 / 2 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) = ( ( ( 1 / 2 ) + 𝐵 ) − ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) )
19 15 17 addcomd ( 𝜑 → ( ( 1 / 2 ) + 𝐵 ) = ( 𝐵 + ( 1 / 2 ) ) )
20 19 oveq1d ( 𝜑 → ( ( ( 1 / 2 ) + 𝐵 ) − ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) = ( ( 𝐵 + ( 1 / 2 ) ) − ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) )
21 17 16 15 subsub3d ( 𝜑 → ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) = ( ( 𝐵 + ( 1 / 2 ) ) − ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) )
22 21 eqcomd ( 𝜑 → ( ( 𝐵 + ( 1 / 2 ) ) − ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ) = ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )
23 18 20 22 3eqtrd ( 𝜑 → ( ( 1 / 2 ) − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) = ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )
24 14 23 breqtrd ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )