Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2i1fseqle Structured version   Unicode version

Theorem itg2i1fseqle 19648
 Description: Subject to the conditions coming from mbfi1fseq 19615, the sequence of simple functions are all less than the target function . (Contributed by Mario Carneiro, 17-Aug-2014.)
Hypotheses
Ref Expression
itg2i1fseq.1 MblFn
itg2i1fseq.2
itg2i1fseq.3
itg2i1fseq.4
itg2i1fseq.5
Assertion
Ref Expression
itg2i1fseqle
Distinct variable groups:   ,,   ,   ,,
Allowed substitution hints:   (,)   ()

Proof of Theorem itg2i1fseqle
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5730 . . . . . . 7
21fveq1d 5732 . . . . . 6
3 eqid 2438 . . . . . 6
4 fvex 5744 . . . . . 6
52, 3, 4fvmpt 5808 . . . . 5
65ad2antlr 709 . . . 4
7 nnuz 10523 . . . . 5
8 simplr 733 . . . . 5
9 itg2i1fseq.5 . . . . . . 7
10 fveq2 5730 . . . . . . . . . 10
1110mpteq2dv 4298 . . . . . . . . 9
12 fveq2 5730 . . . . . . . . 9
1311, 12breq12d 4227 . . . . . . . 8
1413rspccva 3053 . . . . . . 7
159, 14sylan 459 . . . . . 6
1615adantlr 697 . . . . 5
17 fveq2 5730 . . . . . . . . . 10
1817fveq1d 5732 . . . . . . . . 9
19 fvex 5744 . . . . . . . . 9
2018, 3, 19fvmpt 5808 . . . . . . . 8
2120adantl 454 . . . . . . 7
22 itg2i1fseq.3 . . . . . . . . . . 11
2322ffvelrnda 5872 . . . . . . . . . 10
24 i1ff 19570 . . . . . . . . . 10
2523, 24syl 16 . . . . . . . . 9
2625ffvelrnda 5872 . . . . . . . 8
2726an32s 781 . . . . . . 7
2821, 27eqeltrd 2512 . . . . . 6
2928adantllr 701 . . . . 5
30 itg2i1fseq.4 . . . . . . . . . . . 12
31 simpr 449 . . . . . . . . . . . . 13
3231ralimi 2783 . . . . . . . . . . . 12
3330, 32syl 16 . . . . . . . . . . 11
34 oveq1 6090 . . . . . . . . . . . . . 14
3534fveq2d 5734 . . . . . . . . . . . . 13
3617, 35breq12d 4227 . . . . . . . . . . . 12
3736rspccva 3053 . . . . . . . . . . 11
3833, 37sylan 459 . . . . . . . . . 10
39 ffn 5593 . . . . . . . . . . . 12
4023, 24, 393syl 19 . . . . . . . . . . 11
41 peano2nn 10014 . . . . . . . . . . . . 13
42 ffvelrn 5870 . . . . . . . . . . . . 13
4322, 41, 42syl2an 465 . . . . . . . . . . . 12
44 i1ff 19570 . . . . . . . . . . . 12
45 ffn 5593 . . . . . . . . . . . 12
4643, 44, 453syl 19 . . . . . . . . . . 11
47 reex 9083 . . . . . . . . . . . 12
4847a1i 11 . . . . . . . . . . 11
49 inidm 3552 . . . . . . . . . . 11
50 eqidd 2439 . . . . . . . . . . 11
51 eqidd 2439 . . . . . . . . . . 11
5240, 46, 48, 48, 49, 50, 51ofrfval 6315 . . . . . . . . . 10
5338, 52mpbid 203 . . . . . . . . 9
5453r19.21bi 2806 . . . . . . . 8
5554an32s 781 . . . . . . 7
56 fveq2 5730 . . . . . . . . . . 11
5756fveq1d 5732 . . . . . . . . . 10
58 fvex 5744 . . . . . . . . . 10
5957, 3, 58fvmpt 5808 . . . . . . . . 9
6041, 59syl 16 . . . . . . . 8
6160adantl 454 . . . . . . 7
6255, 21, 613brtr4d 4244 . . . . . 6
6362adantllr 701 . . . . 5
647, 8, 16, 29, 63climub 12457 . . . 4
656, 64eqbrtrrd 4236 . . 3
6665ralrimiva 2791 . 2
6722ffvelrnda 5872 . . . 4
68 i1ff 19570 . . . 4
69 ffn 5593 . . . 4
7067, 68, 693syl 19 . . 3
71 itg2i1fseq.2 . . . . . 6
72 rexr 9132 . . . . . . . . 9
7372anim1i 553 . . . . . . . 8
74 elrege0 11009 . . . . . . . 8
75 elxrge0 11010 . . . . . . . 8
7673, 74, 753imtr4i 259 . . . . . . 7
7776ssriv 3354 . . . . . 6
78 fss 5601 . . . . . 6
7971, 77, 78sylancl 645 . . . . 5
80 ffn 5593 . . . . 5
8179, 80syl 16 . . . 4