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

Proof

Step Hyp Ref Expression
1 dnif.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 id 
 |-  ( x e. RR -> x e. RR )
3 2 dnicld1 
 |-  ( x e. RR -> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) e. RR )
4 1 3 fmpti 
 |-  T : RR --> RR