Theorem dnizeq0

Description: The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dnizeq0.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		dnizeq0.1	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3	2	zred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4	1	dnival	⊢ ( 𝐴 ∈ ℝ → ( 𝑇 ‘ 𝐴 ) = ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) )
5	3 4	syl	⊢ ( 𝜑 → ( 𝑇 ‘ 𝐴 ) = ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) )
6		halfre	⊢ ( 1 / 2 ) ∈ ℝ
7	6	a1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
8	2 7	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℤ ∧ ( 1 / 2 ) ∈ ℝ ) )
9		flzadd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) = ( 𝐴 + ( ⌊ ‘ ( 1 / 2 ) ) ) )
10	8 9	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) = ( 𝐴 + ( ⌊ ‘ ( 1 / 2 ) ) ) )
11	6	rexri	⊢ ( 1 / 2 ) ∈ ℝ*
12		0re	⊢ 0 ∈ ℝ
13		halfgt0	⊢ 0 < ( 1 / 2 )
14	12 6 13	ltleii	⊢ 0 ≤ ( 1 / 2 )
15		halflt1	⊢ ( 1 / 2 ) < 1
16	11 14 15	3pm3.2i	⊢ ( ( 1 / 2 ) ∈ ℝ* ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 )
17		0xr	⊢ 0 ∈ ℝ*
18		1xr	⊢ 1 ∈ ℝ*
19	17 18	pm3.2i	⊢ ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* )
20		elico1	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 1 / 2 ) ∈ ( 0 [,) 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ* ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
21	19 20	ax-mp	⊢ ( ( 1 / 2 ) ∈ ( 0 [,) 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ* ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) )
22	16 21	mpbir	⊢ ( 1 / 2 ) ∈ ( 0 [,) 1 )
23	22	a1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ( 0 [,) 1 ) )
24		ico01fl0	⊢ ( ( 1 / 2 ) ∈ ( 0 [,) 1 ) → ( ⌊ ‘ ( 1 / 2 ) ) = 0 )
25	23 24	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( 1 / 2 ) ) = 0 )
26	25	oveq2d	⊢ ( 𝜑 → ( 𝐴 + ( ⌊ ‘ ( 1 / 2 ) ) ) = ( 𝐴 + 0 ) )
27	3	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28	27	addid1d	⊢ ( 𝜑 → ( 𝐴 + 0 ) = 𝐴 )
29	26 28	eqtrd	⊢ ( 𝜑 → ( 𝐴 + ( ⌊ ‘ ( 1 / 2 ) ) ) = 𝐴 )
30	10 29	eqtrd	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) = 𝐴 )
31	30	oveq1d	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) = ( 𝐴 − 𝐴 ) )
32	27	subidd	⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = 0 )
33	31 32	eqtrd	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) = 0 )
34	33	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) = ( abs ‘ 0 ) )
35		abs0	⊢ ( abs ‘ 0 ) = 0
36	35	a1i	⊢ ( 𝜑 → ( abs ‘ 0 ) = 0 )
37	34 36	eqtrd	⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) = 0 )
38	5 37	eqtrd	⊢ ( 𝜑 → ( 𝑇 ‘ 𝐴 ) = 0 )