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	ffvelcdmda	|- ( ( 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 ) )