Metamath Proof Explorer


Theorem remul

Description: Real part of a product. (Contributed by NM, 28-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion remul A B A B = A B A B

Proof

Step Hyp Ref Expression
1 remullem A B A B = A B A B A B = A B + A B A B = A B
2 1 simp1d A B A B = A B A B