Metamath Proof Explorer

Table of Contents - 5.2.1. Some deductions from the field axioms for complex numbers

1. cnex
2. addcl
3. readdcl
4. mulcl
5. remulcl
6. mulcom
7. addass
8. mulass
9. adddi
10. recn
11. reex
12. reelprrecn
13. cnelprrecn
14. mpoaddf
15. mpomulf
16. elimne0
17. adddir
18. 0cn
19. 0cnd
20. c0ex
21. 1cnd
22. 1ex
23. cnre
24. mulrid
25. mullid
26. 1re
27. 1red
28. 0re
29. 0red
30. mulridi
31. mullidi
32. addcli
33. mulcli
34. mulcomi
35. mulcomli
36. addassi
37. mulassi
38. adddii
39. adddiri
40. recni
41. readdcli
42. remulcli
43. mulridd
44. mullidd
45. addcld
46. mulcld
47. mulcomd
48. addassd
49. mulassd
50. adddid
51. adddird
52. adddirp1d
53. joinlmuladdmuld
54. recnd
55. readdcld
56. remulcld