Metamath Proof Explorer

Table of Contents - 5.5.5. Finite intervals of integers

1. cfz
2. df-fz
3. fzval
4. fzval2
5. fzf
6. elfz1
7. elfz
8. elfz2
9. elfzd
10. elfz5
11. elfz4
12. elfzuzb
13. eluzfz
14. elfzuz
15. elfzuz3
16. elfzel2
17. elfzel1
18. elfzelz
19. elfzelzd
20. fzssz
21. elfzle1
22. elfzle2
23. elfzuz2
24. elfzle3
25. eluzfz1
26. eluzfz2
27. eluzfz2b
28. elfz3
29. elfz1eq
30. elfzubelfz
31. peano2fzr
32. fzn0
33. fz0
34. fzn
35. fzen
36. fz1n
37. 0nelfz1
38. 0fz1
39. fz10
40. fz00m1
41. uzsubsubfz
42. uzsubsubfz1
43. ige3m2fz
44. fzsplit2
45. fzsplit
46. fzdisj
47. fz01en
48. elfznn
49. elfz1end
50. fz1ssnn
51. fznn0sub
52. fzmmmeqm
53. fzaddel
54. fzadd2
55. fzsubel
56. fzopth
57. fzass4
58. fzss1
59. fzss2
60. fzssuz
61. fzsn
62. fzssp1
63. fzssnn
64. ssfzunsnext
65. ssfzunsn
66. fzsuc
67. fzpred
68. fzpreddisj
69. elfzp1
70. fzp1ss
71. fzelp1
72. fzp1elp1
73. fznatpl1
74. fzpr
75. fztp
76. fz12pr
77. fzsuc2
78. fzp1disj
79. fzdifsuc
80. fzprval
81. fztpval
82. fzrev
83. fzrev2
84. fzrev2i
85. fzrev3
86. fzrev3i
87. fznn
88. elfz1b
89. elfz1uz
90. elfzm11
91. uzsplit
92. uzdisj
93. fseq1p1m1
94. fseq1m1p1
95. fz1sbc
96. elfzp1b
97. elfzm1b
98. elfzp12
99. fzne1
100. fzdif1
101. fz0dif1
102. fzm1
103. fzneuz
104. fznuz
105. uznfz
106. fzp1nel
107. fzrevral
108. fzrevral2
109. fzrevral3
110. fzshftral
111. ige2m1fz1
112. ige2m1fz