Metamath Proof Explorer


Theorem ioombl1lem2

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses ioombl1.b
|- B = ( A (,) +oo )
ioombl1.a
|- ( ph -> A e. RR )
ioombl1.e
|- ( ph -> E C_ RR )
ioombl1.v
|- ( ph -> ( vol* ` E ) e. RR )
ioombl1.c
|- ( ph -> C e. RR+ )
ioombl1.s
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ioombl1.t
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
ioombl1.u
|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ioombl1.f1
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ioombl1.f2
|- ( ph -> E C_ U. ran ( (,) o. F ) )
ioombl1.f3
|- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) )
ioombl1.p
|- P = ( 1st ` ( F ` n ) )
ioombl1.q
|- Q = ( 2nd ` ( F ` n ) )
ioombl1.g
|- G = ( n e. NN |-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
ioombl1.h
|- H = ( n e. NN |-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
Assertion ioombl1lem2
|- ( ph -> sup ( ran S , RR* , < ) e. RR )

Proof

Step Hyp Ref Expression
1 ioombl1.b
 |-  B = ( A (,) +oo )
2 ioombl1.a
 |-  ( ph -> A e. RR )
3 ioombl1.e
 |-  ( ph -> E C_ RR )
4 ioombl1.v
 |-  ( ph -> ( vol* ` E ) e. RR )
5 ioombl1.c
 |-  ( ph -> C e. RR+ )
6 ioombl1.s
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
7 ioombl1.t
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
8 ioombl1.u
 |-  U = seq 1 ( + , ( ( abs o. - ) o. H ) )
9 ioombl1.f1
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
10 ioombl1.f2
 |-  ( ph -> E C_ U. ran ( (,) o. F ) )
11 ioombl1.f3
 |-  ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) )
12 ioombl1.p
 |-  P = ( 1st ` ( F ` n ) )
13 ioombl1.q
 |-  Q = ( 2nd ` ( F ` n ) )
14 ioombl1.g
 |-  G = ( n e. NN |-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
15 ioombl1.h
 |-  H = ( n e. NN |-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
16 eqid
 |-  ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
17 16 6 ovolsf
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
18 9 17 syl
 |-  ( ph -> S : NN --> ( 0 [,) +oo ) )
19 18 frnd
 |-  ( ph -> ran S C_ ( 0 [,) +oo ) )
20 icossxr
 |-  ( 0 [,) +oo ) C_ RR*
21 19 20 sstrdi
 |-  ( ph -> ran S C_ RR* )
22 supxrcl
 |-  ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
23 21 22 syl
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR* )
24 5 rpred
 |-  ( ph -> C e. RR )
25 4 24 readdcld
 |-  ( ph -> ( ( vol* ` E ) + C ) e. RR )
26 mnfxr
 |-  -oo e. RR*
27 26 a1i
 |-  ( ph -> -oo e. RR* )
28 18 ffnd
 |-  ( ph -> S Fn NN )
29 1nn
 |-  1 e. NN
30 fnfvelrn
 |-  ( ( S Fn NN /\ 1 e. NN ) -> ( S ` 1 ) e. ran S )
31 28 29 30 sylancl
 |-  ( ph -> ( S ` 1 ) e. ran S )
32 21 31 sseldd
 |-  ( ph -> ( S ` 1 ) e. RR* )
33 rge0ssre
 |-  ( 0 [,) +oo ) C_ RR
34 ffvelrn
 |-  ( ( S : NN --> ( 0 [,) +oo ) /\ 1 e. NN ) -> ( S ` 1 ) e. ( 0 [,) +oo ) )
35 18 29 34 sylancl
 |-  ( ph -> ( S ` 1 ) e. ( 0 [,) +oo ) )
36 33 35 sselid
 |-  ( ph -> ( S ` 1 ) e. RR )
37 36 mnfltd
 |-  ( ph -> -oo < ( S ` 1 ) )
38 supxrub
 |-  ( ( ran S C_ RR* /\ ( S ` 1 ) e. ran S ) -> ( S ` 1 ) <_ sup ( ran S , RR* , < ) )
39 21 31 38 syl2anc
 |-  ( ph -> ( S ` 1 ) <_ sup ( ran S , RR* , < ) )
40 27 32 23 37 39 xrltletrd
 |-  ( ph -> -oo < sup ( ran S , RR* , < ) )
41 xrre
 |-  ( ( ( sup ( ran S , RR* , < ) e. RR* /\ ( ( vol* ` E ) + C ) e. RR ) /\ ( -oo < sup ( ran S , RR* , < ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) ) ) -> sup ( ran S , RR* , < ) e. RR )
42 23 25 40 11 41 syl22anc
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR )