Theorem elnn1uz2

Description: A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012)

	Ref	Expression
Assertion	elnn1uz2	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluz2b3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
2	1	orbi2i	⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ↔ ( 𝑁 = 1 ∨ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) ) )
3		exmidne	⊢ ( 𝑁 = 1 ∨ 𝑁 ≠ 1 )
4		ordi	⊢ ( ( 𝑁 = 1 ∨ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) ) ↔ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ℕ ) ∧ ( 𝑁 = 1 ∨ 𝑁 ≠ 1 ) ) )
5	3 4	mpbiran2	⊢ ( ( 𝑁 = 1 ∨ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) ) ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ℕ ) )
6		1nn	⊢ 1 ∈ ℕ
7		eleq1	⊢ ( 𝑁 = 1 → ( 𝑁 ∈ ℕ ↔ 1 ∈ ℕ ) )
8	6 7	mpbiri	⊢ ( 𝑁 = 1 → 𝑁 ∈ ℕ )
9		pm2.621	⊢ ( ( 𝑁 = 1 → 𝑁 ∈ ℕ ) → ( ( 𝑁 = 1 ∨ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ ) )
10	8 9	ax-mp	⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
11		olc	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ∨ 𝑁 ∈ ℕ ) )
12	10 11	impbii	⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ℕ ) ↔ 𝑁 ∈ ℕ )
13	2 5 12	3bitrri	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )