Metamath Proof Explorer


Theorem itg2gt0

Description: If the function F is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypotheses itg2gt0.1 φAdomvol
itg2gt0.2 φ0<volA
itg2gt0.3 φF:0+∞
itg2gt0.4 φFMblFn
itg2gt0.5 φxA0<Fx
Assertion itg2gt0 φ0<2F

Proof

Step Hyp Ref Expression
1 itg2gt0.1 φAdomvol
2 itg2gt0.2 φ0<volA
3 itg2gt0.3 φF:0+∞
4 itg2gt0.4 φFMblFn
5 itg2gt0.5 φxA0<Fx
6 iccssxr 0+∞*
7 volf vol:domvol0+∞
8 7 ffvelrni AdomvolvolA0+∞
9 6 8 sselid AdomvolvolA*
10 1 9 syl φvolA*
11 10 adantr φ¬0<2FvolA*
12 4 elexd φFV
13 cnvexg FVF-1V
14 12 13 syl φF-1V
15 imaexg F-1VF-11n+∞V
16 14 15 syl φF-11n+∞V
17 16 adantr φnF-11n+∞V
18 17 fmpttd φnF-11n+∞:V
19 18 ffnd φnF-11n+∞Fn
20 fniunfv nF-11n+∞FnknF-11n+∞k=rannF-11n+∞
21 19 20 syl φknF-11n+∞k=rannF-11n+∞
22 rge0ssre 0+∞
23 fss F:0+∞0+∞F:
24 3 22 23 sylancl φF:
25 mbfima FMblFnF:F-11n+∞domvol
26 4 24 25 syl2anc φF-11n+∞domvol
27 26 adantr φnF-11n+∞domvol
28 27 fmpttd φnF-11n+∞:domvol
29 28 ffvelrnda φknF-11n+∞kdomvol
30 29 ralrimiva φknF-11n+∞kdomvol
31 iunmbl knF-11n+∞kdomvolknF-11n+∞kdomvol
32 30 31 syl φknF-11n+∞kdomvol
33 21 32 eqeltrrd φrannF-11n+∞domvol
34 mblss rannF-11n+∞domvolrannF-11n+∞
35 33 34 syl φrannF-11n+∞
36 ovolcl rannF-11n+∞vol*rannF-11n+∞*
37 35 36 syl φvol*rannF-11n+∞*
38 37 adantr φ¬0<2Fvol*rannF-11n+∞*
39 0xr 0*
40 39 a1i φ¬0<2F0*
41 mblvol AdomvolvolA=vol*A
42 1 41 syl φvolA=vol*A
43 mblss AdomvolA
44 1 43 syl φA
45 44 sselda φxAx
46 3 ffvelrnda φxFx0+∞
47 elrege0 Fx0+∞Fx0Fx
48 46 47 sylib φxFx0Fx
49 48 simpld φxFx
50 45 49 syldan φxAFx
51 nnrecl Fx0<Fxk1k<Fx
52 50 5 51 syl2anc φxAk1k<Fx
53 3 ffnd φFFn
54 53 ad2antrr φxAkFFn
55 elpreima FFnxF-11k+∞xFx1k+∞
56 54 55 syl φxAkxF-11k+∞xFx1k+∞
57 45 adantr φxAkx
58 57 biantrurd φxAkFx1k+∞xFx1k+∞
59 nnrecre k1k
60 59 adantl φk1k
61 60 rexrd φk1k*
62 61 adantlr φxAk1k*
63 elioopnf 1k*Fx1k+∞Fx1k<Fx
64 62 63 syl φxAkFx1k+∞Fx1k<Fx
65 56 58 64 3bitr2d φxAkxF-11k+∞Fx1k<Fx
66 id kk
67 imaexg F-1VF-11k+∞V
68 14 67 syl φF-11k+∞V
69 68 adantr φxAF-11k+∞V
70 oveq2 n=k1n=1k
71 70 oveq1d n=k1n+∞=1k+∞
72 71 imaeq2d n=kF-11n+∞=F-11k+∞
73 eqid nF-11n+∞=nF-11n+∞
74 72 73 fvmptg kF-11k+∞VnF-11n+∞k=F-11k+∞
75 66 69 74 syl2anr φxAknF-11n+∞k=F-11k+∞
76 75 eleq2d φxAkxnF-11n+∞kxF-11k+∞
77 50 adantr φxAkFx
78 77 biantrurd φxAk1k<FxFx1k<Fx
79 65 76 78 3bitr4rd φxAk1k<FxxnF-11n+∞k
80 79 rexbidva φxAk1k<FxkxnF-11n+∞k
81 52 80 mpbid φxAkxnF-11n+∞k
82 81 ex φxAkxnF-11n+∞k
83 eluni2 xrannF-11n+∞zrannF-11n+∞xz
84 eleq2 z=nF-11n+∞kxzxnF-11n+∞k
85 84 rexrn nF-11n+∞FnzrannF-11n+∞xzkxnF-11n+∞k
86 19 85 syl φzrannF-11n+∞xzkxnF-11n+∞k
87 83 86 syl5bb φxrannF-11n+∞kxnF-11n+∞k
88 82 87 sylibrd φxAxrannF-11n+∞
89 88 ssrdv φArannF-11n+∞
90 ovolss ArannF-11n+∞rannF-11n+∞vol*Avol*rannF-11n+∞
91 89 35 90 syl2anc φvol*Avol*rannF-11n+∞
92 42 91 eqbrtrd φvolAvol*rannF-11n+∞
93 92 adantr φ¬0<2FvolAvol*rannF-11n+∞
94 mblvol rannF-11n+∞domvolvolrannF-11n+∞=vol*rannF-11n+∞
95 33 94 syl φvolrannF-11n+∞=vol*rannF-11n+∞
96 peano2nn kk+1
97 96 adantl φkk+1
98 nnrecre k+11k+1
99 97 98 syl φk1k+1
100 99 rexrd φk1k+1*
101 nnre kk
102 101 adantl φkk
103 102 lep1d φkkk+1
104 nngt0 k0<k
105 104 adantl φk0<k
106 97 nnred φkk+1
107 97 nngt0d φk0<k+1
108 lerec k0<kk+10<k+1kk+11k+11k
109 102 105 106 107 108 syl22anc φkkk+11k+11k
110 103 109 mpbid φk1k+11k
111 iooss1 1k+1*1k+11k1k+∞1k+1+∞
112 100 110 111 syl2anc φk1k+∞1k+1+∞
113 imass2 1k+∞1k+1+∞F-11k+∞F-11k+1+∞
114 112 113 syl φkF-11k+∞F-11k+1+∞
115 66 68 74 syl2anr φknF-11n+∞k=F-11k+∞
116 imaexg F-1VF-11k+1+∞V
117 14 116 syl φF-11k+1+∞V
118 oveq2 n=k+11n=1k+1
119 118 oveq1d n=k+11n+∞=1k+1+∞
120 119 imaeq2d n=k+1F-11n+∞=F-11k+1+∞
121 120 73 fvmptg k+1F-11k+1+∞VnF-11n+∞k+1=F-11k+1+∞
122 96 117 121 syl2anr φknF-11n+∞k+1=F-11k+1+∞
123 114 115 122 3sstr4d φknF-11n+∞knF-11n+∞k+1
124 123 ralrimiva φknF-11n+∞knF-11n+∞k+1
125 volsup nF-11n+∞:domvolknF-11n+∞knF-11n+∞k+1volrannF-11n+∞=supvolrannF-11n+∞*<
126 28 124 125 syl2anc φvolrannF-11n+∞=supvolrannF-11n+∞*<
127 95 126 eqtr3d φvol*rannF-11n+∞=supvolrannF-11n+∞*<
128 127 adantr φ¬0<2Fvol*rannF-11n+∞=supvolrannF-11n+∞*<
129 68 adantr φ¬0<2FF-11k+∞V
130 66 129 74 syl2anr φ¬0<2FknF-11n+∞k=F-11k+∞
131 130 fveq2d φ¬0<2FkvolnF-11n+∞k=volF-11k+∞
132 39 a1i φk0<volF-11k+∞0*
133 nnrecgt0 k0<1k
134 133 adantl φk0<1k
135 0re 0
136 ltle 01k0<1k01k
137 135 60 136 sylancr φk0<1k01k
138 134 137 mpd φk01k
139 elxrge0 1k0+∞1k*01k
140 61 138 139 sylanbrc φk1k0+∞
141 0e0iccpnf 00+∞
142 ifcl 1k0+∞00+∞ifxF-11k+∞1k00+∞
143 140 141 142 sylancl φkifxF-11k+∞1k00+∞
144 143 adantr φkxifxF-11k+∞1k00+∞
145 144 fmpttd φkxifxF-11k+∞1k0:0+∞
146 145 adantrr φk0<volF-11k+∞xifxF-11k+∞1k0:0+∞
147 itg2cl xifxF-11k+∞1k0:0+∞2xifxF-11k+∞1k0*
148 146 147 syl φk0<volF-11k+∞2xifxF-11k+∞1k0*
149 icossicc 0+∞0+∞
150 fss F:0+∞0+∞0+∞F:0+∞
151 3 149 150 sylancl φF:0+∞
152 itg2cl F:0+∞2F*
153 151 152 syl φ2F*
154 153 adantr φk0<volF-11k+∞2F*
155 0nrp ¬0+
156 simpr φk0<volF-11k+∞0=2xifxF-11k+∞1k00=2xifxF-11k+∞1k0
157 115 29 eqeltrrd φkF-11k+∞domvol
158 157 adantrr φk0<volF-11k+∞F-11k+∞domvol
159 158 adantr φk0<volF-11k+∞0=2xifxF-11k+∞1k0F-11k+∞domvol
160 156 135 eqeltrrdi φk0<volF-11k+∞0=2xifxF-11k+∞1k02xifxF-11k+∞1k0
161 60 134 elrpd φk1k+
162 161 adantrr φk0<volF-11k+∞1k+
163 162 adantr φk0<volF-11k+∞0=2xifxF-11k+∞1k01k+
164 itg2const2 F-11k+∞domvol1k+volF-11k+∞2xifxF-11k+∞1k0
165 159 163 164 syl2anc φk0<volF-11k+∞0=2xifxF-11k+∞1k0volF-11k+∞2xifxF-11k+∞1k0
166 160 165 mpbird φk0<volF-11k+∞0=2xifxF-11k+∞1k0volF-11k+∞
167 elrege0 1k0+∞1k01k
168 60 138 167 sylanbrc φk1k0+∞
169 168 adantrr φk0<volF-11k+∞1k0+∞
170 169 adantr φk0<volF-11k+∞0=2xifxF-11k+∞1k01k0+∞
171 itg2const F-11k+∞domvolvolF-11k+∞1k0+∞2xifxF-11k+∞1k0=1kvolF-11k+∞
172 159 166 170 171 syl3anc φk0<volF-11k+∞0=2xifxF-11k+∞1k02xifxF-11k+∞1k0=1kvolF-11k+∞
173 156 172 eqtrd φk0<volF-11k+∞0=2xifxF-11k+∞1k00=1kvolF-11k+∞
174 simplrr φk0<volF-11k+∞0=2xifxF-11k+∞1k00<volF-11k+∞
175 166 174 elrpd φk0<volF-11k+∞0=2xifxF-11k+∞1k0volF-11k+∞+
176 163 175 rpmulcld φk0<volF-11k+∞0=2xifxF-11k+∞1k01kvolF-11k+∞+
177 173 176 eqeltrd φk0<volF-11k+∞0=2xifxF-11k+∞1k00+
178 177 ex φk0<volF-11k+∞0=2xifxF-11k+∞1k00+
179 155 178 mtoi φk0<volF-11k+∞¬0=2xifxF-11k+∞1k0
180 itg2ge0 xifxF-11k+∞1k0:0+∞02xifxF-11k+∞1k0
181 146 180 syl φk0<volF-11k+∞02xifxF-11k+∞1k0
182 xrleloe 0*2xifxF-11k+∞1k0*02xifxF-11k+∞1k00<2xifxF-11k+∞1k00=2xifxF-11k+∞1k0
183 39 148 182 sylancr φk0<volF-11k+∞02xifxF-11k+∞1k00<2xifxF-11k+∞1k00=2xifxF-11k+∞1k0
184 181 183 mpbid φk0<volF-11k+∞0<2xifxF-11k+∞1k00=2xifxF-11k+∞1k0
185 184 ord φk0<volF-11k+∞¬0<2xifxF-11k+∞1k00=2xifxF-11k+∞1k0
186 179 185 mt3d φk0<volF-11k+∞0<2xifxF-11k+∞1k0
187 151 adantr φk0<volF-11k+∞F:0+∞
188 60 adantr φkxF-11k+∞1k
189 53 adantr φkFFn
190 189 55 syl φkxF-11k+∞xFx1k+∞
191 190 biimpa φkxF-11k+∞xFx1k+∞
192 191 simpld φkxF-11k+∞x
193 49 adantlr φkxFx
194 192 193 syldan φkxF-11k+∞Fx
195 61 adantr φkxF-11k+∞1k*
196 191 simprd φkxF-11k+∞Fx1k+∞
197 simpr Fx1k<Fx1k<Fx
198 63 197 syl6bi 1k*Fx1k+∞1k<Fx
199 195 196 198 sylc φkxF-11k+∞1k<Fx
200 188 194 199 ltled φkxF-11k+∞1kFx
201 48 simprd φx0Fx
202 201 adantlr φkx0Fx
203 192 202 syldan φkxF-11k+∞0Fx
204 breq1 1k=ifxF-11k+∞1k01kFxifxF-11k+∞1k0Fx
205 breq1 0=ifxF-11k+∞1k00FxifxF-11k+∞1k0Fx
206 204 205 ifboth 1kFx0FxifxF-11k+∞1k0Fx
207 200 203 206 syl2anc φkxF-11k+∞ifxF-11k+∞1k0Fx
208 207 adantlr φkxxF-11k+∞ifxF-11k+∞1k0Fx
209 iffalse ¬xF-11k+∞ifxF-11k+∞1k0=0
210 209 adantl φkx¬xF-11k+∞ifxF-11k+∞1k0=0
211 202 adantr φkx¬xF-11k+∞0Fx
212 210 211 eqbrtrd φkx¬xF-11k+∞ifxF-11k+∞1k0Fx
213 208 212 pm2.61dan φkxifxF-11k+∞1k0Fx
214 213 ralrimiva φkxifxF-11k+∞1k0Fx
215 214 adantrr φk0<volF-11k+∞xifxF-11k+∞1k0Fx
216 reex V
217 216 a1i φV
218 ovex 1kV
219 c0ex 0V
220 218 219 ifex ifxF-11k+∞1k0V
221 220 a1i φxifxF-11k+∞1k0V
222 fvexd φxFxV
223 eqidd φxifxF-11k+∞1k0=xifxF-11k+∞1k0
224 3 feqmptd φF=xFx
225 217 221 222 223 224 ofrfval2 φxifxF-11k+∞1k0fFxifxF-11k+∞1k0Fx
226 225 biimpar φxifxF-11k+∞1k0FxxifxF-11k+∞1k0fF
227 215 226 syldan φk0<volF-11k+∞xifxF-11k+∞1k0fF
228 itg2le xifxF-11k+∞1k0:0+∞F:0+∞xifxF-11k+∞1k0fF2xifxF-11k+∞1k02F
229 146 187 227 228 syl3anc φk0<volF-11k+∞2xifxF-11k+∞1k02F
230 132 148 154 186 229 xrltletrd φk0<volF-11k+∞0<2F
231 230 expr φk0<volF-11k+∞0<2F
232 231 con3d φk¬0<2F¬0<volF-11k+∞
233 7 ffvelrni F-11k+∞domvolvolF-11k+∞0+∞
234 6 233 sselid F-11k+∞domvolvolF-11k+∞*
235 157 234 syl φkvolF-11k+∞*
236 xrlenlt volF-11k+∞*0*volF-11k+∞0¬0<volF-11k+∞
237 235 39 236 sylancl φkvolF-11k+∞0¬0<volF-11k+∞
238 232 237 sylibrd φk¬0<2FvolF-11k+∞0
239 238 imp φk¬0<2FvolF-11k+∞0
240 239 an32s φ¬0<2FkvolF-11k+∞0
241 131 240 eqbrtrd φ¬0<2FkvolnF-11n+∞k0
242 241 ralrimiva φ¬0<2FkvolnF-11n+∞k0
243 ffn nF-11n+∞:VnF-11n+∞Fn
244 fveq2 z=nF-11n+∞kvolz=volnF-11n+∞k
245 244 breq1d z=nF-11n+∞kvolz0volnF-11n+∞k0
246 245 ralrn nF-11n+∞FnzrannF-11n+∞volz0kvolnF-11n+∞k0
247 18 243 246 3syl φzrannF-11n+∞volz0kvolnF-11n+∞k0
248 247 adantr φ¬0<2FzrannF-11n+∞volz0kvolnF-11n+∞k0
249 242 248 mpbird φ¬0<2FzrannF-11n+∞volz0
250 ffn vol:domvol0+∞volFndomvol
251 7 250 ax-mp volFndomvol
252 28 frnd φrannF-11n+∞domvol
253 252 adantr φ¬0<2FrannF-11n+∞domvol
254 breq1 x=volzx0volz0
255 254 ralima volFndomvolrannF-11n+∞domvolxvolrannF-11n+∞x0zrannF-11n+∞volz0
256 251 253 255 sylancr φ¬0<2FxvolrannF-11n+∞x0zrannF-11n+∞volz0
257 249 256 mpbird φ¬0<2FxvolrannF-11n+∞x0
258 imassrn volrannF-11n+∞ranvol
259 frn vol:domvol0+∞ranvol0+∞
260 7 259 ax-mp ranvol0+∞
261 260 6 sstri ranvol*
262 258 261 sstri volrannF-11n+∞*
263 supxrleub volrannF-11n+∞*0*supvolrannF-11n+∞*<0xvolrannF-11n+∞x0
264 262 39 263 mp2an supvolrannF-11n+∞*<0xvolrannF-11n+∞x0
265 257 264 sylibr φ¬0<2FsupvolrannF-11n+∞*<0
266 128 265 eqbrtrd φ¬0<2Fvol*rannF-11n+∞0
267 11 38 40 93 266 xrletrd φ¬0<2FvolA0
268 267 ex φ¬0<2FvolA0
269 xrlenlt volA*0*volA0¬0<volA
270 10 39 269 sylancl φvolA0¬0<volA
271 268 270 sylibd φ¬0<2F¬0<volA
272 2 271 mt4d φ0<2F