Theorem eluz2b3

Description: Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012)

	Ref	Expression
Assertion	eluz2b3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eluz2b2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
2		nngt1ne1	⊢ ( 𝑁 ∈ ℕ → ( 1 < 𝑁 ↔ 𝑁 ≠ 1 ) )
3	2	pm5.32i	⊢ ( ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
4	1 3	bitri	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )