Metamath Proof Explorer


Theorem addcjd

Description: A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of Gleason p. 133. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypothesis recld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
Assertion addcjd ( ๐œ‘ โ†’ ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) = ( 2 ยท ( โ„œ โ€˜ ๐ด ) ) )

Proof

Step Hyp Ref Expression
1 recld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
2 addcj โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) = ( 2 ยท ( โ„œ โ€˜ ๐ด ) ) )
3 1 2 syl โŠข ( ๐œ‘ โ†’ ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) = ( 2 ยท ( โ„œ โ€˜ ๐ด ) ) )