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 e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )

Proof

Step Hyp Ref Expression
1 eluz2b3
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
2 1 orbi2i
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) <-> ( N = 1 \/ ( N e. NN /\ N =/= 1 ) ) )
3 exmidne
 |-  ( N = 1 \/ N =/= 1 )
4 ordi
 |-  ( ( N = 1 \/ ( N e. NN /\ N =/= 1 ) ) <-> ( ( N = 1 \/ N e. NN ) /\ ( N = 1 \/ N =/= 1 ) ) )
5 3 4 mpbiran2
 |-  ( ( N = 1 \/ ( N e. NN /\ N =/= 1 ) ) <-> ( N = 1 \/ N e. NN ) )
6 1nn
 |-  1 e. NN
7 eleq1
 |-  ( N = 1 -> ( N e. NN <-> 1 e. NN ) )
8 6 7 mpbiri
 |-  ( N = 1 -> N e. NN )
9 pm2.621
 |-  ( ( N = 1 -> N e. NN ) -> ( ( N = 1 \/ N e. NN ) -> N e. NN ) )
10 8 9 ax-mp
 |-  ( ( N = 1 \/ N e. NN ) -> N e. NN )
11 olc
 |-  ( N e. NN -> ( N = 1 \/ N e. NN ) )
12 10 11 impbii
 |-  ( ( N = 1 \/ N e. NN ) <-> N e. NN )
13 2 5 12 3bitrri
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )