Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( N e. NN0 /\ Z e. ZZ ) -> Z e. ZZ ) |
2 |
|
nn0z |
|- ( N e. NN0 -> N e. ZZ ) |
3 |
|
zaddcl |
|- ( ( N e. ZZ /\ Z e. ZZ ) -> ( N + Z ) e. ZZ ) |
4 |
2 3
|
sylan |
|- ( ( N e. NN0 /\ Z e. ZZ ) -> ( N + Z ) e. ZZ ) |
5 |
|
zre |
|- ( Z e. ZZ -> Z e. RR ) |
6 |
|
nn0addge2 |
|- ( ( Z e. RR /\ N e. NN0 ) -> Z <_ ( N + Z ) ) |
7 |
5 6
|
sylan |
|- ( ( Z e. ZZ /\ N e. NN0 ) -> Z <_ ( N + Z ) ) |
8 |
7
|
ancoms |
|- ( ( N e. NN0 /\ Z e. ZZ ) -> Z <_ ( N + Z ) ) |
9 |
|
eluz2 |
|- ( ( N + Z ) e. ( ZZ>= ` Z ) <-> ( Z e. ZZ /\ ( N + Z ) e. ZZ /\ Z <_ ( N + Z ) ) ) |
10 |
1 4 8 9
|
syl3anbrc |
|- ( ( N e. NN0 /\ Z e. ZZ ) -> ( N + Z ) e. ( ZZ>= ` Z ) ) |