Metamath Proof Explorer

Table of Contents - 5.4.7. Nonnegative integers (as a subset of complex numbers)

1. cn0
2. df-n0
3. elnn0
4. nnssnn0
5. nn0ssre
6. nn0sscn
7. nn0ex
8. nnnn0
9. nnnn0i
10. nn0re
11. nn0cn
12. nn0rei
13. nn0cni
14. dfn2
15. elnnne0
16. 0nn0
17. 1nn0
18. 2nn0
19. 3nn0
20. 4nn0
21. 5nn0
22. 6nn0
23. 7nn0
24. 8nn0
25. 9nn0
26. nn0ge0
27. nn0nlt0
28. nn0ge0i
29. nn0le0eq0
30. nn0p1gt0
31. nnnn0addcl
32. nn0nnaddcl
33. 0mnnnnn0
34. un0addcl
35. un0mulcl
36. nn0addcl
37. nn0mulcl
38. nn0addcli
39. nn0mulcli
40. nn0p1nn
41. peano2nn0
42. nnm1nn0
43. elnn0nn
44. elnnnn0
45. elnnnn0b
46. elnnnn0c
47. nn0addge1
48. nn0addge2
49. nn0addge1i
50. nn0addge2i
51. nn0sub
52. ltsubnn0
53. nn0negleid
54. difgtsumgt
55. nn0le2xi
56. nn0lele2xi
57. fcdmnn0supp
58. fcdmnn0fsupp
59. fcdmnn0suppg
60. fcdmnn0fsuppg
61. nnnn0d
62. nn0red
63. nn0cnd
64. nn0ge0d
65. nn0addcld
66. nn0mulcld
67. nn0readdcl
68. nn0n0n1ge2
69. nn0n0n1ge2b
70. nn0ge2m1nn
71. nn0ge2m1nn0
72. nn0nndivcl