Metamath Proof Explorer

Table of Contents - 5.6.10. The binomial coefficient operation

1. cbc
2. df-bc
3. bcval
4. bcval2
5. bcval3
6. bcval4
7. bcrpcl
8. bccmpl
9. bcn0
10. bc0k
11. bcnn
12. bcn1
13. bcnp1n
14. bcm1k
15. bcp1n
16. bcp1nk
17. bcval5
18. bcn2
19. bcp1m1
20. bcpasc
21. bccl
22. bccl2
23. bcn2m1
24. bcn2p1
25. permnn
26. bcnm1
27. 4bc3eq4
28. 4bc2eq6