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 syl6bb φ 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 syl6rbb φ 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