Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
immul2
Next ⟩
imdiv
Metamath Proof Explorer
Ascii
Unicode
Theorem
immul2
Description:
Imaginary part of a product.
(Contributed by
Mario Carneiro
, 2-Aug-2014)
Ref
Expression
Assertion
immul2
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
ℑ
⁡
A
⁢
B
=
A
⁢
ℑ
⁡
B
Proof
Step
Hyp
Ref
Expression
1
recn
⊢
A
∈
ℝ
→
A
∈
ℂ
2
immul
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B
3
1
2
sylan
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
ℑ
⁡
A
⁢
B
=
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B
4
rere
⊢
A
∈
ℝ
→
ℜ
⁡
A
=
A
5
4
adantr
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
ℜ
⁡
A
=
A
6
5
oveq1d
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
ℜ
⁡
A
⁢
ℑ
⁡
B
=
A
⁢
ℑ
⁡
B
7
reim0
⊢
A
∈
ℝ
→
ℑ
⁡
A
=
0
8
7
oveq1d
⊢
A
∈
ℝ
→
ℑ
⁡
A
⁢
ℜ
⁡
B
=
0
⋅
ℜ
⁡
B
9
recl
⊢
B
∈
ℂ
→
ℜ
⁡
B
∈
ℝ
10
9
recnd
⊢
B
∈
ℂ
→
ℜ
⁡
B
∈
ℂ
11
10
mul02d
⊢
B
∈
ℂ
→
0
⋅
ℜ
⁡
B
=
0
12
8
11
sylan9eq
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
ℑ
⁡
A
⁢
ℜ
⁡
B
=
0
13
6
12
oveq12d
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
ℜ
⁡
A
⁢
ℑ
⁡
B
+
ℑ
⁡
A
⁢
ℜ
⁡
B
=
A
⁢
ℑ
⁡
B
+
0
14
imcl
⊢
B
∈
ℂ
→
ℑ
⁡
B
∈
ℝ
15
14
recnd
⊢
B
∈
ℂ
→
ℑ
⁡
B
∈
ℂ
16
mulcl
⊢
A
∈
ℂ
∧
ℑ
⁡
B
∈
ℂ
→
A
⁢
ℑ
⁡
B
∈
ℂ
17
1
15
16
syl2an
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
A
⁢
ℑ
⁡
B
∈
ℂ
18
17
addid1d
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
A
⁢
ℑ
⁡
B
+
0
=
A
⁢
ℑ
⁡
B
19
3
13
18
3eqtrd
⊢
A
∈
ℝ
∧
B
∈
ℂ
→
ℑ
⁡
A
⁢
B
=
A
⁢
ℑ
⁡
B