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. pr01ssre
31. mulridi
32. mullidi
33. addcli
34. mulcli
35. mulcomi
36. mulcomli
37. addassi
38. mulassi
39. adddii
40. adddiri
41. recni
42. readdcli
43. remulcli
44. mulridd
45. mullidd
46. addcld
47. mulcld
48. mulcomd
49. addassd
50. mulassd
51. adddid
52. adddird
53. adddirp1d
54. joinlmuladdmuld
55. recnd
56. readdcld
57. remulcld