Metamath Proof Explorer

Theorem znnnlt1

Description: An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005)

Ref Expression
Assertion znnnlt1 ⊢ N ∈ ℤ → ¬ N ∈ ℕ ↔ N < 1

Proof

Step Hyp Ref Expression
1 elnnz1 ⊢ N ∈ ℕ ↔ N ∈ ℤ ∧ 1 ≤ N
2 1 baib ⊢ N ∈ ℤ → N ∈ ℕ ↔ 1 ≤ N
3 2 notbid ⊢ N ∈ ℤ → ¬ N ∈ ℕ ↔ ¬ 1 ≤ N
4 zre ⊢ N ∈ ℤ → N ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 ltnle ⊢ N ∈ ℝ ∧ 1 ∈ ℝ → N < 1 ↔ ¬ 1 ≤ N
7 4 5 6 sylancl ⊢ N ∈ ℤ → N < 1 ↔ ¬ 1 ≤ N
8 3 7 bitr4d ⊢ N ∈ ℤ → ¬ N ∈ ℕ ↔ N < 1