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

Theorem itg2i1fseqle 19125
 Description: Subject to the conditions coming from mbfi1fseq 19092, 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 5541 . . . . . . 7
21fveq1d 5543 . . . . . 6
3 eqid 2296 . . . . . 6
4 fvex 5555 . . . . . 6
52, 3, 4fvmpt 5618 . . . . 5
65ad2antlr 707 . . . 4
7 nnuz 10279 . . . . 5
8 simplr 731 . . . . 5
9 itg2i1fseq.5 . . . . . . 7
10 fveq2 5541 . . . . . . . . . 10
1110mpteq2dv 4123 . . . . . . . . 9
12 fveq2 5541 . . . . . . . . 9
1311, 12breq12d 4052 . . . . . . . 8
1413rspccva 2896 . . . . . . 7
159, 14sylan 457 . . . . . 6
1615adantlr 695 . . . . 5
17 fveq2 5541 . . . . . . . . . 10
1817fveq1d 5543 . . . . . . . . 9
19 fvex 5555 . . . . . . . . 9
2018, 3, 19fvmpt 5618 . . . . . . . 8
2120adantl 452 . . . . . . 7
22 itg2i1fseq.3 . . . . . . . . . . 11
23 ffvelrn 5679 . . . . . . . . . . 11
2422, 23sylan 457 . . . . . . . . . 10
25 i1ff 19047 . . . . . . . . . 10
2624, 25syl 15 . . . . . . . . 9
27 ffvelrn 5679 . . . . . . . . 9
2826, 27sylan 457 . . . . . . . 8
2928an32s 779 . . . . . . 7
3021, 29eqeltrd 2370 . . . . . 6
3130adantllr 699 . . . . 5
32 itg2i1fseq.4 . . . . . . . . . . . 12
33 simpr 447 . . . . . . . . . . . . 13
3433ralimi 2631 . . . . . . . . . . . 12
3532, 34syl 15 . . . . . . . . . . 11
36 oveq1 5881 . . . . . . . . . . . . . 14
3736fveq2d 5545 . . . . . . . . . . . . 13
3817, 37breq12d 4052 . . . . . . . . . . . 12
3938rspccva 2896 . . . . . . . . . . 11
4035, 39sylan 457 . . . . . . . . . 10
41 ffn 5405 . . . . . . . . . . . 12
4224, 25, 413syl 18 . . . . . . . . . . 11
43 peano2nn 9774 . . . . . . . . . . . . 13
44 ffvelrn 5679 . . . . . . . . . . . . 13
4522, 43, 44syl2an 463 . . . . . . . . . . . 12
46 i1ff 19047 . . . . . . . . . . . 12
47 ffn 5405 . . . . . . . . . . . 12
4845, 46, 473syl 18 . . . . . . . . . . 11
49 reex 8844 . . . . . . . . . . . 12
5049a1i 10 . . . . . . . . . . 11
51 inidm 3391 . . . . . . . . . . 11
52 eqidd 2297 . . . . . . . . . . 11
53 eqidd 2297 . . . . . . . . . . 11
5442, 48, 50, 50, 51, 52, 53ofrfval 6102 . . . . . . . . . 10
5540, 54mpbid 201 . . . . . . . . 9
5655r19.21bi 2654 . . . . . . . 8
5756an32s 779 . . . . . . 7
58 fveq2 5541 . . . . . . . . . . 11
5958fveq1d 5543 . . . . . . . . . 10
60 fvex 5555 . . . . . . . . . 10
6159, 3, 60fvmpt 5618 . . . . . . . . 9
6243, 61syl 15 . . . . . . . 8
6362adantl 452 . . . . . . 7
6457, 21, 633brtr4d 4069 . . . . . 6
6564adantllr 699 . . . . 5
667, 8, 16, 31, 65climub 12151 . . . 4
676, 66eqbrtrrd 4061 . . 3
6867ralrimiva 2639 . 2
69 ffvelrn 5679 . . . . 5
7022, 69sylan 457 . . . 4
71 i1ff 19047 . . . 4
72 ffn 5405 . . . 4
7370, 71, 723syl 18 . . 3
74 itg2i1fseq.2 . . . . . 6
75 rexr 8893 . . . . . . . . 9
7675anim1i 551 . . . . . . . 8
77 elrege0 10762 . . . . . . . 8
78 elxrge0 10763 . . . . . . . 8
7976, 77, 783imtr4i 257 . . . . . . 7
8079ssriv 3197 . . . . . 6
81 fss 5413 . . . . . 6
8274, 80, 81sylancl 643 . . . . 5
83 ffn 5405 . . . . 5
8482, 83syl 15 . . . 4