Metamath Proof Explorer

Table of Contents - 5.4.9. Integers (as a subset of complex numbers)

1. cz
2. df-z
3. elz
4. nnnegz
5. zre
6. zcn
7. zrei
8. zssre
9. zsscn
10. zex
11. elnnz
12. 0z
13. 0zd
14. elnn0z
15. elznn0nn
16. elznn0
17. elznn
18. zle0orge1
19. elz2
20. dfz2
21. zexALT
22. nnz
23. nnssz
24. nn0ssz
25. nnzOLD
26. nn0z
27. nn0zd
28. nnzd
29. nnzi
30. nn0zi
31. elnnz1
32. znnnlt1
33. nnzrab
34. nn0zrab
35. 1z
36. 1zzd
37. 2z
38. 3z
39. 4z
40. znegcl
41. neg1z
42. znegclb
43. nn0negz
44. nn0negzi
45. zaddcl
46. peano2z
47. zsubcl
48. peano2zm
49. zletr
50. zrevaddcl
51. znnsub
52. znn0sub
53. nzadd
54. zmulcl
55. zltp1le
56. zleltp1
57. zlem1lt
58. zltlem1
59. zltlem1d
60. zgt0ge1
61. nnleltp1
62. nnltp1le
63. nnaddm1cl
64. nn0ltp1le
65. nn0leltp1
66. nn0ltlem1
67. nn0sub2
68. nn0lt10b
69. nn0lt2
70. nn0le2is012
71. nn0lem1lt
72. nnlem1lt
73. nnltlem1
74. nnm1ge0
75. nn0ge0div
76. zdiv
77. zdivadd
78. zdivmul
79. zextle
80. zextlt
81. recnz
82. btwnnz
83. gtndiv
84. halfnz
85. 3halfnz
86. suprzcl
87. prime
88. msqznn
89. zneo
90. nneo
91. nneoi
92. zeo
93. zeo2
94. peano2uz2
95. peano5uzi
96. peano5uzti
97. dfuzi
98. uzind
99. uzind2
100. uzind3
101. nn0ind
102. nn0indALT
103. nn0indd
104. fzind
105. fnn0ind
106. nn0ind-raph
107. zindd
108. fzindd
109. btwnz
110. zred
111. zcnd
112. znegcld
113. peano2zd
114. zaddcld
115. zsubcld
116. zmulcld
117. znnn0nn
118. zadd2cl
119. zriotaneg
120. suprfinzcl