Metamath Proof Explorer

Table of Contents - 5.3.3. Multiplication

1. kcnktkm1cn
2. muladd
3. subdi
4. subdir
5. ine0
6. mulneg1
7. mulneg2
8. mulneg12
9. mul2neg
10. submul2
11. mulm1
12. addneg1mul
13. mulsub
14. mulsub2
15. mulm1i
16. mulneg1i
17. mulneg2i
18. mul2negi
19. subdii
20. subdiri
21. muladdi
22. mulm1d
23. mulneg1d
24. mulneg2d
25. mul2negd
26. subdid
27. subdird
28. muladdd
29. mulsubd
30. muls1d
31. mulsubfacd
32. addmulsub
33. subaddmulsub
34. mulsubaddmulsub