Step |
Hyp |
Ref |
Expression |
1 |
|
0lt1 |
|- 0 < 1 |
2 |
|
0re |
|- 0 e. RR |
3 |
|
1re |
|- 1 e. RR |
4 |
2 3
|
ltnlei |
|- ( 0 < 1 <-> -. 1 <_ 0 ) |
5 |
1 4
|
mpbi |
|- -. 1 <_ 0 |
6 |
5
|
intnanr |
|- -. ( 1 <_ 0 /\ 0 <_ N ) |
7 |
6
|
intnan |
|- -. ( ( 1 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 1 <_ 0 /\ 0 <_ N ) ) |
8 |
|
df-nel |
|- ( 0 e/ ( 1 ... N ) <-> -. 0 e. ( 1 ... N ) ) |
9 |
|
elfz2 |
|- ( 0 e. ( 1 ... N ) <-> ( ( 1 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 1 <_ 0 /\ 0 <_ N ) ) ) |
10 |
8 9
|
xchbinx |
|- ( 0 e/ ( 1 ... N ) <-> -. ( ( 1 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 1 <_ 0 /\ 0 <_ N ) ) ) |
11 |
7 10
|
mpbir |
|- 0 e/ ( 1 ... N ) |