Metamath Proof Explorer

Theorem ovolmge0

Description: The set M is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis elovolm.1 
|- M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
Assertion ovolmge0 
|- ( B e. M -> 0 <_ B )

Proof

Step Hyp Ref Expression
1 elovolm.1 
 |-  M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
2 1 elovolm 
 |-  ( B e. M <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
3 elovolmlem 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> f : NN --> ( <_ i^i ( RR X. RR ) ) )
4 eqid 
 |-  ( ( abs o. - ) o. f ) = ( ( abs o. - ) o. f )
5 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
6 4 5 ovolsf 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) )
7 1nn 
 |-  1 e. NN
8 ffvelrn 
 |-  ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) /\ 1 e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. ( 0 [,) +oo ) )
9 6 7 8 sylancl 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. ( 0 [,) +oo ) )
10 elrege0 
 |-  ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. ( 0 [,) +oo ) <-> ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. RR /\ 0 <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) ) )
11 10 simprbi 
 |-  ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. ( 0 [,) +oo ) -> 0 <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) )
12 9 11 syl 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> 0 <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) )
13 6 frnd 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ ( 0 [,) +oo ) )
14 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
15 13 14 sstrdi 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* )
16 6 ffnd 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn NN )
17 fnfvelrn 
 |-  ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) Fn NN /\ 1 e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) )
18 16 7 17 sylancl 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) )
19 supxrub 
 |-  ( ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* /\ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. ran seq 1 ( + , ( ( abs o. - ) o. f ) ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
20 15 18 19 syl2anc 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
21 0xr 
 |-  0 e. RR*
22 14 9 sselid 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. RR* )
23 supxrcl 
 |-  ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
24 15 23 syl 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
25 xrletr 
 |-  ( ( 0 e. RR* /\ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) e. RR* /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* ) -> ( ( 0 <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) /\ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> 0 <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
26 21 22 24 25 mp3an2i 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( 0 <_ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) /\ ( seq 1 ( + , ( ( abs o. - ) o. f ) ) ` 1 ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> 0 <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
27 12 20 26 mp2and 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> 0 <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
28 3 27 sylbi 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> 0 <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
29 breq2 
 |-  ( B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) -> ( 0 <_ B <-> 0 <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
30 28 29 syl5ibrcom 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) -> 0 <_ B ) )
31 30 adantld 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> 0 <_ B ) )
32 31 rexlimiv 
 |-  ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> 0 <_ B )
33 2 32 sylbi 
 |-  ( B e. M -> 0 <_ B )