Metamath Proof Explorer

Theorem iblpos

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

Ref Expression
Hypotheses iblrelem.1 ⊢φ∧x∈A→B∈ℝ
iblpos.2 ⊢φ∧x∈A→0≤B
Assertion iblpos ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢φ∧x∈A→B∈ℝ
2 iblpos.2 ⊢φ∧x∈A→0≤B
3 1 iblrelem ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
4 df-3an ⊢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∈ℝ
5 3 4 bitrdi ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
6 1 2 iblposlem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0=0
7 0re ⊢0∈ℝ
8 6 7 eqeltrdi ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
9 8 biantrud ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
10 2 ex ⊢φ→x∈A→0≤B
11 10 pm4.71rd ⊢φ→x∈A↔0≤B∧x∈A
12 ancom ⊢0≤B∧x∈A↔x∈A∧0≤B
13 11 12 bitr2di ⊢φ→x∈A∧0≤B↔x∈A
14 13 ifbid ⊢φ→ifx∈A∧0≤BB0=ifx∈AB0
15 14 mpteq2dv ⊢φ→x∈ℝ⟼ifx∈A∧0≤BB0=x∈ℝ⟼ifx∈AB0
16 15 fveq2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0=∫2⁡x∈ℝ⟼ifx∈AB0
17 16 eleq1d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ↔∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
18 17 anbi2d ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
19 5 9 18 3bitr2d ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ