Metamath Proof Explorer


Theorem itgre

Description: Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014)

Ref Expression
Hypotheses itgcnval.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
itgcnval.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
Assertion itgre ( 𝜑 → ( ℜ ‘ ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgcnval.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
2 itgcnval.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
3 1 2 itgcnval ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
4 3 fveq2d ( 𝜑 → ( ℜ ‘ ∫ 𝐴 𝐵 d 𝑥 ) = ( ℜ ‘ ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
5 iblmbf ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
6 2 5 syl ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
7 6 1 mbfmptcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
8 7 recld ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
9 7 iblcn ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
10 2 9 mpbid ( 𝜑 → ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
11 10 simpld ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
12 8 11 itgrecl ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℝ )
13 7 imcld ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
14 10 simprd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
15 13 14 itgrecl ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℝ )
16 12 15 crred ( 𝜑 → ( ℜ ‘ ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 )
17 4 16 eqtrd ( 𝜑 → ( ℜ ‘ ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 )