Metamath Proof Explorer


Theorem immul2

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

Ref Expression
Assertion immul2 A B A B = A B

Proof

Step Hyp Ref Expression
1 recn A A
2 immul A B A B = A B + A B
3 1 2 sylan A B A B = A B + A B
4 rere A A = A
5 4 adantr A B A = A
6 5 oveq1d A B A B = A B
7 reim0 A A = 0
8 7 oveq1d A A B = 0 B
9 recl B B
10 9 recnd B B
11 10 mul02d B 0 B = 0
12 8 11 sylan9eq A B A B = 0
13 6 12 oveq12d A B A B + A B = A B + 0
14 imcl B B
15 14 recnd B B
16 mulcl A B A B
17 1 15 16 syl2an A B A B
18 17 addid1d A B A B + 0 = A B
19 3 13 18 3eqtrd A B A B = A B