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. zgt0ge1
60. nnleltp1
61. nnltp1le
62. nnaddm1cl
63. nn0ltp1le
64. nn0leltp1
65. nn0ltlem1
66. nn0sub2
67. nn0lt10b
68. nn0lt2
69. nn0le2is012
70. nn0lem1lt
71. nnlem1lt
72. nnltlem1
73. nnm1ge0
74. nn0ge0div
75. zdiv
76. zdivadd
77. zdivmul
78. zextle
79. zextlt
80. recnz
81. btwnnz
82. gtndiv
83. halfnz
84. 3halfnz
85. suprzcl
86. prime
87. msqznn
88. zneo
89. nneo
90. nneoi
91. zeo
92. zeo2
93. peano2uz2
94. peano5uzi
95. peano5uzti
96. dfuzi
97. uzind
98. uzind2
99. uzind3
100. nn0ind
101. nn0indALT
102. nn0indd
103. fzind
104. fnn0ind
105. nn0ind-raph
106. zindd
107. fzindd
108. btwnz
109. zred
110. zcnd
111. znegcld
112. peano2zd
113. zaddcld
114. zsubcld
115. zmulcld
116. znnn0nn
117. zadd2cl
118. zriotaneg
119. suprfinzcl