Description: A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of Gleason p. 133. (Contributed by NM, 21-Jan-2007) (Revised by Mario Carneiro, 14-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | addcj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reval | |
|
2 | 1 | oveq2d | |
3 | cjcl | |
|
4 | addcl | |
|
5 | 3 4 | mpdan | |
6 | 2cn | |
|
7 | 2ne0 | |
|
8 | divcan2 | |
|
9 | 6 7 8 | mp3an23 | |
10 | 5 9 | syl | |
11 | 2 10 | eqtr2d | |