Metamath Proof Explorer

Theorem iblrelem

Description: Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis iblrelem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
Assertion 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 ∈ ℝ

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
2 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
3 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
4 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
5 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
6 2 3 4 5 1 iblcnlem ⊢ φ → 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 ∈ ℝ
7 1 reim0d ⊢ φ ∧ x ∈ A → ℑ ⁡ B = 0
8 7 itgvallem3 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 = 0
9 0re ⊢ 0 ∈ ℝ
10 8 9 eqeltrdi ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ
11 7 negeqd ⊢ φ ∧ x ∈ A → − ℑ ⁡ B = − 0
12 neg0 ⊢ − 0 = 0
13 11 12 eqtrdi ⊢ φ ∧ x ∈ A → − ℑ ⁡ B = 0
14 13 itgvallem3 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = 0
15 14 9 eqeltrdi ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
16 10 15 jca ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
17 16 biantrud ⊢ φ → ∫ 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 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
18 1 rered ⊢ φ ∧ x ∈ A → ℜ ⁡ B = B
19 18 ibllem ⊢ φ → if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = if x ∈ A ∧ 0 ≤ B B 0
20 19 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0
21 20 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0
22 21 eleq1d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ ↔ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
23 18 negeqd ⊢ φ ∧ x ∈ A → − ℜ ⁡ B = − B
24 23 ibllem ⊢ φ → if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = if x ∈ A ∧ 0 ≤ − B − B 0
25 24 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
26 25 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
27 26 eleq1d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ ↔ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
28 22 27 anbi12d ⊢ φ → ∫ 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 ∈ ℝ
29 17 28 bitr3d ⊢ φ → ∫ 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 ∈ ℝ ↔ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
30 29 anbi2d ⊢ φ → 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 ∈ ℝ
31 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 ∈ ℝ
32 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 ∈ ℝ
33 30 31 32 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 ∈ ℝ
34 6 33 bitrd ⊢ φ → 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 ∈ ℝ