Metamath Proof Explorer


Theorem itg2cnlem2

Description: Lemma for itgcn . (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses itg2cn.1 φF:0+∞
itg2cn.2 φFMblFn
itg2cn.3 φ2F
itg2cn.4 φC+
itg2cn.5 φM
itg2cn.6 φ¬2xifFxMFx02FC2
Assertion itg2cnlem2 φd+udomvolvolu<d2xifxuFx0<C

Proof

Step Hyp Ref Expression
1 itg2cn.1 φF:0+∞
2 itg2cn.2 φFMblFn
3 itg2cn.3 φ2F
4 itg2cn.4 φC+
5 itg2cn.5 φM
6 itg2cn.6 φ¬2xifFxMFx02FC2
7 4 rphalfcld φC2+
8 5 nnrpd φM+
9 7 8 rpdivcld φC2M+
10 simprl φudomvolvolu<C2Mudomvol
11 2 adantr φudomvolvolu<C2MFMblFn
12 rge0ssre 0+∞
13 fss F:0+∞0+∞F:
14 1 12 13 sylancl φF:
15 14 adantr φudomvolvolu<C2MF:
16 mbfima FMblFnF:F-1M+∞domvol
17 11 15 16 syl2anc φudomvolvolu<C2MF-1M+∞domvol
18 inmbl udomvolF-1M+∞domvoluF-1M+∞domvol
19 10 17 18 syl2anc φudomvolvolu<C2MuF-1M+∞domvol
20 difmbl udomvolF-1M+∞domvoluF-1M+∞domvol
21 10 17 20 syl2anc φudomvolvolu<C2MuF-1M+∞domvol
22 inass uF-1M+∞uF-1M+∞=uF-1M+∞uF-1M+∞
23 disjdif F-1M+∞uF-1M+∞=
24 23 ineq2i uF-1M+∞uF-1M+∞=u
25 in0 u=
26 22 24 25 3eqtri uF-1M+∞uF-1M+∞=
27 26 fveq2i vol*uF-1M+∞uF-1M+∞=vol*
28 ovol0 vol*=0
29 27 28 eqtri vol*uF-1M+∞uF-1M+∞=0
30 29 a1i φudomvolvolu<C2Mvol*uF-1M+∞uF-1M+∞=0
31 inundif uF-1M+∞uF-1M+∞=u
32 31 eqcomi u=uF-1M+∞uF-1M+∞
33 32 a1i φudomvolvolu<C2Mu=uF-1M+∞uF-1M+∞
34 mblss udomvolu
35 10 34 syl φudomvolvolu<C2Mu
36 35 sselda φudomvolvolu<C2Mxux
37 1 adantr φudomvolvolu<C2MF:0+∞
38 37 ffvelrnda φudomvolvolu<C2MxFx0+∞
39 elrege0 Fx0+∞Fx0Fx
40 38 39 sylib φudomvolvolu<C2MxFx0Fx
41 40 simpld φudomvolvolu<C2MxFx
42 41 rexrd φudomvolvolu<C2MxFx*
43 40 simprd φudomvolvolu<C2Mx0Fx
44 elxrge0 Fx0+∞Fx*0Fx
45 42 43 44 sylanbrc φudomvolvolu<C2MxFx0+∞
46 36 45 syldan φudomvolvolu<C2MxuFx0+∞
47 eqid xifxuF-1M+∞Fx0=xifxuF-1M+∞Fx0
48 eqid xifxuF-1M+∞Fx0=xifxuF-1M+∞Fx0
49 eqid xifxuFx0=xifxuFx0
50 0e0iccpnf 00+∞
51 ifcl Fx0+∞00+∞ifxuF-1M+∞Fx00+∞
52 45 50 51 sylancl φudomvolvolu<C2MxifxuF-1M+∞Fx00+∞
53 52 fmpttd φudomvolvolu<C2MxifxuF-1M+∞Fx0:0+∞
54 3 adantr φudomvolvolu<C2M2F
55 icossicc 0+∞0+∞
56 fss F:0+∞0+∞0+∞F:0+∞
57 37 55 56 sylancl φudomvolvolu<C2MF:0+∞
58 41 leidd φudomvolvolu<C2MxFxFx
59 breq1 Fx=ifxuF-1M+∞Fx0FxFxifxuF-1M+∞Fx0Fx
60 breq1 0=ifxuF-1M+∞Fx00FxifxuF-1M+∞Fx0Fx
61 59 60 ifboth FxFx0FxifxuF-1M+∞Fx0Fx
62 58 43 61 syl2anc φudomvolvolu<C2MxifxuF-1M+∞Fx0Fx
63 62 ralrimiva φudomvolvolu<C2MxifxuF-1M+∞Fx0Fx
64 reex V
65 64 a1i φudomvolvolu<C2MV
66 eqidd φudomvolvolu<C2MxifxuF-1M+∞Fx0=xifxuF-1M+∞Fx0
67 37 feqmptd φudomvolvolu<C2MF=xFx
68 65 52 41 66 67 ofrfval2 φudomvolvolu<C2MxifxuF-1M+∞Fx0fFxifxuF-1M+∞Fx0Fx
69 63 68 mpbird φudomvolvolu<C2MxifxuF-1M+∞Fx0fF
70 itg2le xifxuF-1M+∞Fx0:0+∞F:0+∞xifxuF-1M+∞Fx0fF2xifxuF-1M+∞Fx02F
71 53 57 69 70 syl3anc φudomvolvolu<C2M2xifxuF-1M+∞Fx02F
72 itg2lecl xifxuF-1M+∞Fx0:0+∞2F2xifxuF-1M+∞Fx02F2xifxuF-1M+∞Fx0
73 53 54 71 72 syl3anc φudomvolvolu<C2M2xifxuF-1M+∞Fx0
74 ifcl Fx0+∞00+∞ifxuF-1M+∞Fx00+∞
75 45 50 74 sylancl φudomvolvolu<C2MxifxuF-1M+∞Fx00+∞
76 75 fmpttd φudomvolvolu<C2MxifxuF-1M+∞Fx0:0+∞
77 breq1 Fx=ifxuF-1M+∞Fx0FxFxifxuF-1M+∞Fx0Fx
78 breq1 0=ifxuF-1M+∞Fx00FxifxuF-1M+∞Fx0Fx
79 77 78 ifboth FxFx0FxifxuF-1M+∞Fx0Fx
80 58 43 79 syl2anc φudomvolvolu<C2MxifxuF-1M+∞Fx0Fx
81 80 ralrimiva φudomvolvolu<C2MxifxuF-1M+∞Fx0Fx
82 eqidd φudomvolvolu<C2MxifxuF-1M+∞Fx0=xifxuF-1M+∞Fx0
83 65 75 41 82 67 ofrfval2 φudomvolvolu<C2MxifxuF-1M+∞Fx0fFxifxuF-1M+∞Fx0Fx
84 81 83 mpbird φudomvolvolu<C2MxifxuF-1M+∞Fx0fF
85 itg2le xifxuF-1M+∞Fx0:0+∞F:0+∞xifxuF-1M+∞Fx0fF2xifxuF-1M+∞Fx02F
86 76 57 84 85 syl3anc φudomvolvolu<C2M2xifxuF-1M+∞Fx02F
87 itg2lecl xifxuF-1M+∞Fx0:0+∞2F2xifxuF-1M+∞Fx02F2xifxuF-1M+∞Fx0
88 76 54 86 87 syl3anc φudomvolvolu<C2M2xifxuF-1M+∞Fx0
89 19 21 30 33 46 47 48 49 73 88 itg2split φudomvolvolu<C2M2xifxuFx0=2xifxuF-1M+∞Fx0+2xifxuF-1M+∞Fx0
90 4 adantr φudomvolvolu<C2MC+
91 90 rphalfcld φudomvolvolu<C2MC2+
92 91 rpred φudomvolvolu<C2MC2
93 ifcl Fx0+∞00+∞ifxF-1M+∞Fx00+∞
94 45 50 93 sylancl φudomvolvolu<C2MxifxF-1M+∞Fx00+∞
95 94 fmpttd φudomvolvolu<C2MxifxF-1M+∞Fx0:0+∞
96 breq1 Fx=ifxF-1M+∞Fx0FxFxifxF-1M+∞Fx0Fx
97 breq1 0=ifxF-1M+∞Fx00FxifxF-1M+∞Fx0Fx
98 96 97 ifboth FxFx0FxifxF-1M+∞Fx0Fx
99 58 43 98 syl2anc φudomvolvolu<C2MxifxF-1M+∞Fx0Fx
100 99 ralrimiva φudomvolvolu<C2MxifxF-1M+∞Fx0Fx
101 eqidd φudomvolvolu<C2MxifxF-1M+∞Fx0=xifxF-1M+∞Fx0
102 65 94 45 101 67 ofrfval2 φudomvolvolu<C2MxifxF-1M+∞Fx0fFxifxF-1M+∞Fx0Fx
103 100 102 mpbird φudomvolvolu<C2MxifxF-1M+∞Fx0fF
104 itg2le xifxF-1M+∞Fx0:0+∞F:0+∞xifxF-1M+∞Fx0fF2xifxF-1M+∞Fx02F
105 95 57 103 104 syl3anc φudomvolvolu<C2M2xifxF-1M+∞Fx02F
106 itg2lecl xifxF-1M+∞Fx0:0+∞2F2xifxF-1M+∞Fx02F2xifxF-1M+∞Fx0
107 95 54 105 106 syl3anc φudomvolvolu<C2M2xifxF-1M+∞Fx0
108 0red φudomvolvolu<C2Mx0
109 elinel2 xuF-1M+∞xF-1M+∞
110 109 a1i φudomvolvolu<C2MxxuF-1M+∞xF-1M+∞
111 ifle Fx00FxxuF-1M+∞xF-1M+∞ifxuF-1M+∞Fx0ifxF-1M+∞Fx0
112 41 108 43 110 111 syl31anc φudomvolvolu<C2MxifxuF-1M+∞Fx0ifxF-1M+∞Fx0
113 112 ralrimiva φudomvolvolu<C2MxifxuF-1M+∞Fx0ifxF-1M+∞Fx0
114 65 52 94 66 101 ofrfval2 φudomvolvolu<C2MxifxuF-1M+∞Fx0fxifxF-1M+∞Fx0xifxuF-1M+∞Fx0ifxF-1M+∞Fx0
115 113 114 mpbird φudomvolvolu<C2MxifxuF-1M+∞Fx0fxifxF-1M+∞Fx0
116 itg2le xifxuF-1M+∞Fx0:0+∞xifxF-1M+∞Fx0:0+∞xifxuF-1M+∞Fx0fxifxF-1M+∞Fx02xifxuF-1M+∞Fx02xifxF-1M+∞Fx0
117 53 95 115 116 syl3anc φudomvolvolu<C2M2xifxuF-1M+∞Fx02xifxF-1M+∞Fx0
118 67 fveq2d φudomvolvolu<C2M2F=2xFx
119 cmmbl F-1M+∞domvolF-1M+∞domvol
120 17 119 syl φudomvolvolu<C2MF-1M+∞domvol
121 disjdif F-1M+∞F-1M+∞=
122 121 fveq2i vol*F-1M+∞F-1M+∞=vol*
123 122 28 eqtri vol*F-1M+∞F-1M+∞=0
124 123 a1i φudomvolvolu<C2Mvol*F-1M+∞F-1M+∞=0
125 undif2 F-1M+∞F-1M+∞=F-1M+∞
126 mblss F-1M+∞domvolF-1M+∞
127 17 126 syl φudomvolvolu<C2MF-1M+∞
128 ssequn1 F-1M+∞F-1M+∞=
129 127 128 sylib φudomvolvolu<C2MF-1M+∞=
130 125 129 eqtr2id φudomvolvolu<C2M=F-1M+∞F-1M+∞
131 eqid xifxF-1M+∞Fx0=xifxF-1M+∞Fx0
132 eqid xifxF-1M+∞Fx0=xifxF-1M+∞Fx0
133 iftrue xifxFx0=Fx
134 133 mpteq2ia xifxFx0=xFx
135 134 eqcomi xFx=xifxFx0
136 ifcl Fx0+∞00+∞ifxF-1M+∞Fx00+∞
137 45 50 136 sylancl φudomvolvolu<C2MxifxF-1M+∞Fx00+∞
138 137 fmpttd φudomvolvolu<C2MxifxF-1M+∞Fx0:0+∞
139 breq1 Fx=ifxF-1M+∞Fx0FxFxifxF-1M+∞Fx0Fx
140 breq1 0=ifxF-1M+∞Fx00FxifxF-1M+∞Fx0Fx
141 139 140 ifboth FxFx0FxifxF-1M+∞Fx0Fx
142 58 43 141 syl2anc φudomvolvolu<C2MxifxF-1M+∞Fx0Fx
143 142 ralrimiva φudomvolvolu<C2MxifxF-1M+∞Fx0Fx
144 eqidd φudomvolvolu<C2MxifxF-1M+∞Fx0=xifxF-1M+∞Fx0
145 65 137 45 144 67 ofrfval2 φudomvolvolu<C2MxifxF-1M+∞Fx0fFxifxF-1M+∞Fx0Fx
146 143 145 mpbird φudomvolvolu<C2MxifxF-1M+∞Fx0fF
147 itg2le xifxF-1M+∞Fx0:0+∞F:0+∞xifxF-1M+∞Fx0fF2xifxF-1M+∞Fx02F
148 138 57 146 147 syl3anc φudomvolvolu<C2M2xifxF-1M+∞Fx02F
149 itg2lecl xifxF-1M+∞Fx0:0+∞2F2xifxF-1M+∞Fx02F2xifxF-1M+∞Fx0
150 138 54 148 149 syl3anc φudomvolvolu<C2M2xifxF-1M+∞Fx0
151 17 120 124 130 45 131 132 135 107 150 itg2split φudomvolvolu<C2M2xFx=2xifxF-1M+∞Fx0+2xifxF-1M+∞Fx0
152 118 151 eqtrd φudomvolvolu<C2M2F=2xifxF-1M+∞Fx0+2xifxF-1M+∞Fx0
153 eldif xF-1M+∞x¬xF-1M+∞
154 153 baib xxF-1M+∞¬xF-1M+∞
155 154 adantl φudomvolvolu<C2MxxF-1M+∞¬xF-1M+∞
156 1 ffnd φFFn
157 156 ad2antrr φudomvolvolu<C2MxFFn
158 elpreima FFnxF-1M+∞xFxM+∞
159 157 158 syl φudomvolvolu<C2MxxF-1M+∞xFxM+∞
160 41 biantrurd φudomvolvolu<C2MxM<FxFxM<Fx
161 5 nnred φM
162 161 ad2antrr φudomvolvolu<C2MxM
163 162 rexrd φudomvolvolu<C2MxM*
164 elioopnf M*FxM+∞FxM<Fx
165 163 164 syl φudomvolvolu<C2MxFxM+∞FxM<Fx
166 simpr φudomvolvolu<C2Mxx
167 166 biantrurd φudomvolvolu<C2MxFxM+∞xFxM+∞
168 160 165 167 3bitr2d φudomvolvolu<C2MxM<FxxFxM+∞
169 162 41 ltnled φudomvolvolu<C2MxM<Fx¬FxM
170 159 168 169 3bitr2rd φudomvolvolu<C2Mx¬FxMxF-1M+∞
171 170 con1bid φudomvolvolu<C2Mx¬xF-1M+∞FxM
172 155 171 bitrd φudomvolvolu<C2MxxF-1M+∞FxM
173 172 ifbid φudomvolvolu<C2MxifxF-1M+∞Fx0=ifFxMFx0
174 173 mpteq2dva φudomvolvolu<C2MxifxF-1M+∞Fx0=xifFxMFx0
175 174 fveq2d φudomvolvolu<C2M2xifxF-1M+∞Fx0=2xifFxMFx0
176 6 adantr φudomvolvolu<C2M¬2xifFxMFx02FC2
177 175 176 eqnbrtrd φudomvolvolu<C2M¬2xifxF-1M+∞Fx02FC2
178 54 92 resubcld φudomvolvolu<C2M2FC2
179 178 150 ltnled φudomvolvolu<C2M2FC2<2xifxF-1M+∞Fx0¬2xifxF-1M+∞Fx02FC2
180 177 179 mpbird φudomvolvolu<C2M2FC2<2xifxF-1M+∞Fx0
181 54 92 150 ltsubadd2d φudomvolvolu<C2M2FC2<2xifxF-1M+∞Fx02F<C2+2xifxF-1M+∞Fx0
182 180 181 mpbid φudomvolvolu<C2M2F<C2+2xifxF-1M+∞Fx0
183 152 182 eqbrtrrd φudomvolvolu<C2M2xifxF-1M+∞Fx0+2xifxF-1M+∞Fx0<C2+2xifxF-1M+∞Fx0
184 107 92 150 ltadd1d φudomvolvolu<C2M2xifxF-1M+∞Fx0<C22xifxF-1M+∞Fx0+2xifxF-1M+∞Fx0<C2+2xifxF-1M+∞Fx0
185 183 184 mpbird φudomvolvolu<C2M2xifxF-1M+∞Fx0<C2
186 73 107 92 117 185 lelttrd φudomvolvolu<C2M2xifxuF-1M+∞Fx0<C2
187 161 adantr φudomvolvolu<C2MM
188 mblvol udomvolvolu=vol*u
189 10 188 syl φudomvolvolu<C2Mvolu=vol*u
190 9 rpred φC2M
191 190 adantr φudomvolvolu<C2MC2M
192 ovolcl uvol*u*
193 35 192 syl φudomvolvolu<C2Mvol*u*
194 191 rexrd φudomvolvolu<C2MC2M*
195 simprr φudomvolvolu<C2Mvolu<C2M
196 189 195 eqbrtrrd φudomvolvolu<C2Mvol*u<C2M
197 193 194 196 xrltled φudomvolvolu<C2Mvol*uC2M
198 ovollecl uC2Mvol*uC2Mvol*u
199 35 191 197 198 syl3anc φudomvolvolu<C2Mvol*u
200 189 199 eqeltrd φudomvolvolu<C2Mvolu
201 187 200 remulcld φudomvolvolu<C2MMvolu
202 187 rexrd φudomvolvolu<C2MM*
203 5 adantr φudomvolvolu<C2MM
204 203 nnnn0d φudomvolvolu<C2MM0
205 204 nn0ge0d φudomvolvolu<C2M0M
206 elxrge0 M0+∞M*0M
207 202 205 206 sylanbrc φudomvolvolu<C2MM0+∞
208 ifcl M0+∞00+∞ifxuM00+∞
209 207 50 208 sylancl φudomvolvolu<C2MifxuM00+∞
210 209 adantr φudomvolvolu<C2MxifxuM00+∞
211 210 fmpttd φudomvolvolu<C2MxifxuM0:0+∞
212 eldifn xuF-1M+∞¬xF-1M+∞
213 212 adantl φudomvolvolu<C2MxuF-1M+∞¬xF-1M+∞
214 difssd φudomvolvolu<C2MuF-1M+∞u
215 214 sselda φudomvolvolu<C2MxuF-1M+∞xu
216 36 170 syldan φudomvolvolu<C2Mxu¬FxMxF-1M+∞
217 215 216 syldan φudomvolvolu<C2MxuF-1M+∞¬FxMxF-1M+∞
218 217 con1bid φudomvolvolu<C2MxuF-1M+∞¬xF-1M+∞FxM
219 213 218 mpbid φudomvolvolu<C2MxuF-1M+∞FxM
220 iftrue xuF-1M+∞ifxuF-1M+∞Fx0=Fx
221 220 adantl φudomvolvolu<C2MxuF-1M+∞ifxuF-1M+∞Fx0=Fx
222 215 iftrued φudomvolvolu<C2MxuF-1M+∞ifxuM0=M
223 219 221 222 3brtr4d φudomvolvolu<C2MxuF-1M+∞ifxuF-1M+∞Fx0ifxuM0
224 iffalse ¬xuF-1M+∞ifxuF-1M+∞Fx0=0
225 224 adantl φudomvolvolu<C2M¬xuF-1M+∞ifxuF-1M+∞Fx0=0
226 0le0 00
227 breq2 M=ifxuM00M0ifxuM0
228 breq2 0=ifxuM0000ifxuM0
229 227 228 ifboth 0M000ifxuM0
230 205 226 229 sylancl φudomvolvolu<C2M0ifxuM0
231 230 adantr φudomvolvolu<C2M¬xuF-1M+∞0ifxuM0
232 225 231 eqbrtrd φudomvolvolu<C2M¬xuF-1M+∞ifxuF-1M+∞Fx0ifxuM0
233 223 232 pm2.61dan φudomvolvolu<C2MifxuF-1M+∞Fx0ifxuM0
234 233 ralrimivw φudomvolvolu<C2MxifxuF-1M+∞Fx0ifxuM0
235 eqidd φudomvolvolu<C2MxifxuM0=xifxuM0
236 65 75 210 82 235 ofrfval2 φudomvolvolu<C2MxifxuF-1M+∞Fx0fxifxuM0xifxuF-1M+∞Fx0ifxuM0
237 234 236 mpbird φudomvolvolu<C2MxifxuF-1M+∞Fx0fxifxuM0
238 itg2le xifxuF-1M+∞Fx0:0+∞xifxuM0:0+∞xifxuF-1M+∞Fx0fxifxuM02xifxuF-1M+∞Fx02xifxuM0
239 76 211 237 238 syl3anc φudomvolvolu<C2M2xifxuF-1M+∞Fx02xifxuM0
240 elrege0 M0+∞M0M
241 187 205 240 sylanbrc φudomvolvolu<C2MM0+∞
242 itg2const udomvolvoluM0+∞2xifxuM0=Mvolu
243 10 200 241 242 syl3anc φudomvolvolu<C2M2xifxuM0=Mvolu
244 239 243 breqtrd φudomvolvolu<C2M2xifxuF-1M+∞Fx0Mvolu
245 203 nngt0d φudomvolvolu<C2M0<M
246 ltmuldiv2 voluC2M0<MMvolu<C2volu<C2M
247 200 92 187 245 246 syl112anc φudomvolvolu<C2MMvolu<C2volu<C2M
248 195 247 mpbird φudomvolvolu<C2MMvolu<C2
249 88 201 92 244 248 lelttrd φudomvolvolu<C2M2xifxuF-1M+∞Fx0<C2
250 73 88 92 92 186 249 lt2addd φudomvolvolu<C2M2xifxuF-1M+∞Fx0+2xifxuF-1M+∞Fx0<C2+C2
251 89 250 eqbrtrd φudomvolvolu<C2M2xifxuFx0<C2+C2
252 90 rpcnd φudomvolvolu<C2MC
253 252 2halvesd φudomvolvolu<C2MC2+C2=C
254 251 253 breqtrd φudomvolvolu<C2M2xifxuFx0<C
255 254 expr φudomvolvolu<C2M2xifxuFx0<C
256 255 ralrimiva φudomvolvolu<C2M2xifxuFx0<C
257 breq2 d=C2Mvolu<dvolu<C2M
258 257 rspceaimv C2M+udomvolvolu<C2M2xifxuFx0<Cd+udomvolvolu<d2xifxuFx0<C
259 9 256 258 syl2anc φd+udomvolvolu<d2xifxuFx0<C