Metamath Proof Explorer

Theorem dnibndlem8

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

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

Proof

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