Metamath Proof Explorer


Theorem immuli

Description: Imaginary part of a product. (Contributed by NM, 28-Jul-1999)

Ref Expression
Hypotheses recl.1 A
readdi.2 B
Assertion immuli A B = A B + A B

Proof

Step Hyp Ref Expression
1 recl.1 A
2 readdi.2 B
3 immul A B A B = A B + A B
4 1 2 3 mp2an A B = A B + A B