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

Theorem itg2i1fseq3 19602
 Description: Special case of itg2i1fseq2 19601: if the integral of is a real number, then the standard limit relation holds on the integrals of simple functions approaching . (Contributed by Mario Carneiro, 17-Aug-2014.)
Hypotheses
Ref Expression
itg2i1fseq.1 MblFn
itg2i1fseq.2
itg2i1fseq.3
itg2i1fseq.4
itg2i1fseq.5
itg2i1fseq.6
itg2i1fseq3.7
Assertion
Ref Expression
itg2i1fseq3
Distinct variable groups:   ,,,   ,,,   ,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem itg2i1fseq3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 itg2i1fseq.1 . 2 MblFn
2 itg2i1fseq.2 . 2
3 itg2i1fseq.3 . 2
4 itg2i1fseq.4 . 2
5 itg2i1fseq.5 . 2
6 itg2i1fseq.6 . 2
7 itg2i1fseq3.7 . 2
8 rexr 9086 . . . . . . . 8
98anim1i 552 . . . . . . 7
10 elrege0 10963 . . . . . . 7
11 elxrge0 10964 . . . . . . 7
129, 10, 113imtr4i 258 . . . . . 6
1312ssriv 3312 . . . . 5
14 fss 5558 . . . . 5
152, 13, 14sylancl 644 . . . 4