Metamath Proof Explorer


Theorem reim

Description: The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion reim AA=iA

Proof

Step Hyp Ref Expression
1 ax-icn i
2 mulcl iAiA
3 1 2 mpan AiA
4 imval iAiA=iAi
5 3 4 syl AiA=iAi
6 ine0 i0
7 divcan3 Aii0iAi=A
8 1 6 7 mp3an23 AiAi=A
9 8 fveq2d AiAi=A
10 5 9 eqtr2d AA=iA