Metamath Proof Explorer
Table of Contents - 5.6.9. Factorial function
- cfa
- df-fac
- facnn
- fac0
- fac1
- facp1
- fac2
- fac3
- fac4
- facnn2
- faccl
- faccld
- facmapnn
- facne0
- facdiv
- facndiv
- facwordi
- faclbnd
- faclbnd2
- faclbnd3
- faclbnd4lem1
- faclbnd4lem2
- faclbnd4lem3
- faclbnd4lem4
- faclbnd4
- faclbnd5
- faclbnd6
- facubnd
- facavg