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