This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑍 ∈ ℤ → ( 𝑍 ≤ 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 ≤ 𝑍 ) )