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 = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
Assertion	dnival	|- ( A e. RR -> ( T ` A ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )

Proof

Step	Hyp	Ref	Expression
1		dnival.1	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		fvoveq1	|- ( x = A -> ( |_ ` ( x + ( 1 / 2 ) ) ) = ( |_ ` ( A + ( 1 / 2 ) ) ) )
3		id	|- ( x = A -> x = A )
4	2 3	oveq12d	|- ( x = A -> ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) )
5	4	fveq2d	|- ( x = A -> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
6		fvex	|- ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. _V
7	5 1 6	fvmpt	|- ( A e. RR -> ( T ` A ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )