Metamath Proof Explorer


Theorem remuli

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

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

Proof

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