Metamath Proof Explorer

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 ⊢N∈ℕ↔N=1∨N∈ℤ≥2

Proof

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