Metamath Proof Explorer


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 dx = A B dx

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 dx = A B dx + i A B dx
4 3 fveq2d φ A B dx = A B dx + i A B dx
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 dx
13 7 imcld φ x A B
14 10 simprd φ x A B 𝐿 1
15 13 14 itgrecl φ A B dx
16 12 15 crimd φ A B dx + i A B dx = A B dx
17 4 16 eqtrd φ A B dx = A B dx