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	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	dnizeq0.1	$$⊢\phi \to A\in \mathbb{Z}$$
Assertion	dnizeq0	$$⊢\phi \to T\left(A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		dnizeq0.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		dnizeq0.1	$$⊢\phi \to A\in \mathbb{Z}$$
3	2	zred	$$⊢\phi \to A\in ℝ$$
4	1	dnival	$$⊢A\in ℝ\to T\left(A\right)=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
5	3 4	syl	$$⊢\phi \to T\left(A\right)=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
6		halfre	$$⊢\frac{1}{2}\in ℝ$$
7	6	a1i	$$⊢\phi \to \frac{1}{2}\in ℝ$$
8	2 7	jca	$$⊢\phi \to \left(A\in \mathbb{Z}\wedge \frac{1}{2}\in ℝ\right)$$
9		flzadd	$$⊢\left(A\in \mathbb{Z}\wedge \frac{1}{2}\in ℝ\right)\to ⌊A+\left(\frac{1}{2}\right)⌋=A+⌊\frac{1}{2}⌋$$
10	8 9	syl	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋=A+⌊\frac{1}{2}⌋$$
11	6	rexri	$$⊢\frac{1}{2}\in {ℝ}^{*}$$
12		0re	$$⊢0\in ℝ$$
13		halfgt0	$$⊢0<\frac{1}{2}$$
14	12 6 13	ltleii	$$⊢0\le \frac{1}{2}$$
15		halflt1	$$⊢\frac{1}{2}<1$$
16	11 14 15	3pm3.2i	$$⊢\left(\frac{1}{2}\in {ℝ}^{*}\wedge 0\le \frac{1}{2}\wedge \frac{1}{2}<1\right)$$
17		0xr	$$⊢0\in {ℝ}^{*}$$
18		1xr	$$⊢1\in {ℝ}^{*}$$
19	17 18	pm3.2i	$$⊢\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)$$
20		elico1	$$⊢\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\to \left(\frac{1}{2}\in \left[0,1\right)\leftrightarrow \left(\frac{1}{2}\in {ℝ}^{*}\wedge 0\le \frac{1}{2}\wedge \frac{1}{2}<1\right)\right)$$
21	19 20	ax-mp	$$⊢\frac{1}{2}\in \left[0,1\right)\leftrightarrow \left(\frac{1}{2}\in {ℝ}^{*}\wedge 0\le \frac{1}{2}\wedge \frac{1}{2}<1\right)$$
22	16 21	mpbir	$$⊢\frac{1}{2}\in \left[0,1\right)$$
23	22	a1i	$$⊢\phi \to \frac{1}{2}\in \left[0,1\right)$$
24		ico01fl0	$$⊢\frac{1}{2}\in \left[0,1\right)\to ⌊\frac{1}{2}⌋=0$$
25	23 24	syl	$$⊢\phi \to ⌊\frac{1}{2}⌋=0$$
26	25	oveq2d	$$⊢\phi \to A+⌊\frac{1}{2}⌋=A+0$$
27	3	recnd	$$⊢\phi \to A\in ℂ$$
28	27	addridd	$$⊢\phi \to A+0=A$$
29	26 28	eqtrd	$$⊢\phi \to A+⌊\frac{1}{2}⌋=A$$
30	10 29	eqtrd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋=A$$
31	30	oveq1d	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋-A=A-A$$
32	27	subidd	$$⊢\phi \to A-A=0$$
33	31 32	eqtrd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋-A=0$$
34	33	fveq2d	$$⊢\phi \to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|=\left|0\right|$$
35		abs0	$$⊢\left|0\right|=0$$
36	35	a1i	$$⊢\phi \to \left|0\right|=0$$
37	34 36	eqtrd	$$⊢\phi \to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|=0$$
38	5 37	eqtrd	$$⊢\phi \to T\left(A\right)=0$$