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. fz0to5un2tp
  15. elfz0ubfz0
  16. elfz0fzfz0
  17. fz0fzelfz0
  18. fznn0sub2
  19. uzsubfz0
  20. fz0fzdiffz0
  21. elfzmlbm
  22. elfzmlbp
  23. fzctr
  24. difelfzle
  25. difelfznle
  26. nn0split
  27. nn0disj
  28. fz0sn0fz1
  29. fvffz0
  30. 1fv
  31. 4fvwrd4
  32. 2ffzeq
  33. preduz
  34. prednn
  35. prednn0
  36. predfz