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 ) ) )