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

Proof

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