Metamath Proof Explorer


Theorem iblcn

Description: Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis iblcn.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
Assertion iblcn ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )

Proof

Step Hyp Ref Expression
1 iblcn.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
2 1 ismbfcn2 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ MblFn ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )
3 2 anbi1d ( 𝜑 → ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) ↔ ( ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ∧ ( ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) ) )
4 3anass ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ↔ ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) )
5 an4 ( ( ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ∧ ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) ↔ ( ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ∧ ( ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) )
6 3 4 5 3bitr4g ( 𝜑 → ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ↔ ( ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ∧ ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) ) )
7 eqid ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
8 eqid ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
9 eqid ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
10 eqid ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
11 7 8 9 10 1 iblcnlem1 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) )
12 1 recld ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
13 12 iblrelem ( 𝜑 → ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
14 3anass ( ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
15 13 14 bitrdi ( 𝜑 → ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) )
16 1 imcld ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
17 16 iblrelem ( 𝜑 → ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
18 3anass ( ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ↔ ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
19 17 18 bitrdi ( 𝜑 → ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) )
20 15 19 anbi12d ( 𝜑 → ( ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ↔ ( ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ∧ ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) ) )
21 6 11 20 3bitr4d ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )