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

Proof

Step	Hyp	Ref	Expression
1		dnicld1.1	|- ( ph -> A e. RR )
2		halfre	|- ( 1 / 2 ) e. RR
3	2	a1i	|- ( ph -> ( 1 / 2 ) e. RR )
4	1 3	jca	|- ( ph -> ( A e. RR /\ ( 1 / 2 ) e. RR ) )
5		readdcl	|- ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A + ( 1 / 2 ) ) e. RR )
6	4 5	syl	|- ( ph -> ( A + ( 1 / 2 ) ) e. RR )
7		reflcl	|- ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
8	6 7	syl	|- ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
9	8	recnd	|- ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
10	1	recnd	|- ( ph -> A e. CC )
11	9 10	subcld	|- ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) e. CC )
12	11	abscld	|- ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )