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

Proof

Step	Hyp	Ref	Expression
1		dnicld2.1	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		dnicld2.2	|- ( ph -> A e. RR )
3	1	dnival	|- ( A e. RR -> ( T ` A ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
4	2 3	syl	|- ( ph -> ( T ` A ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
5	2	dnicld1	|- ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
6	4 5	eqeltrd	|- ( ph -> ( T ` A ) e. RR )