Theorem eluz2gt1

Description: An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020)

	Ref	Expression
Assertion	eluz2gt1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		eluz2b1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )
2	1	simprbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑁 )