Metamath Proof Explorer

Table of Contents - 15.6.3. Natural numbers

1. cnn0s
2. cnns
3. df-n0s
4. df-nns
5. n0sex
6. nnsex
7. peano5n0s
8. n0ssno
9. nnssn0s
10. nnssno
11. n0sno
12. nnsno
13. n0snod
14. nnsnod
15. nnn0s
16. nnn0sd
17. 0n0s
18. peano2n0s
19. dfn0s2
20. n0sind
21. n0scut
22. n0ons
23. nnne0s
24. n0sge0
25. nnsgt0
26. elnns
27. elnns2
28. n0addscl
29. n0mulscl
30. nnaddscl
31. nnmulscl
32. 1n0s
33. 1nns
34. peano2nns
35. n0sbday
36. n0ssold
37. nnsrecgt0d
38. seqn0sfn
39. eln0s
40. n0s0m1
41. n0subs
42. n0p1nns