Metamath Proof Explorer


Theorem iblabsr

Description: A measurable function is integrable iff its absolute value is integrable. (See iblabs for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses iblabsr.1 φxABV
iblabsr.2 φxABMblFn
iblabsr.3 φxAB𝐿1
Assertion iblabsr φxAB𝐿1

Proof

Step Hyp Ref Expression
1 iblabsr.1 φxABV
2 iblabsr.2 φxABMblFn
3 iblabsr.3 φxAB𝐿1
4 ifan ifxA0BikBik0=ifxAif0BikBik00
5 2 1 mbfmptcl φxAB
6 5 adantlr φk03xAB
7 ax-icn i
8 ine0 i0
9 elfzelz k03k
10 9 ad2antlr φk03xAk
11 expclz ii0kik
12 7 8 10 11 mp3an12i φk03xAik
13 expne0i ii0kik0
14 7 8 10 13 mp3an12i φk03xAik0
15 6 12 14 divcld φk03xABik
16 15 recld φk03xABik
17 0re 0
18 ifcl Bik0if0BikBik0
19 16 17 18 sylancl φk03xAif0BikBik0
20 19 rexrd φk03xAif0BikBik0*
21 max1 0Bik0if0BikBik0
22 17 16 21 sylancr φk03xA0if0BikBik0
23 elxrge0 if0BikBik00+∞if0BikBik0*0if0BikBik0
24 20 22 23 sylanbrc φk03xAif0BikBik00+∞
25 0e0iccpnf 00+∞
26 25 a1i φk03¬xA00+∞
27 24 26 ifclda φk03ifxAif0BikBik000+∞
28 4 27 eqeltrid φk03ifxA0BikBik00+∞
29 28 adantr φk03xifxA0BikBik00+∞
30 29 fmpttd φk03xifxA0BikBik0:0+∞
31 5 abscld φxAB
32 5 absge0d φxA0B
33 31 32 iblpos φxAB𝐿1xABMblFn2xifxAB0
34 3 33 mpbid φxABMblFn2xifxAB0
35 34 simprd φ2xifxAB0
36 35 adantr φk032xifxAB0
37 31 rexrd φxAB*
38 elxrge0 B0+∞B*0B
39 37 32 38 sylanbrc φxAB0+∞
40 25 a1i φ¬xA00+∞
41 39 40 ifclda φifxAB00+∞
42 41 adantr φxifxAB00+∞
43 42 fmpttd φxifxAB0:0+∞
44 43 adantr φk03xifxAB0:0+∞
45 15 releabsd φk03xABikBik
46 6 12 14 absdivd φk03xABik=Bik
47 elfznn0 k03k0
48 47 ad2antlr φk03xAk0
49 absexp ik0ik=ik
50 7 48 49 sylancr φk03xAik=ik
51 absi i=1
52 51 oveq1i ik=1k
53 1exp k1k=1
54 10 53 syl φk03xA1k=1
55 52 54 eqtrid φk03xAik=1
56 50 55 eqtrd φk03xAik=1
57 56 oveq2d φk03xABik=B1
58 31 recnd φxAB
59 58 adantlr φk03xAB
60 59 div1d φk03xAB1=B
61 46 57 60 3eqtrd φk03xABik=B
62 45 61 breqtrd φk03xABikB
63 6 absge0d φk03xA0B
64 breq1 Bik=if0BikBik0BikBif0BikBik0B
65 breq1 0=if0BikBik00Bif0BikBik0B
66 64 65 ifboth BikB0Bif0BikBik0B
67 62 63 66 syl2anc φk03xAif0BikBik0B
68 iftrue xAifxAif0BikBik00=if0BikBik0
69 68 adantl φk03xAifxAif0BikBik00=if0BikBik0
70 iftrue xAifxAB0=B
71 70 adantl φk03xAifxAB0=B
72 67 69 71 3brtr4d φk03xAifxAif0BikBik00ifxAB0
73 72 ex φk03xAifxAif0BikBik00ifxAB0
74 0le0 00
75 74 a1i ¬xA00
76 iffalse ¬xAifxAif0BikBik00=0
77 iffalse ¬xAifxAB0=0
78 75 76 77 3brtr4d ¬xAifxAif0BikBik00ifxAB0
79 73 78 pm2.61d1 φk03ifxAif0BikBik00ifxAB0
80 4 79 eqbrtrid φk03ifxA0BikBik0ifxAB0
81 80 ralrimivw φk03xifxA0BikBik0ifxAB0
82 reex V
83 82 a1i φk03V
84 37 adantlr φk03xAB*
85 84 63 38 sylanbrc φk03xAB0+∞
86 85 26 ifclda φk03ifxAB00+∞
87 86 adantr φk03xifxAB00+∞
88 eqidd φk03xifxA0BikBik0=xifxA0BikBik0
89 eqidd φk03xifxAB0=xifxAB0
90 83 29 87 88 89 ofrfval2 φk03xifxA0BikBik0fxifxAB0xifxA0BikBik0ifxAB0
91 81 90 mpbird φk03xifxA0BikBik0fxifxAB0
92 itg2le xifxA0BikBik0:0+∞xifxAB0:0+∞xifxA0BikBik0fxifxAB02xifxA0BikBik02xifxAB0
93 30 44 91 92 syl3anc φk032xifxA0BikBik02xifxAB0
94 itg2lecl xifxA0BikBik0:0+∞2xifxAB02xifxA0BikBik02xifxAB02xifxA0BikBik0
95 30 36 93 94 syl3anc φk032xifxA0BikBik0
96 95 ralrimiva φk032xifxA0BikBik0
97 eqidd φxifxA0BikBik0=xifxA0BikBik0
98 eqidd φxABik=Bik
99 97 98 1 isibl2 φxAB𝐿1xABMblFnk032xifxA0BikBik0
100 2 96 99 mpbir2and φxAB𝐿1