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