Metamath Proof Explorer
Description: A number plus its conjugate is twice its real part. Compare Proposition
10-3.4(h) of Gleason p. 133. (Contributed by NM, 2-Oct-1999)
|
|
Ref |
Expression |
|
Hypothesis |
recl.1 |
⊢ 𝐴 ∈ ℂ |
|
Assertion |
addcji |
⊢ ( 𝐴 + ( ∗ ‘ 𝐴 ) ) = ( 2 · ( ℜ ‘ 𝐴 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
recl.1 |
⊢ 𝐴 ∈ ℂ |
2 |
|
addcj |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ∗ ‘ 𝐴 ) ) = ( 2 · ( ℜ ‘ 𝐴 ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( 𝐴 + ( ∗ ‘ 𝐴 ) ) = ( 2 · ( ℜ ‘ 𝐴 ) ) |