Theorem zabs0b

Description: An integer has an absolute value less than 1 iff it is 0. (Contributed by AV, 21-Nov-2025)

	Ref	Expression
Assertion	zabs0b	$$⊢X\in \mathbb{Z}\to \left(\left|X\right|<1\leftrightarrow X=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0abscl	$$⊢X\in \mathbb{Z}\to \left|X\right|\in {\mathbb{N}}_0$$
2		nn0lt10b	$$⊢\left|X\right|\in {\mathbb{N}}_0\to \left(\left|X\right|<1\leftrightarrow \left|X\right|=0\right)$$
3	1 2	syl	$$⊢X\in \mathbb{Z}\to \left(\left|X\right|<1\leftrightarrow \left|X\right|=0\right)$$
4		zcn	$$⊢X\in \mathbb{Z}\to X\in ℂ$$
5	4	abs00ad	$$⊢X\in \mathbb{Z}\to \left(\left|X\right|=0\leftrightarrow X=0\right)$$
6	3 5	bitrd	$$⊢X\in \mathbb{Z}\to \left(\left|X\right|<1\leftrightarrow X=0\right)$$