Metamath Proof Explorer

Table of Contents - 5.9.3. Real and imaginary parts; conjugate

1. ccj
2. cre
3. cim
4. df-cj
5. df-re
6. df-im
7. cjval
8. cjth
9. cjf
10. cjcl
11. reval
12. imval
13. imre
14. reim
15. recl
16. imcl
17. ref
18. imf
19. crre
20. crim
21. replim
22. remim
23. reim0
24. reim0b
25. rereb
26. mulre
27. rere
28. cjreb
29. recj
30. reneg
31. readd
32. resub
33. remullem
34. remul
35. remul2
36. rediv
37. imcj
38. imneg
39. imadd
40. imsub
41. immul
42. immul2
43. imdiv
44. cjre
45. cjcj
46. cjadd
47. cjmul
48. ipcnval
49. cjmulrcl
50. cjmulval
51. cjmulge0
52. cjneg
53. addcj
54. cjsub
55. cjexp
56. imval2
57. re0
58. im0
59. re1
60. im1
61. rei
62. imi
63. cj0
64. cji
65. cjreim
66. cjreim2
67. cj11
68. cjne0
69. cjdiv
70. cnrecnv
71. sqeqd
72. recli
73. imcli
74. cjcli
75. replimi
76. cjcji
77. reim0bi
78. rerebi
79. cjrebi
80. recji
81. imcji
82. cjmulrcli
83. cjmulvali
84. cjmulge0i
85. renegi
86. imnegi
87. cjnegi
88. addcji
89. readdi
90. imaddi
91. remuli
92. immuli
93. cjaddi
94. cjmuli
95. ipcni
96. cjdivi
97. crrei
98. crimi
99. recld
100. imcld
101. cjcld
102. replimd
103. remimd
104. cjcjd
105. reim0bd
106. rerebd
107. cjrebd
108. cjne0d
109. recjd
110. imcjd
111. cjmulrcld
112. cjmulvald
113. cjmulge0d
114. renegd
115. imnegd
116. cjnegd
117. addcjd
118. cjexpd
119. readdd
120. imaddd
121. resubd
122. imsubd
123. remuld
124. immuld
125. cjaddd
126. cjmuld
127. ipcnd
128. cjdivd
129. rered
130. reim0d
131. cjred
132. remul2d
133. immul2d
134. redivd
135. imdivd
136. crred
137. crimd