Metamath Proof Explorer


Theorem iblabs

Description: The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses iblabs.1 φxABV
iblabs.2 φxAB𝐿1
Assertion iblabs φxAB𝐿1

Proof

Step Hyp Ref Expression
1 iblabs.1 φxABV
2 iblabs.2 φxAB𝐿1
3 absf abs:
4 3 a1i φabs:
5 iblmbf xAB𝐿1xABMblFn
6 2 5 syl φxABMblFn
7 6 1 mbfmptcl φxAB
8 4 7 cofmpt φabsxAB=xAB
9 7 fmpttd φxAB:A
10 ax-resscn
11 ssid
12 cncfss cncn
13 10 11 12 mp2an cncn
14 abscncf abs:cn
15 13 14 sselii abs:cn
16 15 a1i φabs:cn
17 cncombf xABMblFnxAB:Aabs:cnabsxABMblFn
18 6 9 16 17 syl3anc φabsxABMblFn
19 8 18 eqeltrrd φxABMblFn
20 7 abscld φxAB
21 20 rexrd φxAB*
22 7 absge0d φxA0B
23 elxrge0 B0+∞B*0B
24 21 22 23 sylanbrc φxAB0+∞
25 0e0iccpnf 00+∞
26 25 a1i φ¬xA00+∞
27 24 26 ifclda φifxAB00+∞
28 27 adantr φxifxAB00+∞
29 28 fmpttd φxifxAB0:0+∞
30 reex V
31 30 a1i φV
32 7 recld φxAB
33 32 recnd φxAB
34 33 abscld φxAB
35 33 absge0d φxA0B
36 elrege0 B0+∞B0B
37 34 35 36 sylanbrc φxAB0+∞
38 0e0icopnf 00+∞
39 38 a1i φ¬xA00+∞
40 37 39 ifclda φifxAB00+∞
41 40 adantr φxifxAB00+∞
42 7 imcld φxAB
43 42 recnd φxAB
44 43 abscld φxAB
45 43 absge0d φxA0B
46 elrege0 B0+∞B0B
47 44 45 46 sylanbrc φxAB0+∞
48 47 39 ifclda φifxAB00+∞
49 48 adantr φxifxAB00+∞
50 eqidd φxifxAB0=xifxAB0
51 eqidd φxifxAB0=xifxAB0
52 31 41 49 50 51 offval2 φxifxAB0+fxifxAB0=xifxAB0+ifxAB0
53 iftrue xAifxAB0=B
54 iftrue xAifxAB0=B
55 53 54 oveq12d xAifxAB0+ifxAB0=B+B
56 iftrue xAifxAB+B0=B+B
57 55 56 eqtr4d xAifxAB0+ifxAB0=ifxAB+B0
58 00id 0+0=0
59 iffalse ¬xAifxAB0=0
60 iffalse ¬xAifxAB0=0
61 59 60 oveq12d ¬xAifxAB0+ifxAB0=0+0
62 iffalse ¬xAifxAB+B0=0
63 58 61 62 3eqtr4a ¬xAifxAB0+ifxAB0=ifxAB+B0
64 57 63 pm2.61i ifxAB0+ifxAB0=ifxAB+B0
65 64 mpteq2i xifxAB0+ifxAB0=xifxAB+B0
66 52 65 eqtr2di φxifxAB+B0=xifxAB0+fxifxAB0
67 66 fveq2d φ2xifxAB+B0=2xifxAB0+fxifxAB0
68 eqid xifxAB0=xifxAB0
69 7 iblcn φxAB𝐿1xAB𝐿1xAB𝐿1
70 2 69 mpbid φxAB𝐿1xAB𝐿1
71 70 simpld φxAB𝐿1
72 1 2 68 71 32 iblabslem φxifxAB0MblFn2xifxAB0
73 72 simpld φxifxAB0MblFn
74 41 fmpttd φxifxAB0:0+∞
75 72 simprd φ2xifxAB0
76 eqid xifxAB0=xifxAB0
77 70 simprd φxAB𝐿1
78 1 2 76 77 42 iblabslem φxifxAB0MblFn2xifxAB0
79 78 simpld φxifxAB0MblFn
80 49 fmpttd φxifxAB0:0+∞
81 78 simprd φ2xifxAB0
82 73 74 75 79 80 81 itg2add φ2xifxAB0+fxifxAB0=2xifxAB0+2xifxAB0
83 67 82 eqtrd φ2xifxAB+B0=2xifxAB0+2xifxAB0
84 75 81 readdcld φ2xifxAB0+2xifxAB0
85 83 84 eqeltrd φ2xifxAB+B0
86 34 44 readdcld φxAB+B
87 86 rexrd φxAB+B*
88 34 44 35 45 addge0d φxA0B+B
89 elxrge0 B+B0+∞B+B*0B+B
90 87 88 89 sylanbrc φxAB+B0+∞
91 90 26 ifclda φifxAB+B00+∞
92 91 adantr φxifxAB+B00+∞
93 92 fmpttd φxifxAB+B0:0+∞
94 ax-icn i
95 mulcl iBiB
96 94 43 95 sylancr φxAiB
97 33 96 abstrid φxAB+iBB+iB
98 7 replimd φxAB=B+iB
99 98 fveq2d φxAB=B+iB
100 absmul iBiB=iB
101 94 43 100 sylancr φxAiB=iB
102 absi i=1
103 102 oveq1i iB=1B
104 44 recnd φxAB
105 104 mulid2d φxA1B=B
106 103 105 eqtrid φxAiB=B
107 101 106 eqtr2d φxAB=iB
108 107 oveq2d φxAB+B=B+iB
109 97 99 108 3brtr4d φxABB+B
110 iftrue xAifxAB0=B
111 110 adantl φxAifxAB0=B
112 56 adantl φxAifxAB+B0=B+B
113 109 111 112 3brtr4d φxAifxAB0ifxAB+B0
114 113 ex φxAifxAB0ifxAB+B0
115 0le0 00
116 115 a1i ¬xA00
117 iffalse ¬xAifxAB0=0
118 116 117 62 3brtr4d ¬xAifxAB0ifxAB+B0
119 114 118 pm2.61d1 φifxAB0ifxAB+B0
120 119 ralrimivw φxifxAB0ifxAB+B0
121 eqidd φxifxAB0=xifxAB0
122 eqidd φxifxAB+B0=xifxAB+B0
123 31 28 92 121 122 ofrfval2 φxifxAB0fxifxAB+B0xifxAB0ifxAB+B0
124 120 123 mpbird φxifxAB0fxifxAB+B0
125 itg2le xifxAB0:0+∞xifxAB+B0:0+∞xifxAB0fxifxAB+B02xifxAB02xifxAB+B0
126 29 93 124 125 syl3anc φ2xifxAB02xifxAB+B0
127 itg2lecl xifxAB0:0+∞2xifxAB+B02xifxAB02xifxAB+B02xifxAB0
128 29 85 126 127 syl3anc φ2xifxAB0
129 20 22 iblpos φxAB𝐿1xABMblFn2xifxAB0
130 19 128 129 mpbir2and φxAB𝐿1