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 ยท ( โ โ ๐ด ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recld.1 | โข ( ๐ โ ๐ด โ โ ) | |
2 | addcj | โข ( ๐ด โ โ โ ( ๐ด + ( โ โ ๐ด ) ) = ( 2 ยท ( โ โ ๐ด ) ) ) | |
3 | 1 2 | syl | โข ( ๐ โ ( ๐ด + ( โ โ ๐ด ) ) = ( 2 ยท ( โ โ ๐ด ) ) ) |