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. nn0z
26. nn0zd
27. nnzd
28. nnzi
29. nn0zi
30. elnnz1
31. znnnlt1
32. nnzrab
33. nn0zrab
34. 1z
35. 1zzd
36. 2z
37. 3z
38. 4z
39. znegcl
40. neg1z
41. znegclb
42. nn0negz
43. nn0negzi
44. zaddcl
45. peano2z
46. zsubcl
47. peano2zm
48. zletr
49. zrevaddcl
50. znnsub
51. znn0sub
52. nzadd
53. zmulcl
54. zltp1le
55. zleltp1
56. zlem1lt
57. zltlem1
58. zltlem1d
59. zltp1led
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