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∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ

Proof

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