Metamath Proof Explorer

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 ∈ ℤ → Z ≤ 0 ∨ 1 ≤ Z

Proof

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