Step |
Hyp |
Ref |
Expression |
1 |
|
peano2z |
|- ( M e. ZZ -> ( M + 1 ) e. ZZ ) |
2 |
1
|
3ad2ant1 |
|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( M + 1 ) e. ZZ ) |
3 |
|
peano2z |
|- ( N e. ZZ -> ( N + 1 ) e. ZZ ) |
4 |
3
|
3ad2ant2 |
|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( N + 1 ) e. ZZ ) |
5 |
|
zre |
|- ( M e. ZZ -> M e. RR ) |
6 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
7 |
|
1re |
|- 1 e. RR |
8 |
|
leadd1 |
|- ( ( M e. RR /\ N e. RR /\ 1 e. RR ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) ) |
9 |
7 8
|
mp3an3 |
|- ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) ) |
10 |
5 6 9
|
syl2an |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) ) |
11 |
10
|
biimp3a |
|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( M + 1 ) <_ ( N + 1 ) ) |
12 |
2 4 11
|
3jca |
|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( ( M + 1 ) e. ZZ /\ ( N + 1 ) e. ZZ /\ ( M + 1 ) <_ ( N + 1 ) ) ) |
13 |
|
eluz2 |
|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) |
14 |
|
eluz2 |
|- ( ( N + 1 ) e. ( ZZ>= ` ( M + 1 ) ) <-> ( ( M + 1 ) e. ZZ /\ ( N + 1 ) e. ZZ /\ ( M + 1 ) <_ ( N + 1 ) ) ) |
15 |
12 13 14
|
3imtr4i |
|- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` ( M + 1 ) ) ) |