Theorem rddif2

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

	Ref	Expression
Assertion	rddif2	$$⊢A\in ℝ\to 0\le \left(\frac{1}{2}\right)-\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$

Proof

Step	Hyp	Ref	Expression
1		rddif	$$⊢A\in ℝ\to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\le \frac{1}{2}$$
2		halfre	$$⊢\frac{1}{2}\in ℝ$$
3	2	a1i	$$⊢A\in ℝ\to \frac{1}{2}\in ℝ$$
4		id	$$⊢A\in ℝ\to A\in ℝ$$
5	4	dnicld1	$$⊢A\in ℝ\to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\in ℝ$$
6	3 5	subge0d	$$⊢A\in ℝ\to \left(0\le \left(\frac{1}{2}\right)-\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\leftrightarrow \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\le \frac{1}{2}\right)$$
7	1 6	mpbird	$$⊢A\in ℝ\to 0\le \left(\frac{1}{2}\right)-\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$