Theorem dnicld2

Description: Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021)

	Ref	Expression
Hypotheses	dnicld2.1	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	dnicld2.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion	dnicld2	⊢ ( 𝜑 → ( 𝑇 ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		dnicld2.1	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		dnicld2.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3	1	dnival	⊢ ( 𝐴 ∈ ℝ → ( 𝑇 ‘ 𝐴 ) = ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) )
4	2 3	syl	⊢ ( 𝜑 → ( 𝑇 ‘ 𝐴 ) = ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) )
5	2	dnicld1	⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
6	4 5	eqeltrd	⊢ ( 𝜑 → ( 𝑇 ‘ 𝐴 ) ∈ ℝ )