Description: If an integer is greater than 3, then it is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | eluzge3nn | |- ( N e. ( ZZ>= ` 3 ) -> N e. NN ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1z | |- 1 e. ZZ |
|
2 | 1le3 | |- 1 <_ 3 |
|
3 | eluzuzle | |- ( ( 1 e. ZZ /\ 1 <_ 3 ) -> ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 1 ) ) ) |
|
4 | 1 2 3 | mp2an | |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 1 ) ) |
5 | elnnuz | |- ( N e. NN <-> N e. ( ZZ>= ` 1 ) ) |
|
6 | 4 5 | sylibr | |- ( N e. ( ZZ>= ` 3 ) -> N e. NN ) |