Metamath Proof Explorer


Table of Contents - 5.6.9. Factorial function

  1. cfa
  2. df-fac
  3. facnn
  4. fac0
  5. fac1
  6. facp1
  7. fac2
  8. fac3
  9. fac4
  10. facnn2
  11. faccl
  12. faccld
  13. facmapnn
  14. facne0
  15. facdiv
  16. facndiv
  17. facwordi
  18. faclbnd
  19. faclbnd2
  20. faclbnd3
  21. faclbnd4lem1
  22. faclbnd4lem2
  23. faclbnd4lem3
  24. faclbnd4lem4
  25. faclbnd4
  26. faclbnd5
  27. faclbnd6
  28. facubnd
  29. facavg