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	⊢ ( 𝑁 ∈ ℤ → ( ¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1 ) )

Proof

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