Metamath Proof Explorer


Theorem iblrelem

Description: Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis iblrelem.1 φ x A B
Assertion 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

Proof

Step Hyp Ref Expression
1 iblrelem.1 φ x A B
2 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
3 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
4 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
5 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
6 2 3 4 5 1 iblcnlem φ 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 2 x if x A 0 B B 0 2 x if x A 0 B B 0
7 1 reim0d φ x A B = 0
8 7 itgvallem3 φ 2 x if x A 0 B B 0 = 0
9 0re 0
10 8 9 eqeltrdi φ 2 x if x A 0 B B 0
11 7 negeqd φ x A B = 0
12 neg0 0 = 0
13 11 12 syl6eq φ x A B = 0
14 13 itgvallem3 φ 2 x if x A 0 B B 0 = 0
15 14 9 eqeltrdi φ 2 x if x A 0 B B 0
16 10 15 jca φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0
17 16 biantrud φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0
18 1 rered φ x A B = B
19 18 ibllem φ if x A 0 B B 0 = if x A 0 B B 0
20 19 mpteq2dv φ x if x A 0 B B 0 = x if x A 0 B B 0
21 20 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
22 21 eleq1d φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0
23 18 negeqd φ x A B = B
24 23 ibllem φ if x A 0 B B 0 = if x A 0 B B 0
25 24 mpteq2dv φ x if x A 0 B B 0 = x if x A 0 B B 0
26 25 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
27 26 eleq1d φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0
28 22 27 anbi12d φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0
29 17 28 bitr3d φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0 2 x if x A 0 B B 0
30 29 anbi2d φ x A B MblFn 2 x if x A 0 B B 0 2 x if x A 0 B B 0 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
31 3anass x A B MblFn 2 x if x A 0 B B 0 2 x if x A 0 B B 0 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 2 x if x A 0 B B 0 2 x if x A 0 B B 0
32 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
33 30 31 32 3bitr4g φ x A B MblFn 2 x if x A 0 B B 0 2 x if x A 0 B B 0 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
34 6 33 bitrd φ 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