Step |
Hyp |
Ref |
Expression |
1 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
2 |
|
ltp1 |
|- ( N e. RR -> N < ( N + 1 ) ) |
3 |
|
id |
|- ( N e. RR -> N e. RR ) |
4 |
|
peano2re |
|- ( N e. RR -> ( N + 1 ) e. RR ) |
5 |
3 4
|
ltnled |
|- ( N e. RR -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) ) |
6 |
2 5
|
mpbid |
|- ( N e. RR -> -. ( N + 1 ) <_ N ) |
7 |
1 6
|
syl |
|- ( N e. ZZ -> -. ( N + 1 ) <_ N ) |
8 |
7
|
intnand |
|- ( N e. ZZ -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) |
9 |
8
|
3ad2ant2 |
|- ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) |
10 |
|
elfz2 |
|- ( ( N + 1 ) e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) /\ ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) ) |
11 |
10
|
notbii |
|- ( -. ( N + 1 ) e. ( M ... N ) <-> -. ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) /\ ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) ) |
12 |
|
imnan |
|- ( ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) <-> -. ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) /\ ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) ) |
13 |
11 12
|
bitr4i |
|- ( -. ( N + 1 ) e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) ) |
14 |
9 13
|
mpbir |
|- -. ( N + 1 ) e. ( M ... N ) |