Database
BASIC REAL AND COMPLEX ANALYSIS
Integrals
Lebesgue integration
Lesbesgue integral
itgim
Next ⟩
iblneg
Metamath Proof Explorer
Ascii
Unicode
Theorem
itgim
Description:
Imaginary part of an integral.
(Contributed by
Mario Carneiro
, 14-Aug-2014)
Ref
Expression
Hypotheses
itgcnval.1
⊢
φ
∧
x
∈
A
→
B
∈
V
itgcnval.2
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
Assertion
itgim
⊢
φ
→
ℑ
⁡
∫
A
B
d
x
=
∫
A
ℑ
⁡
B
d
x
Proof
Step
Hyp
Ref
Expression
1
itgcnval.1
⊢
φ
∧
x
∈
A
→
B
∈
V
2
itgcnval.2
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
3
1
2
itgcnval
⊢
φ
→
∫
A
B
d
x
=
∫
A
ℜ
⁡
B
d
x
+
i
⁢
∫
A
ℑ
⁡
B
d
x
4
3
fveq2d
⊢
φ
→
ℑ
⁡
∫
A
B
d
x
=
ℑ
⁡
∫
A
ℜ
⁡
B
d
x
+
i
⁢
∫
A
ℑ
⁡
B
d
x
5
iblmbf
⊢
x
∈
A
⟼
B
∈
𝐿
1
→
x
∈
A
⟼
B
∈
MblFn
6
2
5
syl
⊢
φ
→
x
∈
A
⟼
B
∈
MblFn
7
6
1
mbfmptcl
⊢
φ
∧
x
∈
A
→
B
∈
ℂ
8
7
recld
⊢
φ
∧
x
∈
A
→
ℜ
⁡
B
∈
ℝ
9
7
iblcn
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
↔
x
∈
A
⟼
ℜ
⁡
B
∈
𝐿
1
∧
x
∈
A
⟼
ℑ
⁡
B
∈
𝐿
1
10
2
9
mpbid
⊢
φ
→
x
∈
A
⟼
ℜ
⁡
B
∈
𝐿
1
∧
x
∈
A
⟼
ℑ
⁡
B
∈
𝐿
1
11
10
simpld
⊢
φ
→
x
∈
A
⟼
ℜ
⁡
B
∈
𝐿
1
12
8
11
itgrecl
⊢
φ
→
∫
A
ℜ
⁡
B
d
x
∈
ℝ
13
7
imcld
⊢
φ
∧
x
∈
A
→
ℑ
⁡
B
∈
ℝ
14
10
simprd
⊢
φ
→
x
∈
A
⟼
ℑ
⁡
B
∈
𝐿
1
15
13
14
itgrecl
⊢
φ
→
∫
A
ℑ
⁡
B
d
x
∈
ℝ
16
12
15
crimd
⊢
φ
→
ℑ
⁡
∫
A
ℜ
⁡
B
d
x
+
i
⁢
∫
A
ℑ
⁡
B
d
x
=
∫
A
ℑ
⁡
B
d
x
17
4
16
eqtrd
⊢
φ
→
ℑ
⁡
∫
A
B
d
x
=
∫
A
ℑ
⁡
B
d
x