Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itg2gt0cn Unicode version

Theorem itg2gt0cn 26159
 Description: itg2gt0 19605 holds on functions continuous on an open interval in the absence of ax-cc 8271. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)
Hypotheses
Ref Expression
itg2gt0cn.2
itg2gt0cn.3
itg2gt0cn.5
itg2gt0cn.cn
Assertion
Ref Expression
itg2gt0cn
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem itg2gt0cn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0xr 9087 . . . 4
21a1i 11 . . 3
3 imassrn 5175 . . . . 5
4 itg2gt0cn.3 . . . . . . 7
5 frn 5556 . . . . . . 7
64, 5syl 16 . . . . . 6
7 icossxr 10951 . . . . . 6
86, 7syl6ss 3320 . . . . 5
93, 8syl5ss 3319 . . . 4
10 supxrcl 10849 . . . 4
119, 10syl 16 . . 3
12 itg2gt0cn.2 . . . . . 6
13 ltrelxr 9095 . . . . . . . . . 10
1413ssbri 4214 . . . . . . . . 9
1512, 14syl 16 . . . . . . . 8
16 brxp 4868 . . . . . . . 8
1715, 16sylib 189 . . . . . . 7
18 ioon0 10898 . . . . . . 7
1917, 18syl 16 . . . . . 6
2012, 19mpbird 224 . . . . 5
21 itg2gt0cn.5 . . . . . 6
2221ralrimiva 2749 . . . . 5
23 r19.2z 3677 . . . . 5
2420, 22, 23syl2anc 643 . . . 4
25 supxrlub 10860 . . . . . 6
269, 1, 25sylancl 644 . . . . 5
27 ffn 5550 . . . . . . 7
284, 27syl 16 . . . . . 6
29 ioossre 10928 . . . . . 6
30 breq2 4176 . . . . . . 7
3130rexima 5936 . . . . . 6
3228, 29, 31sylancl 644 . . . . 5
3326, 32bitrd 245 . . . 4
3424, 33mpbird 224 . . 3
35 qbtwnxr 10742 . . 3
362, 11, 34, 35syl3anc 1184 . 2
37 qre 10535 . . . . . . . . 9
3837adantr 452 . . . . . . . 8
39 simpr 448 . . . . . . . 8
4038, 39elrpd 10602 . . . . . . 7
4140anim1i 552 . . . . . 6
4241anasss 629 . . . . 5
43 simplr 732 . . . . . . 7
44 rpxr 10575 . . . . . . . . . . 11
45 supxrlub 10860 . . . . . . . . . . 11
469, 44, 45syl2an 464 . . . . . . . . . 10
47 breq2 4176 . . . . . . . . . . . . 13
4847rexima 5936 . . . . . . . . . . . 12
4928, 29, 48sylancl 644 . . . . . . . . . . 11
5049adantr 452 . . . . . . . . . 10
5146, 50bitrd 245 . . . . . . . . 9
52 itg2gt0cn.cn . . . . . . . . . . . . . . . . 17
5352ad3antrrr 711 . . . . . . . . . . . . . . . 16
54 simplr 732 . . . . . . . . . . . . . . . 16
55 fssres 5569 . . . . . . . . . . . . . . . . . . . . . . 23
5629, 55mpan2 653 . . . . . . . . . . . . . . . . . . . . . 22
57 elrege0 10963 . . . . . . . . . . . . . . . . . . . . . . . . 25
5857simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . 24
5958ssriv 3312 . . . . . . . . . . . . . . . . . . . . . . 23
60 fss 5558 . . . . . . . . . . . . . . . . . . . . . . 23
6159, 60mpan2 653 . . . . . . . . . . . . . . . . . . . . . 22
624, 56, 613syl 19 . . . . . . . . . . . . . . . . . . . . 21
6362adantr 452 . . . . . . . . . . . . . . . . . . . 20
6463ffvelrnda 5829 . . . . . . . . . . . . . . . . . . 19
65 rpre 10574 . . . . . . . . . . . . . . . . . . . 20
6665ad2antlr 708 . . . . . . . . . . . . . . . . . . 19
6764, 66resubcld 9421 . . . . . . . . . . . . . . . . . 18
6867adantr 452 . . . . . . . . . . . . . . . . 17
6966, 64posdifd 9569 . . . . . . . . . . . . . . . . . 18
7069biimpa 471 . . . . . . . . . . . . . . . . 17
7168, 70elrpd 10602 . . . . . . . . . . . . . . . 16
72 cncfi 18877 . . . . . . . . . . . . . . . 16
7353, 54, 71, 72syl3anc 1184 . . . . . . . . . . . . . . 15
7473ex 424 . . . . . . . . . . . . . 14
75 fvres 5704 . . . . . . . . . . . . . . . 16
7675breq2d 4184 . . . . . . . . . . . . . . 15
7776adantl 453 . . . . . . . . . . . . . 14
78 fvres 5704 . . . . . . . . . . . . . . . . . . . . 21
7978adantl 453 . . . . . . . . . . . . . . . . . . . 20
8075ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20
8179, 80oveq12d 6058 . . . . . . . . . . . . . . . . . . 19
8281fveq2d 5691 . . . . . . . . . . . . . . . . . 18
8375oveq1d 6055 . . . . . . . . . . . . . . . . . . 19
8483ad2antlr 708 . . . . . . . . . . . . . . . . . 18
8582, 84breq12d 4185 . . . . . . . . . . . . . . . . 17
8685imbi2d 308 . . . . . . . . . . . . . . . 16
8786ralbidva 2682 . . . . . . . . . . . . . . 15
8887rexbidv 2687 . . . . . . . . . . . . . 14
8974, 77, 883imtr3d 259 . . . . . . . . . . . . 13
9089imp 419 . . . . . . . . . . . 12
911a1i 11 . . . . . . . . . . . . . . 15
92 ioorp 10944 . . . . . . . . . . . . . . . . . . . . . 22
93 ioossicc 10952 . . . . . . . . . . . . . . . . . . . . . 22
9492, 93eqsstr3i 3339 . . . . . . . . . . . . . . . . . . . . 21
9594sseli 3304 . . . . . . . . . . . . . . . . . . . 20
96 0le0 10037 . . . . . . . . . . . . . . . . . . . . 21
97 elxrge0 10964 . . . . . . . . . . . . . . . . . . . . 21
981, 96, 97mpbir2an 887 . . . . . . . . . . . . . . . . . . . 20
99 ifcl 3735 . . . . . . . . . . . . . . . . . . . 20
10095, 98, 99sylancl 644 . . . . . . . . . . . . . . . . . . 19
101100adantr 452 . . . . . . . . . . . . . . . . . 18
102 eqid 2404 . . . . . . . . . . . . . . . . . 18
103101, 102fmptd 5852 . . . . . . . . . . . . . . . . 17
104 itg2cl 19577 . . . . . . . . . . . . . . . . 17
105103, 104syl 16 . . . . . . . . . . . . . . . 16
106105ad5antlr 716 . . . . . . . . . . . . . . 15
107 ifcl 3735 . . . . . . . . . . . . . . . . . . . 20
10895, 98, 107sylancl 644 . . . . . . . . . . . . . . . . . . 19
109108adantr 452 . . . . . . . . . . . . . . . . . 18
110 eqid 2404 . . . . . . . . . . . . . . . . . 18
111109, 110fmptd 5852 . . . . . . . . . . . . . . . . 17
112 itg2cl 19577 . . . . . . . . . . . . . . . . 17
113111, 112syl 16 . . . . . . . . . . . . . . . 16
114113ad5antlr 716 . . . . . . . . . . . . . . 15
11565ad4antlr 714 . . . . . . . . . . . . . . . . . 18
116 ioombl 19412 . . . . . . . . . . . . . . . . . . . . 21
117 mblvol 19379 . . . . . . . . . . . . . . . . . . . . 21
118116, 117ax-mp 8 . . . . . . . . . . . . . . . . . . . 20
119 elioore 10902 . . . . . . . . . . . . . . . . . . . . . . . . 25
120119ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . 24
121 rpre 10574 . . . . . . . . . . . . . . . . . . . . . . . . 25
122121adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24
123120, 122resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . 23
124123adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
125123rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . 24
126125adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
12717simpld 446 . . . . . . . . . . . . . . . . . . . . . . . 24
128127ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23
12917simprd 450 . . . . . . . . . . . . . . . . . . . . . . . 24
130129ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23
131127ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25
132 xrltnle 9100 . . . . . . . . . . . . . . . . . . . . . . . . 25
133125, 131, 132syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24
134133biimpar 472 . . . . . . . . . . . . . . . . . . . . . . 23
13512ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23
136 xrre2 10714 . . . . . . . . . . . . . . . . . . . . . . 23
137126, 128, 130, 134, 135, 136syl32anc 1192 . . . . . . . . . . . . . . . . . . . . . 22
138124, 137ifclda 3726 . . . . . . . . . . . . . . . . . . . . 21
139129ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23
140122, 120readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . 24
141140adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
142 mnfxr 10670 . . . . . . . . . . . . . . . . . . . . . . . . . 26
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
144 mnfle 10685 . . . . . . . . . . . . . . . . . . . . . . . . . 26
145127, 144syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
146143, 127, 129, 145, 12xrlelttrd 10706 . . . . . . . . . . . . . . . . . . . . . . . 24
147146ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23
148 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23
149 xrre 10713 . . . . . . . . . . . . . . . . . . . . . . 23
150139, 141, 147, 148, 149syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . 22
151140adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
152150, 151ifclda 3726 . . . . . . . . . . . . . . . . . . . . 21
153120rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . 25
154129ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25
155 rpgt0 10579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
156155adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26
157122, 120ltsubposd 9568 . . . . . . . . . . . . . . . . . . . . . . . . . 26
158156, 157mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 25
159 eliooord 10926 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160159simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26
161160ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . 25
162125, 153, 154, 158, 161xrlttrd 10705 . . . . . . . . . . . . . . . . . . . . . . . 24
163122, 120ltaddpos2d 9567 . . . . . . . . . . . . . . . . . . . . . . . . . 26
164156, 163mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 25
165123, 120, 140, 158, 164lttrd 9187 . . . . . . . . . . . . . . . . . . . . . . . 24
166 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25
167 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25
168166, 167ifboth 3730 . . . . . . . . . . . . . . . . . . . . . . . 24
169162, 165, 168syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
17012ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . 24
171140rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . 25
172159simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . 26
173172ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . 25
174131, 153, 171, 173, 164xrlttrd 10705 . . . . . . . . . . . . . . . . . . . . . . . 24
175 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25
176 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25
177175, 176ifboth 3730 . . . . . . . . . . . . . . . . . . . . . . . 24
178170, 174, 177syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
179 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . 24
180 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . 24
181179, 180ifboth 3730 . . . . . . . . . . . . . . . . . . . . . . 23
182169, 178, 181syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
183138, 152, 182ltled 9177 . . . . . . . . . . . . . . . . . . . . 21
184 ovolioo 19415 . . . . . . . . . . . . . . . . . . . . 21
185138, 152, 183, 184syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20
186118, 185syl5eq 2448 . . . . . . . . . . . . . . . . . . 19
187152, 138resubcld 9421 . . . . . . . . . . . . . . . . . . 19
188186, 187eqeltrd 2478 . . . . . . . . . . . . . . . . . 18
189 rpgt0 10579 . . . . . . . . . . . . . . . . . . 19
190189ad4antlr 714 . . . . . . . . . . . . . . . . . 18
191138, 152posdifd 9569 . . . . . . . . . . . . . . . . . . . 20
192182, 191mpbid 202 . . . . . . . . . . . . . . . . . . 19
193192, 186breqtrrd 4198 . . . . . . . . . . . . . . . . . 18
194115, 188, 190, 193mulgt0d 9181 . . . . . . . . . . . . . . . . 17
195 iooin 10906 . . . . . . . . . . . . . . . . . . . . . . 23
196131, 154, 125, 171, 195syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . 22
197196eleq2d 2471 . . . . . . . . . . . . . . . . . . . . 21
198197ifbid 3717 . . . . . . . . . . . . . . . . . . . 20
199198mpteq2dv 4256 . . . . . . . . . . . . . . . . . . 19
200199fveq2d 5691 . . . . . . . . . . . . . . . . . 18
201116a1i 11 . . . . . . . . . . . . . . . . . . 19
202 rpge0 10580 . . . . . . . . . . . . . . . . . . . . 21
203 elrege0 10963 . . . . . . . . . . . . . . . . . . . . 21
20465, 202, 203sylanbrc 646 . . . . . . . . . . . . . . . . . . . 20
205204ad4antlr 714 . . . . . . . . . . . . . . . . . . 19
206 itg2const 19585 . . . . . . . . . . . . . . . . . . 19
207201, 188, 205, 206syl3anc 1184 . . . . . . . . . . . . . . . . . 18
208200, 207eqtrd 2436 . . . . . . . . . . . . . . . . 17
209194, 208breqtrrd 4198 . . . . . . . . . . . . . . . 16
210209adantr 452 . . . . . . . . . . . . . . 15
211103ad5antlr 716 . . . . . . . . . . . . . . . 16
212111ad5antlr 716 . . . . . . . . . . . . . . . 16
213 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
214213fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
215214breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . 26
216 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217216oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218217fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
219218breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . 26
220215, 219imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . 25
221220rspccva 3011 . . . . . . . . . . . . . . . . . . . . . . . 24
222 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25
223 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25
22465leidd 9549 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
225224ad6antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . 26
226119ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
227121ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
228226, 227resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
229228rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
230227, 226readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
231230rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
232 elioo2 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
233229, 231, 232syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
234 3anass 940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
235233, 234syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
236 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
237119ad5antlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
238236, 237resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
239121ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
240238, 239absltd 12187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
241239renegcld 9420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
242237, 241, 236ltaddsub2d 9583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243237recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
244239recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245243, 244negsubd 9373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
246245breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
247242, 246bitr3d 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
248236, 237, 239ltsubaddd 9578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
249247, 248anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
250240, 249bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
251250pm5.32da 623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
252235, 251bitr4d 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
253252biimpa 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
254 pm3.35 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
255254ancoms 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
25665ad6antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2574ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
258257ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
25959, 258sseldi 3306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
260259adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2614adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
262261ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
26359, 262sseldi 3306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
264119, 263sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
265264ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
266259, 265resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
267264, 66resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
268267ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
269266, 268absltd 12187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
270264recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
271 rpcn 10576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
272271ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
273270, 272negsubdi2d 9383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
274273ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
275274breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
276275anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
277269, 276bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
278277simprbda 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
279264ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
280256, 260, 279ltsub1d 9591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
281278, 280mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
282256, 260, 281ltled 9177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
283255, 282sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
284283an4s 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28