Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
remuli
Next ⟩
immuli
Metamath Proof Explorer
Ascii
Unicode
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