Theorem dnicld1

Description: Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021)

	Ref	Expression
Hypothesis	dnicld1.1	$$⊢\phi \to A\in ℝ$$
Assertion	dnicld1	$$⊢\phi \to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dnicld1.1	$$⊢\phi \to A\in ℝ$$
2		halfre	$$⊢\frac{1}{2}\in ℝ$$
3	2	a1i	$$⊢\phi \to \frac{1}{2}\in ℝ$$
4	1 3	jca	$$⊢\phi \to \left(A\in ℝ\wedge \frac{1}{2}\in ℝ\right)$$
5		readdcl	$$⊢\left(A\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to A+\left(\frac{1}{2}\right)\in ℝ$$
6	4 5	syl	$$⊢\phi \to A+\left(\frac{1}{2}\right)\in ℝ$$
7		reflcl	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
8	6 7	syl	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
9	8	recnd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋\in ℂ$$
10	1	recnd	$$⊢\phi \to A\in ℂ$$
11	9 10	subcld	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋-A\in ℂ$$
12	11	abscld	$$⊢\phi \to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\in ℝ$$