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