Metamath Proof Explorer

Table of Contents - 5.5.6. Finite intervals of nonnegative integers

Finite intervals of nonnegative integers (or "finite sets of sequential nonnegative integers") are finite intervals of integers with 0 as lower bound: , usually abbreviated by "fz0".

  1. elfz2nn0
  2. fznn0
  3. elfznn0
  4. elfz3nn0
  5. fz0ssnn0
  6. fz1ssfz0
  7. 0elfz
  8. nn0fz0
  9. elfz0add
  10. fz0sn
  11. fz0tp
  12. fz0to3un2pr
  13. fz0to4untppr
  14. elfz0ubfz0
  15. elfz0fzfz0
  16. fz0fzelfz0
  17. fznn0sub2
  18. uzsubfz0
  19. fz0fzdiffz0
  20. elfzmlbm
  21. elfzmlbp
  22. fzctr
  23. difelfzle
  24. difelfznle
  25. nn0split
  26. nn0disj
  27. fz0sn0fz1
  28. fvffz0
  29. 1fv
  30. 4fvwrd4
  31. 2ffzeq
  32. preduz
  33. prednn
  34. prednn0
  35. predfz