Metamath Proof Explorer

Theorem hoiprodcl3

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

Ref Expression
Hypotheses hoiprodcl3.k 
|- F/ k ph
hoiprodcl3.x 
|- ( ph -> X e. Fin )
hoiprodcl3.a 
|- ( ( ph /\ k e. X ) -> A e. RR )
hoiprodcl3.b 
|- ( ( ph /\ k e. X ) -> B e. RR )
Assertion hoiprodcl3 
|- ( ph -> prod_ k e. X ( vol ` ( A [,) B ) ) e. ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 hoiprodcl3.k 
 |-  F/ k ph
2 hoiprodcl3.x 
 |-  ( ph -> X e. Fin )
3 hoiprodcl3.a 
 |-  ( ( ph /\ k e. X ) -> A e. RR )
4 hoiprodcl3.b 
 |-  ( ( ph /\ k e. X ) -> B e. RR )
5 0xr 
 |-  0 e. RR*
6 5 a1i 
 |-  ( ph -> 0 e. RR* )
7 pnfxr 
 |-  +oo e. RR*
8 7 a1i 
 |-  ( ph -> +oo e. RR* )
9 volico 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
10 3 4 9 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )
11 4 3 resubcld 
 |-  ( ( ph /\ k e. X ) -> ( B - A ) e. RR )
12 0red 
 |-  ( ( ph /\ k e. X ) -> 0 e. RR )
13 11 12 ifcld 
 |-  ( ( ph /\ k e. X ) -> if ( A < B , ( B - A ) , 0 ) e. RR )
14 10 13 eqeltrd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( A [,) B ) ) e. RR )
15 1 2 14 fprodreclf 
 |-  ( ph -> prod_ k e. X ( vol ` ( A [,) B ) ) e. RR )
16 15 rexrd 
 |-  ( ph -> prod_ k e. X ( vol ` ( A [,) B ) ) e. RR* )
17 4 rexrd 
 |-  ( ( ph /\ k e. X ) -> B e. RR* )
18 icombl 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) e. dom vol )
19 3 17 18 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( A [,) B ) e. dom vol )
20 volge0 
 |-  ( ( A [,) B ) e. dom vol -> 0 <_ ( vol ` ( A [,) B ) ) )
21 19 20 syl 
 |-  ( ( ph /\ k e. X ) -> 0 <_ ( vol ` ( A [,) B ) ) )
22 1 2 14 21 fprodge0 
 |-  ( ph -> 0 <_ prod_ k e. X ( vol ` ( A [,) B ) ) )
23 15 ltpnfd 
 |-  ( ph -> prod_ k e. X ( vol ` ( A [,) B ) ) < +oo )
24 6 8 16 22 23 elicod 
 |-  ( ph -> prod_ k e. X ( vol ` ( A [,) B ) ) e. ( 0 [,) +oo ) )