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. 0elpr01
22. 1cnd
23. 1ex
24. 1elpr01
25. cnre
26. mulrid
27. mullid
28. 1re
29. 1red
30. 0re
31. 0red
32. pr01ssre
33. mulridi
34. mullidi
35. addcli
36. mulcli
37. mulcomi
38. mulcomli
39. addassi
40. mulassi
41. adddii
42. adddiri
43. recni
44. readdcli
45. remulcli
46. mulridd
47. mullidd
48. addcld
49. mulcld
50. mulcomd
51. addassd
52. mulassd
53. adddid
54. adddird
55. adddirp1d
56. joinlmuladdmuld
57. recnd
58. readdcld
59. remulcld