Metamath Proof Explorer

Theorem iblre

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

Ref Expression
Hypothesis iblrelem.1 ⊢φ∧x∈A→B∈ℝ
Assertion iblre ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼if0≤BB0∈𝐿1∧x∈A⟼if0≤−B−B0∈𝐿1

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢φ∧x∈A→B∈ℝ
2 1 mbfposb ⊢φ→x∈A⟼B∈MblFn↔x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn
3 ifan ⊢ifx∈A∧0≤BB0=ifx∈Aif0≤BB00
4 3 mpteq2i ⊢x∈ℝ⟼ifx∈A∧0≤BB0=x∈ℝ⟼ifx∈Aif0≤BB00
5 4 fveq2i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0=∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00
6 5 eleq1i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ↔∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ
7 ifan ⊢ifx∈A∧0≤−B−B0=ifx∈Aif0≤−B−B00
8 7 mpteq2i ⊢x∈ℝ⟼ifx∈A∧0≤−B−B0=x∈ℝ⟼ifx∈Aif0≤−B−B00
9 8 fveq2i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0=∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00
10 9 eleq1i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ↔∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
11 6 10 anbi12i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ↔∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
12 11 a1i ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ↔∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
13 2 12 anbi12d ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ↔x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
14 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∈ℝ
15 an4 ⊢x∈A⟼if0≤BB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ∧x∈A⟼if0≤−B−B0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ↔x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
16 13 14 15 3bitr4g ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ↔x∈A⟼if0≤BB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ∧x∈A⟼if0≤−B−B0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
17 1 iblrelem ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
18 0re ⊢0∈ℝ
19 ifcl ⊢B∈ℝ∧0∈ℝ→if0≤BB0∈ℝ
20 1 18 19 sylancl ⊢φ∧x∈A→if0≤BB0∈ℝ
21 max1 ⊢0∈ℝ∧B∈ℝ→0≤if0≤BB0
22 18 1 21 sylancr ⊢φ∧x∈A→0≤if0≤BB0
23 20 22 iblpos ⊢φ→x∈A⟼if0≤BB0∈𝐿1↔x∈A⟼if0≤BB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ
24 1 renegcld ⊢φ∧x∈A→−B∈ℝ
25 ifcl ⊢−B∈ℝ∧0∈ℝ→if0≤−B−B0∈ℝ
26 24 18 25 sylancl ⊢φ∧x∈A→if0≤−B−B0∈ℝ
27 max1 ⊢0∈ℝ∧−B∈ℝ→0≤if0≤−B−B0
28 18 24 27 sylancr ⊢φ∧x∈A→0≤if0≤−B−B0
29 26 28 iblpos ⊢φ→x∈A⟼if0≤−B−B0∈𝐿1↔x∈A⟼if0≤−B−B0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
30 23 29 anbi12d ⊢φ→x∈A⟼if0≤BB0∈𝐿1∧x∈A⟼if0≤−B−B0∈𝐿1↔x∈A⟼if0≤BB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ∧x∈A⟼if0≤−B−B0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
31 16 17 30 3bitr4d ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼if0≤BB0∈𝐿1∧x∈A⟼if0≤−B−B0∈𝐿1