Theorem dnival

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

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

Proof

Step	Hyp	Ref	Expression
1		dnival.1	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		fvoveq1	$$⊢x=A\to ⌊x+\left(\frac{1}{2}\right)⌋=⌊A+\left(\frac{1}{2}\right)⌋$$
3		id	$$⊢x=A\to x=A$$
4	2 3	oveq12d	$$⊢x=A\to ⌊x+\left(\frac{1}{2}\right)⌋-x=⌊A+\left(\frac{1}{2}\right)⌋-A$$
5	4	fveq2d	$$⊢x=A\to \left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
6		fvex	$$⊢\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\in \mathrm{V}$$
7	5 1 6	fvmpt	$$⊢A\in ℝ\to T\left(A\right)=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$