Metamath Proof Explorer


Theorem dnibndlem4

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

Ref Expression
Assertion dnibndlem4 ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 id ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ )
2 halfre ( 1 / 2 ) ∈ ℝ
3 2 a1i ( 𝐵 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
4 1 3 readdcld ( 𝐵 ∈ ℝ → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
5 flle ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( 𝐵 + ( 1 / 2 ) ) )
6 4 5 syl ( 𝐵 ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( 𝐵 + ( 1 / 2 ) ) )
7 reflcl ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
8 4 7 syl ( 𝐵 ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
9 8 3 1 lesubaddd ( 𝐵 ∈ ℝ → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ≤ 𝐵 ↔ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( 𝐵 + ( 1 / 2 ) ) ) )
10 6 9 mpbird ( 𝐵 ∈ ℝ → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ≤ 𝐵 )
11 8 3 jca ( 𝐵 ∈ ℝ → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
12 resubcl ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ )
13 11 12 syl ( 𝐵 ∈ ℝ → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ )
14 1 13 subge0d ( 𝐵 ∈ ℝ → ( 0 ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) ↔ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ≤ 𝐵 ) )
15 10 14 mpbird ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) )