Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
immuli
Next ⟩
cjaddi
Metamath Proof Explorer
Ascii
Unicode
Theorem
immuli
Description:
Imaginary part of a product.
(Contributed by
NM
, 28-Jul-1999)
Ref
Expression
Hypotheses
recl.1
⊢
A
∈
ℂ
readdi.2
⊢
B
∈
ℂ
Assertion
immuli
⊢
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B
Proof
Step
Hyp
Ref
Expression
1
recl.1
⊢
A
∈
ℂ
2
readdi.2
⊢
B
∈
ℂ
3
immul
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B
4
1
2
3
mp2an
⊢
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B