Step |
Hyp |
Ref |
Expression |
1 |
|
eluzaddi.1 |
|- M e. ZZ |
2 |
|
eluzaddi.2 |
|- K e. ZZ |
3 |
|
eluzelz |
|- ( N e. ( ZZ>= ` M ) -> N e. ZZ ) |
4 |
|
zaddcl |
|- ( ( N e. ZZ /\ K e. ZZ ) -> ( N + K ) e. ZZ ) |
5 |
3 2 4
|
sylancl |
|- ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ZZ ) |
6 |
1
|
eluz1i |
|- ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) |
7 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
8 |
1
|
zrei |
|- M e. RR |
9 |
2
|
zrei |
|- K e. RR |
10 |
|
leadd1 |
|- ( ( M e. RR /\ N e. RR /\ K e. RR ) -> ( M <_ N <-> ( M + K ) <_ ( N + K ) ) ) |
11 |
8 9 10
|
mp3an13 |
|- ( N e. RR -> ( M <_ N <-> ( M + K ) <_ ( N + K ) ) ) |
12 |
7 11
|
syl |
|- ( N e. ZZ -> ( M <_ N <-> ( M + K ) <_ ( N + K ) ) ) |
13 |
12
|
biimpa |
|- ( ( N e. ZZ /\ M <_ N ) -> ( M + K ) <_ ( N + K ) ) |
14 |
6 13
|
sylbi |
|- ( N e. ( ZZ>= ` M ) -> ( M + K ) <_ ( N + K ) ) |
15 |
|
zaddcl |
|- ( ( M e. ZZ /\ K e. ZZ ) -> ( M + K ) e. ZZ ) |
16 |
1 2 15
|
mp2an |
|- ( M + K ) e. ZZ |
17 |
16
|
eluz1i |
|- ( ( N + K ) e. ( ZZ>= ` ( M + K ) ) <-> ( ( N + K ) e. ZZ /\ ( M + K ) <_ ( N + K ) ) ) |
18 |
5 14 17
|
sylanbrc |
|- ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) ) |