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 ) ) ) )