# Metamath Proof Explorer

## Theorem hoiprodcl

Description: The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses hoiprodcl.1
`|- F/ k ph`
hoiprodcl.2
`|- ( ph -> X e. Fin )`
hoiprodcl.3
`|- ( ph -> I : X --> ( RR X. RR ) )`
Assertion hoiprodcl
`|- ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. ( 0 [,) +oo ) )`

### Proof

Step Hyp Ref Expression
1 hoiprodcl.1
` |-  F/ k ph`
2 hoiprodcl.2
` |-  ( ph -> X e. Fin )`
3 hoiprodcl.3
` |-  ( ph -> I : X --> ( RR X. RR ) )`
4 0xr
` |-  0 e. RR*`
5 4 a1i
` |-  ( ph -> 0 e. RR* )`
6 pnfxr
` |-  +oo e. RR*`
7 6 a1i
` |-  ( ph -> +oo e. RR* )`
` |-  ( ( ph /\ k e. X ) -> I : X --> ( RR X. RR ) )`
9 simpr
` |-  ( ( ph /\ k e. X ) -> k e. X )`
10 8 9 fvovco
` |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) = ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) )`
11 10 fveq2d
` |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( [,) o. I ) ` k ) ) = ( vol ` ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) ) )`
12 3 ffvelrnda
` |-  ( ( ph /\ k e. X ) -> ( I ` k ) e. ( RR X. RR ) )`
13 xp1st
` |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 1st ` ( I ` k ) ) e. RR )`
14 12 13 syl
` |-  ( ( ph /\ k e. X ) -> ( 1st ` ( I ` k ) ) e. RR )`
15 xp2nd
` |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 2nd ` ( I ` k ) ) e. RR )`
16 12 15 syl
` |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. RR )`
17 volico
` |-  ( ( ( 1st ` ( I ` k ) ) e. RR /\ ( 2nd ` ( I ` k ) ) e. RR ) -> ( vol ` ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) ) = if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) )`
18 14 16 17 syl2anc
` |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) ) = if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) )`
19 11 18 eqtrd
` |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( [,) o. I ) ` k ) ) = if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) )`
20 16 14 resubcld
` |-  ( ( ph /\ k e. X ) -> ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) e. RR )`
21 0red
` |-  ( ( ph /\ k e. X ) -> 0 e. RR )`
22 20 21 ifcld
` |-  ( ( ph /\ k e. X ) -> if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) e. RR )`
23 19 22 eqeltrd
` |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( [,) o. I ) ` k ) ) e. RR )`
24 1 2 23 fprodreclf
` |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. RR )`
25 24 rexrd
` |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. RR* )`
26 16 rexrd
` |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. RR* )`
27 icombl
` |-  ( ( ( 1st ` ( I ` k ) ) e. RR /\ ( 2nd ` ( I ` k ) ) e. RR* ) -> ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) e. dom vol )`
28 14 26 27 syl2anc
` |-  ( ( ph /\ k e. X ) -> ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) e. dom vol )`
29 10 28 eqeltrd
` |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) e. dom vol )`
30 volge0
` |-  ( ( ( [,) o. I ) ` k ) e. dom vol -> 0 <_ ( vol ` ( ( [,) o. I ) ` k ) ) )`
31 29 30 syl
` |-  ( ( ph /\ k e. X ) -> 0 <_ ( vol ` ( ( [,) o. I ) ` k ) ) )`
32 1 2 23 31 fprodge0
` |-  ( ph -> 0 <_ prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) )`
33 24 ltpnfd
` |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) < +oo )`
34 5 7 25 32 33 elicod
` |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. ( 0 [,) +oo ) )`