# Metamath Proof Explorer

## Theorem ovollb

Description: The outer volume is a lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Hypothesis ovollb.1
`|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )`
Assertion ovollb
`|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )`

### Proof

Step Hyp Ref Expression
1 ovollb.1
` |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )`
2 simpr
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> A C_ U. ran ( (,) o. F ) )`
3 ioof
` |-  (,) : ( RR* X. RR* ) --> ~P RR`
4 simpl
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )`
5 inss2
` |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )`
6 rexpssxrxp
` |-  ( RR X. RR ) C_ ( RR* X. RR* )`
7 5 6 sstri
` |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )`
8 fss
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )`
9 4 7 8 sylancl
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> F : NN --> ( RR* X. RR* ) )`
10 fco
` |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR )`
11 3 9 10 sylancr
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> ( (,) o. F ) : NN --> ~P RR )`
12 11 frnd
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> ran ( (,) o. F ) C_ ~P RR )`
13 sspwuni
` |-  ( ran ( (,) o. F ) C_ ~P RR <-> U. ran ( (,) o. F ) C_ RR )`
14 12 13 sylib
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> U. ran ( (,) o. F ) C_ RR )`
15 2 14 sstrd
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> A C_ RR )`
16 eqid
` |-  { 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* , < ) ) } = { 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* , < ) ) }`
17 16 ovolval
` |-  ( A C_ RR -> ( vol* ` A ) = inf ( { 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* , < ) ) } , RR* , < ) )`
18 15 17 syl
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> ( vol* ` A ) = inf ( { 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* , < ) ) } , RR* , < ) )`
19 ssrab2
` |-  { 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* , < ) ) } C_ RR*`
20 16 1 elovolmr
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> sup ( ran S , RR* , < ) e. { 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* , < ) ) } )`
21 infxrlb
` |-  ( ( { 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* , < ) ) } C_ RR* /\ sup ( ran S , RR* , < ) e. { 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* , < ) ) } ) -> inf ( { 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* , < ) ) } , RR* , < ) <_ sup ( ran S , RR* , < ) )`
22 19 20 21 sylancr
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> inf ( { 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* , < ) ) } , RR* , < ) <_ sup ( ran S , RR* , < ) )`
23 18 22 eqbrtrd
` |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )`