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	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
Assertion	dnif	⊢ 𝑇 : ℝ ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		dnif.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		id	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ )
3	2	dnicld1	⊢ ( 𝑥 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ∈ ℝ )
4	1 3	fmpti	⊢ 𝑇 : ℝ ⟶ ℝ