Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
immuld
Next ⟩
cjaddd
Metamath Proof Explorer
Ascii
Unicode
Theorem
immuld
Description:
Imaginary part of a product.
(Contributed by
Mario Carneiro
, 29-May-2016)
Ref
Expression
Hypotheses
recld.1
⊢
φ
→
A
∈
ℂ
readdd.2
⊢
φ
→
B
∈
ℂ
Assertion
immuld
⊢
φ
→
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B
Proof
Step
Hyp
Ref
Expression
1
recld.1
⊢
φ
→
A
∈
ℂ
2
readdd.2
⊢
φ
→
B
∈
ℂ
3
immul
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B
4
1
2
3
syl2anc
⊢
φ
→
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B