Metamath Proof Explorer


Theorem dnif

Description: The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypothesis dnif.t T = x x + 1 2 x
Assertion dnif T :

Proof

Step Hyp Ref Expression
1 dnif.t T = x x + 1 2 x
2 id x x
3 2 dnicld1 x x + 1 2 x
4 1 3 fmpti T :