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 ABAB=ABAB

Proof

Step Hyp Ref Expression
1 remullem ABAB=ABABAB=AB+ABAB=AB
2 1 simp1d ABAB=ABAB