Metamath Proof Explorer

Table of Contents - 5.4.1. Positive integers (as a subset of complex numbers)

1. cn
2. df-nn
3. nnexALT
4. peano5nni
5. nnssre
6. nnsscn
7. nnex
8. nnre
9. nncn
10. nnrei
11. nncni
12. 1nn
13. peano2nn
14. dfnn2
15. dfnn3
16. nnred
17. nncnd
18. peano2nnd