Metamath Proof Explorer

Theorem iblcn

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

Ref Expression
Hypothesis iblcn.1 ⊢ φ ∧ x ∈ A → B ∈ ℂ
Assertion iblcn ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 iblcn.1 ⊢ φ ∧ x ∈ A → B ∈ ℂ
2 1 ismbfcn2 ⊢ φ → x ∈ A ⟼ B ∈ MblFn ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn
3 2 anbi1d ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
4 3anass ⊢ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
5 an4 ⊢ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
6 3 4 5 3bitr4g ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
7 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
8 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
9 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
10 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
11 7 8 9 10 1 iblcnlem1 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
12 1 recld ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℝ
13 12 iblrelem ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ
14 3anass ⊢ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ
15 13 14 bitrdi ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ
16 1 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
17 16 iblrelem ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
18 3anass ⊢ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ ↔ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
19 17 18 bitrdi ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
20 15 19 anbi12d ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
21 6 11 20 3bitr4d ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1