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	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 ≤ 0 ∨ 1 ≤ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		elznn	⊢ ( 𝑍 ∈ ℤ ↔ ( 𝑍 ∈ ℝ ∧ ( 𝑍 ∈ ℕ ∨ - 𝑍 ∈ ℕ0 ) ) )
2		nnge1	⊢ ( 𝑍 ∈ ℕ → 1 ≤ 𝑍 )
3	2	a1i	⊢ ( 𝑍 ∈ ℝ → ( 𝑍 ∈ ℕ → 1 ≤ 𝑍 ) )
4		elnn0z	⊢ ( - 𝑍 ∈ ℕ0 ↔ ( - 𝑍 ∈ ℤ ∧ 0 ≤ - 𝑍 ) )
5		le0neg1	⊢ ( 𝑍 ∈ ℝ → ( 𝑍 ≤ 0 ↔ 0 ≤ - 𝑍 ) )
6	5	biimprd	⊢ ( 𝑍 ∈ ℝ → ( 0 ≤ - 𝑍 → 𝑍 ≤ 0 ) )
7	6	adantld	⊢ ( 𝑍 ∈ ℝ → ( ( - 𝑍 ∈ ℤ ∧ 0 ≤ - 𝑍 ) → 𝑍 ≤ 0 ) )
8	4 7	biimtrid	⊢ ( 𝑍 ∈ ℝ → ( - 𝑍 ∈ ℕ0 → 𝑍 ≤ 0 ) )
9	3 8	orim12d	⊢ ( 𝑍 ∈ ℝ → ( ( 𝑍 ∈ ℕ ∨ - 𝑍 ∈ ℕ0 ) → ( 1 ≤ 𝑍 ∨ 𝑍 ≤ 0 ) ) )
10	9	imp	⊢ ( ( 𝑍 ∈ ℝ ∧ ( 𝑍 ∈ ℕ ∨ - 𝑍 ∈ ℕ0 ) ) → ( 1 ≤ 𝑍 ∨ 𝑍 ≤ 0 ) )
11	10	orcomd	⊢ ( ( 𝑍 ∈ ℝ ∧ ( 𝑍 ∈ ℕ ∨ - 𝑍 ∈ ℕ0 ) ) → ( 𝑍 ≤ 0 ∨ 1 ≤ 𝑍 ) )
12	1 11	sylbi	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 ≤ 0 ∨ 1 ≤ 𝑍 ) )