Metamath Proof Explorer

Table of Contents - 5.2.5. Initial properties of the complex numbers

1. mul12
2. mul32
3. mul31
4. mul4
5. mul4r
6. muladd11
7. 1p1times
8. peano2cn
9. peano2re
10. readdcan
11. 00id
12. mul02lem1
13. mul02lem2
14. mul02
15. mul01
16. addid1
17. cnegex
18. cnegex2
19. addid2
20. addcan
21. addcan2
22. addcom
23. addid1i
24. addid2i
25. mul02i
26. mul01i
27. addcomi
28. addcomli
29. addcani
30. addcan2i
31. mul12i
32. mul32i
33. mul4i
34. mul02d
35. mul01d
36. addid1d
37. addid2d
38. addcomd
39. addcand
40. addcan2d
41. addcanad
42. addcan2ad
43. addneintrd
44. addneintr2d
45. mul12d
46. mul32d
47. mul31d
48. mul4d
49. muladd11r
50. comraddd
51. ltaddneg
52. ltaddnegr