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. uzsubsubfz
41. uzsubsubfz1
42. ige3m2fz
43. fzsplit2
44. fzsplit
45. fzdisj
46. fz01en
47. elfznn
48. elfz1end
49. fz1ssnn
50. fznn0sub
51. fzmmmeqm
52. fzaddel
53. fzadd2
54. fzsubel
55. fzopth
56. fzass4
57. fzss1
58. fzss2
59. fzssuz
60. fzsn
61. fzssp1
62. fzssnn
63. ssfzunsnext
64. ssfzunsn
65. fzsuc
66. fzpred
67. fzpreddisj
68. elfzp1
69. fzp1ss
70. fzelp1
71. fzp1elp1
72. fznatpl1
73. fzpr
74. fztp
75. fz12pr
76. fzsuc2
77. fzp1disj
78. fzdifsuc
79. fzprval
80. fztpval
81. fzrev
82. fzrev2
83. fzrev2i
84. fzrev3
85. fzrev3i
86. fznn
87. elfz1b
88. elfz1uz
89. elfzm11
90. uzsplit
91. uzdisj
92. fseq1p1m1
93. fseq1m1p1
94. fz1sbc
95. elfzp1b
96. elfzm1b
97. elfzp12
98. fzm1
99. fzneuz
100. fznuz
101. uznfz
102. fzp1nel
103. fzrevral
104. fzrevral2
105. fzrevral3
106. fzshftral
107. ige2m1fz1
108. ige2m1fz