Metamath Proof Explorer


Theorem remul2

Description: Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion remul2 ABAB=AB

Proof

Step Hyp Ref Expression
1 recn AA
2 remul ABAB=ABAB
3 1 2 sylan ABAB=ABAB
4 rere AA=A
5 4 adantr ABA=A
6 5 oveq1d ABAB=AB
7 reim0 AA=0
8 7 oveq1d AAB=0B
9 imcl BB
10 9 recnd BB
11 10 mul02d B0B=0
12 8 11 sylan9eq ABAB=0
13 6 12 oveq12d ABABAB=AB0
14 recl BB
15 14 recnd BB
16 mulcl ABAB
17 1 15 16 syl2an ABAB
18 17 subid1d ABAB0=AB
19 3 13 18 3eqtrd ABAB=AB