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