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