Metamath Proof Explorer


Theorem addcj

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 AA+A=2A

Proof

Step Hyp Ref Expression
1 reval AA=A+A2
2 1 oveq2d A2A=2A+A2
3 cjcl AA
4 addcl AAA+A
5 3 4 mpdan AA+A
6 2cn 2
7 2ne0 20
8 divcan2 A+A2202A+A2=A+A
9 6 7 8 mp3an23 A+A2A+A2=A+A
10 5 9 syl A2A+A2=A+A
11 2 10 eqtr2d AA+A=2A