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. elimne0
15. adddir
16. 0cn
17. 0cnd
18. c0ex
19. 1cnd
20. 1ex
21. cnre
22. mulid1
23. mulid2
24. 1re
25. 1red
26. 0re
27. 0red
28. mulid1i
29. mulid2i
30. addcli
31. mulcli
32. mulcomi
33. mulcomli
34. addassi
35. mulassi
36. adddii
37. adddiri
38. recni
39. readdcli
40. remulcli
41. mulid1d
42. mulid2d
43. addcld
44. mulcld
45. mulcomd
46. addassd
47. mulassd
48. adddid
49. adddird
50. adddirp1d
51. joinlmuladdmuld
52. recnd
53. readdcld
54. remulcld