Theorem dnicld2

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

	Ref	Expression
Hypotheses	dnicld2.1	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	dnicld2.2	$$⊢\phi \to A\in ℝ$$
Assertion	dnicld2	$$⊢\phi \to T\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dnicld2.1	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		dnicld2.2	$$⊢\phi \to A\in ℝ$$
3	1	dnival	$$⊢A\in ℝ\to T\left(A\right)=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
4	2 3	syl	$$⊢\phi \to T\left(A\right)=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
5	2	dnicld1	$$⊢\phi \to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\in ℝ$$
6	4 5	eqeltrd	$$⊢\phi \to T\left(A\right)\in ℝ$$