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 ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ

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 ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
4 df-3an ⊢ 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 ∈ ℝ
5 3 4 bitrdi ⊢ φ → 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 ∈ ℝ
6 1 2 iblposlem ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = 0
7 0re ⊢ 0 ∈ ℝ
8 6 7 eqeltrdi ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
9 8 biantrud ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 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 ∈ ℝ
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 ⊢ φ → if x ∈ A ∧ 0 ≤ B B 0 = if x ∈ A B 0
15 14 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 = x ∈ ℝ ⟼ if x ∈ A B 0
16 15 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
17 16 eleq1d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ↔ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
18 17 anbi2d ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
19 5 9 18 3bitr2d ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ