Theorem rddif2

Description: Variant of rddif . (Contributed by Asger C. Ipsen, 4-Apr-2021)

	Ref	Expression
Assertion	rddif2	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rddif	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ ( 1 / 2 ) )
2		halfre	⊢ ( 1 / 2 ) ∈ ℝ
3	2	a1i	⊢ ( 𝐴 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
4		id	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
5	4	dnicld1	⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
6	3 5	subge0d	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ↔ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ ( 1 / 2 ) ) )
7	1 6	mpbird	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )