Metamath Proof Explorer


Theorem itg2i1fseq3

Description: Special case of itg2i1fseq2 : if the integral of F is a real number, then the standard limit relation holds on the integrals of simple functions approaching F . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2i1fseq.1
|- ( ph -> F e. MblFn )
itg2i1fseq.2
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2i1fseq.3
|- ( ph -> P : NN --> dom S.1 )
itg2i1fseq.4
|- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )
itg2i1fseq.5
|- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
itg2i1fseq.6
|- S = ( m e. NN |-> ( S.1 ` ( P ` m ) ) )
itg2i1fseq3.7
|- ( ph -> ( S.2 ` F ) e. RR )
Assertion itg2i1fseq3
|- ( ph -> S ~~> ( S.2 ` F ) )

Proof

Step Hyp Ref Expression
1 itg2i1fseq.1
 |-  ( ph -> F e. MblFn )
2 itg2i1fseq.2
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 itg2i1fseq.3
 |-  ( ph -> P : NN --> dom S.1 )
4 itg2i1fseq.4
 |-  ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )
5 itg2i1fseq.5
 |-  ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
6 itg2i1fseq.6
 |-  S = ( m e. NN |-> ( S.1 ` ( P ` m ) ) )
7 itg2i1fseq3.7
 |-  ( ph -> ( S.2 ` F ) e. RR )
8 icossicc
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
9 fss
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
10 2 8 9 sylancl
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
11 10 adantr
 |-  ( ( ph /\ k e. NN ) -> F : RR --> ( 0 [,] +oo ) )
12 3 ffvelrnda
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) e. dom S.1 )
13 1 2 3 4 5 itg2i1fseqle
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) oR <_ F )
14 itg2ub
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( P ` k ) e. dom S.1 /\ ( P ` k ) oR <_ F ) -> ( S.1 ` ( P ` k ) ) <_ ( S.2 ` F ) )
15 11 12 13 14 syl3anc
 |-  ( ( ph /\ k e. NN ) -> ( S.1 ` ( P ` k ) ) <_ ( S.2 ` F ) )
16 1 2 3 4 5 6 7 15 itg2i1fseq2
 |-  ( ph -> S ~~> ( S.2 ` F ) )