Metamath Proof Explorer


Theorem itg2i1fseq2

Description: In an extension to the results of itg2i1fseq , if there is an upper bound on the integrals of the simple functions approaching F , then S.2 F is real and the standard limit relation applies. (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 ) ) )
itg2i1fseq2.7
|- ( ph -> M e. RR )
itg2i1fseq2.8
|- ( ( ph /\ k e. NN ) -> ( S.1 ` ( P ` k ) ) <_ M )
Assertion itg2i1fseq2
|- ( 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 itg2i1fseq2.7
 |-  ( ph -> M e. RR )
8 itg2i1fseq2.8
 |-  ( ( ph /\ k e. NN ) -> ( S.1 ` ( P ` k ) ) <_ M )
9 nnuz
 |-  NN = ( ZZ>= ` 1 )
10 1zzd
 |-  ( ph -> 1 e. ZZ )
11 3 ffvelrnda
 |-  ( ( ph /\ m e. NN ) -> ( P ` m ) e. dom S.1 )
12 itg1cl
 |-  ( ( P ` m ) e. dom S.1 -> ( S.1 ` ( P ` m ) ) e. RR )
13 11 12 syl
 |-  ( ( ph /\ m e. NN ) -> ( S.1 ` ( P ` m ) ) e. RR )
14 13 6 fmptd
 |-  ( ph -> S : NN --> RR )
15 3 ffvelrnda
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) e. dom S.1 )
16 peano2nn
 |-  ( k e. NN -> ( k + 1 ) e. NN )
17 ffvelrn
 |-  ( ( P : NN --> dom S.1 /\ ( k + 1 ) e. NN ) -> ( P ` ( k + 1 ) ) e. dom S.1 )
18 3 16 17 syl2an
 |-  ( ( ph /\ k e. NN ) -> ( P ` ( k + 1 ) ) e. dom S.1 )
19 simpr
 |-  ( ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) -> ( P ` n ) oR <_ ( P ` ( n + 1 ) ) )
20 19 ralimi
 |-  ( A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) -> A. n e. NN ( P ` n ) oR <_ ( P ` ( n + 1 ) ) )
21 4 20 syl
 |-  ( ph -> A. n e. NN ( P ` n ) oR <_ ( P ` ( n + 1 ) ) )
22 fveq2
 |-  ( n = k -> ( P ` n ) = ( P ` k ) )
23 fvoveq1
 |-  ( n = k -> ( P ` ( n + 1 ) ) = ( P ` ( k + 1 ) ) )
24 22 23 breq12d
 |-  ( n = k -> ( ( P ` n ) oR <_ ( P ` ( n + 1 ) ) <-> ( P ` k ) oR <_ ( P ` ( k + 1 ) ) ) )
25 24 rspccva
 |-  ( ( A. n e. NN ( P ` n ) oR <_ ( P ` ( n + 1 ) ) /\ k e. NN ) -> ( P ` k ) oR <_ ( P ` ( k + 1 ) ) )
26 21 25 sylan
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) oR <_ ( P ` ( k + 1 ) ) )
27 itg1le
 |-  ( ( ( P ` k ) e. dom S.1 /\ ( P ` ( k + 1 ) ) e. dom S.1 /\ ( P ` k ) oR <_ ( P ` ( k + 1 ) ) ) -> ( S.1 ` ( P ` k ) ) <_ ( S.1 ` ( P ` ( k + 1 ) ) ) )
28 15 18 26 27 syl3anc
 |-  ( ( ph /\ k e. NN ) -> ( S.1 ` ( P ` k ) ) <_ ( S.1 ` ( P ` ( k + 1 ) ) ) )
29 2fveq3
 |-  ( m = k -> ( S.1 ` ( P ` m ) ) = ( S.1 ` ( P ` k ) ) )
30 fvex
 |-  ( S.1 ` ( P ` k ) ) e. _V
31 29 6 30 fvmpt
 |-  ( k e. NN -> ( S ` k ) = ( S.1 ` ( P ` k ) ) )
32 31 adantl
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) = ( S.1 ` ( P ` k ) ) )
33 2fveq3
 |-  ( m = ( k + 1 ) -> ( S.1 ` ( P ` m ) ) = ( S.1 ` ( P ` ( k + 1 ) ) ) )
34 fvex
 |-  ( S.1 ` ( P ` ( k + 1 ) ) ) e. _V
35 33 6 34 fvmpt
 |-  ( ( k + 1 ) e. NN -> ( S ` ( k + 1 ) ) = ( S.1 ` ( P ` ( k + 1 ) ) ) )
36 16 35 syl
 |-  ( k e. NN -> ( S ` ( k + 1 ) ) = ( S.1 ` ( P ` ( k + 1 ) ) ) )
37 36 adantl
 |-  ( ( ph /\ k e. NN ) -> ( S ` ( k + 1 ) ) = ( S.1 ` ( P ` ( k + 1 ) ) ) )
38 28 32 37 3brtr4d
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) <_ ( S ` ( k + 1 ) ) )
39 32 8 eqbrtrd
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) <_ M )
40 39 ralrimiva
 |-  ( ph -> A. k e. NN ( S ` k ) <_ M )
41 brralrspcev
 |-  ( ( M e. RR /\ A. k e. NN ( S ` k ) <_ M ) -> E. z e. RR A. k e. NN ( S ` k ) <_ z )
42 7 40 41 syl2anc
 |-  ( ph -> E. z e. RR A. k e. NN ( S ` k ) <_ z )
43 9 10 14 38 42 climsup
 |-  ( ph -> S ~~> sup ( ran S , RR , < ) )
44 1 2 3 4 5 6 itg2i1fseq
 |-  ( ph -> ( S.2 ` F ) = sup ( ran S , RR* , < ) )
45 14 frnd
 |-  ( ph -> ran S C_ RR )
46 6 13 dmmptd
 |-  ( ph -> dom S = NN )
47 1nn
 |-  1 e. NN
48 ne0i
 |-  ( 1 e. NN -> NN =/= (/) )
49 47 48 mp1i
 |-  ( ph -> NN =/= (/) )
50 46 49 eqnetrd
 |-  ( ph -> dom S =/= (/) )
51 dm0rn0
 |-  ( dom S = (/) <-> ran S = (/) )
52 51 necon3bii
 |-  ( dom S =/= (/) <-> ran S =/= (/) )
53 50 52 sylib
 |-  ( ph -> ran S =/= (/) )
54 ffn
 |-  ( S : NN --> RR -> S Fn NN )
55 breq1
 |-  ( y = ( S ` k ) -> ( y <_ z <-> ( S ` k ) <_ z ) )
56 55 ralrn
 |-  ( S Fn NN -> ( A. y e. ran S y <_ z <-> A. k e. NN ( S ` k ) <_ z ) )
57 14 54 56 3syl
 |-  ( ph -> ( A. y e. ran S y <_ z <-> A. k e. NN ( S ` k ) <_ z ) )
58 57 rexbidv
 |-  ( ph -> ( E. z e. RR A. y e. ran S y <_ z <-> E. z e. RR A. k e. NN ( S ` k ) <_ z ) )
59 42 58 mpbird
 |-  ( ph -> E. z e. RR A. y e. ran S y <_ z )
60 supxrre
 |-  ( ( ran S C_ RR /\ ran S =/= (/) /\ E. z e. RR A. y e. ran S y <_ z ) -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
61 45 53 59 60 syl3anc
 |-  ( ph -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
62 44 61 eqtrd
 |-  ( ph -> ( S.2 ` F ) = sup ( ran S , RR , < ) )
63 43 62 breqtrrd
 |-  ( ph -> S ~~> ( S.2 ` F ) )