Metamath Proof Explorer


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 φA
Assertion dnicld1 φA+12A

Proof

Step Hyp Ref Expression
1 dnicld1.1 φA
2 halfre 12
3 2 a1i φ12
4 1 3 jca φA12
5 readdcl A12A+12
6 4 5 syl φA+12
7 reflcl A+12A+12
8 6 7 syl φA+12
9 8 recnd φA+12
10 1 recnd φA
11 9 10 subcld φA+12A
12 11 abscld φA+12A