Metamath Proof Explorer

Theorem itgposval

Description: The integral 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∈ℝ
itgreval.2 ⊢φ→x∈A⟼B∈𝐿1
itgposval.3 ⊢φ∧x∈A→0≤B
Assertion itgposval ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈AB0

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢φ∧x∈A→B∈ℝ
2 itgreval.2 ⊢φ→x∈A⟼B∈𝐿1
3 itgposval.3 ⊢φ∧x∈A→0≤B
4 1 2 itgrevallem1 ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
5 3 ex ⊢φ→x∈A→0≤B
6 5 pm4.71rd ⊢φ→x∈A↔0≤B∧x∈A
7 ancom ⊢0≤B∧x∈A↔x∈A∧0≤B
8 6 7 bitr2di ⊢φ→x∈A∧0≤B↔x∈A
9 8 ifbid ⊢φ→ifx∈A∧0≤BB0=ifx∈AB0
10 9 mpteq2dv ⊢φ→x∈ℝ⟼ifx∈A∧0≤BB0=x∈ℝ⟼ifx∈AB0
11 10 fveq2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0=∫2⁡x∈ℝ⟼ifx∈AB0
12 1 3 iblposlem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0=0
13 11 12 oveq12d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0=∫2⁡x∈ℝ⟼ifx∈AB0−0
14 1 3 iblpos ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
15 2 14 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
16 15 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
17 16 recnd ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0∈ℂ
18 17 subid1d ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0−0=∫2⁡x∈ℝ⟼ifx∈AB0
19 4 13 18 3eqtrd ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈AB0