Description: Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002) Reduce dependencies on axioms. (Revised by Steven Nguyen, 29-Nov-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nnssz | |- NN C_ ZZ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnre | |- ( x e. NN -> x e. RR ) |
|
| 2 | 3mix2 | |- ( x e. NN -> ( x = 0 \/ x e. NN \/ -u x e. NN ) ) |
|
| 3 | elz | |- ( x e. ZZ <-> ( x e. RR /\ ( x = 0 \/ x e. NN \/ -u x e. NN ) ) ) |
|
| 4 | 1 2 3 | sylanbrc | |- ( x e. NN -> x e. ZZ ) |
| 5 | 4 | ssriv | |- NN C_ ZZ |