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. nnssz
23. nn0ssz
24. nnz
25. nn0z
26. nnzi
27. nn0zi
28. elnnz1
29. znnnlt1
30. nnzrab
31. nn0zrab
32. 1z
33. 1zzd
34. 2z
35. 3z
36. 4z
37. znegcl
38. neg1z
39. znegclb
40. nn0negz
41. nn0negzi
42. zaddcl
43. peano2z
44. zsubcl
45. peano2zm
46. zletr
47. zrevaddcl
48. znnsub
49. znn0sub
50. nzadd
51. zmulcl
52. zltp1le
53. zleltp1
54. zlem1lt
55. zltlem1
56. zgt0ge1
57. nnleltp1
58. nnltp1le
59. nnaddm1cl
60. nn0ltp1le
61. nn0leltp1
62. nn0ltlem1
63. nn0sub2
64. nn0lt10b
65. nn0lt2
66. nn0le2is012
67. nn0lem1lt
68. nnlem1lt
69. nnltlem1
70. nnm1ge0
71. nn0ge0div
72. zdiv
73. zdivadd
74. zdivmul
75. zextle
76. zextlt
77. recnz
78. btwnnz
79. gtndiv
80. halfnz
81. 3halfnz
82. suprzcl
83. prime
84. msqznn
85. zneo
86. nneo
87. nneoi
88. zeo
89. zeo2
90. peano2uz2
91. peano5uzi
92. peano5uzti
93. dfuzi
94. uzind
95. uzind2
96. uzind3
97. nn0ind
98. nn0indALT
99. nn0indd
100. fzind
101. fnn0ind
102. nn0ind-raph
103. zindd
104. btwnz
105. nn0zd
106. nnzd
107. zred
108. zcnd
109. znegcld
110. peano2zd
111. zaddcld
112. zsubcld
113. zmulcld
114. znnn0nn
115. zadd2cl
116. zriotaneg
117. suprfinzcl