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 ⟼ if 0 ≤ B B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ 𝐿 1

Proof

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