Description: The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005) (Proof shortened by Mario Carneiro, 29-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | cjreim2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cjreim | |
|
2 | 1 | fveq2d | |
3 | simpl | |
|
4 | 3 | recnd | |
5 | ax-icn | |
|
6 | 5 | a1i | |
7 | simpr | |
|
8 | 7 | recnd | |
9 | 6 8 | mulcld | |
10 | 4 9 | addcld | |
11 | cjcj | |
|
12 | 10 11 | syl | |
13 | 2 12 | eqtr3d | |