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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion	dnicld1	⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		dnicld1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		halfre	⊢ ( 1 / 2 ) ∈ ℝ
3	2	a1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
4	1 3	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
5		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
6	4 5	syl	⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
7		reflcl	⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
8	6 7	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
9	8	recnd	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ )
10	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
11	9 10	subcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ∈ ℂ )
12	11	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )