Theorem nnne1ge2

Description: A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	nnne1ge2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
2	1	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 𝑁 ∈ ℕ0 )
3		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
4	3	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 𝑁 ≠ 0 )
5		simpr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 𝑁 ≠ 1 )
6		nn0n0n1ge2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )
7	2 4 5 6	syl3anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )