This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 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 ) ) )