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