Theorem zle0orge1

Description: There is no integer in the open unit interval, i.e., an integer is either less than or equal to 0 or greater than or equal to 1 . (Contributed by AV, 4-Jun-2023)

	Ref	Expression
Assertion	zle0orge1	$$⊢Z\in \mathbb{Z}\to \left(Z\le 0\vee 1\le Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		elznn	$$⊢Z\in \mathbb{Z}\leftrightarrow \left(Z\in ℝ\wedge \left(Z\in \mathbb{N}\vee -Z\in {\mathbb{N}}_0\right)\right)$$
2		nnge1	$$⊢Z\in \mathbb{N}\to 1\le Z$$
3	2	a1i	$$⊢Z\in ℝ\to \left(Z\in \mathbb{N}\to 1\le Z\right)$$
4		elnn0z	$$⊢-Z\in {\mathbb{N}}_0\leftrightarrow \left(-Z\in \mathbb{Z}\wedge 0\le -Z\right)$$
5		le0neg1	$$⊢Z\in ℝ\to \left(Z\le 0\leftrightarrow 0\le -Z\right)$$
6	5	biimprd	$$⊢Z\in ℝ\to \left(0\le -Z\to Z\le 0\right)$$
7	6	adantld	$$⊢Z\in ℝ\to \left(\left(-Z\in \mathbb{Z}\wedge 0\le -Z\right)\to Z\le 0\right)$$
8	4 7	biimtrid	$$⊢Z\in ℝ\to \left(-Z\in {\mathbb{N}}_0\to Z\le 0\right)$$
9	3 8	orim12d	$$⊢Z\in ℝ\to \left(\left(Z\in \mathbb{N}\vee -Z\in {\mathbb{N}}_0\right)\to \left(1\le Z\vee Z\le 0\right)\right)$$
10	9	imp	$$⊢\left(Z\in ℝ\wedge \left(Z\in \mathbb{N}\vee -Z\in {\mathbb{N}}_0\right)\right)\to \left(1\le Z\vee Z\le 0\right)$$
11	10	orcomd	$$⊢\left(Z\in ℝ\wedge \left(Z\in \mathbb{N}\vee -Z\in {\mathbb{N}}_0\right)\right)\to \left(Z\le 0\vee 1\le Z\right)$$
12	1 11	sylbi	$$⊢Z\in \mathbb{Z}\to \left(Z\le 0\vee 1\le Z\right)$$