# 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 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
hoiprodcl.2 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
hoiprodcl.3 ${⊢}{\phi }\to {I}:{X}⟶{ℝ}^{2}$
Assertion hoiprodcl ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)\in \left[0,\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 hoiprodcl.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 hoiprodcl.2 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
3 hoiprodcl.3 ${⊢}{\phi }\to {I}:{X}⟶{ℝ}^{2}$
4 0xr ${⊢}0\in {ℝ}^{*}$
5 4 a1i ${⊢}{\phi }\to 0\in {ℝ}^{*}$
6 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
7 6 a1i ${⊢}{\phi }\to \mathrm{+\infty }\in {ℝ}^{*}$
8 3 adantr ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {I}:{X}⟶{ℝ}^{2}$
9 simpr ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {k}\in {X}$
10 8 9 fvovco ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to \left(\left[.\right)\circ {I}\right)\left({k}\right)=\left[{1}^{st}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)\right)$
11 10 fveq2d ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)=vol\left(\left[{1}^{st}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)\right)\right)$
12 3 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {I}\left({k}\right)\in {ℝ}^{2}$
13 xp1st ${⊢}{I}\left({k}\right)\in {ℝ}^{2}\to {1}^{st}\left({I}\left({k}\right)\right)\in ℝ$
14 12 13 syl ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {1}^{st}\left({I}\left({k}\right)\right)\in ℝ$
15 xp2nd ${⊢}{I}\left({k}\right)\in {ℝ}^{2}\to {2}^{nd}\left({I}\left({k}\right)\right)\in ℝ$
16 12 15 syl ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {2}^{nd}\left({I}\left({k}\right)\right)\in ℝ$
17 volico ${⊢}\left({1}^{st}\left({I}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({I}\left({k}\right)\right)\in ℝ\right)\to vol\left(\left[{1}^{st}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)\right)\right)=if\left({1}^{st}\left({I}\left({k}\right)\right)<{2}^{nd}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)-{1}^{st}\left({I}\left({k}\right)\right),0\right)$
18 14 16 17 syl2anc ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to vol\left(\left[{1}^{st}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)\right)\right)=if\left({1}^{st}\left({I}\left({k}\right)\right)<{2}^{nd}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)-{1}^{st}\left({I}\left({k}\right)\right),0\right)$
19 11 18 eqtrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)=if\left({1}^{st}\left({I}\left({k}\right)\right)<{2}^{nd}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)-{1}^{st}\left({I}\left({k}\right)\right),0\right)$
20 16 14 resubcld ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {2}^{nd}\left({I}\left({k}\right)\right)-{1}^{st}\left({I}\left({k}\right)\right)\in ℝ$
21 0red ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to 0\in ℝ$
22 20 21 ifcld ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to if\left({1}^{st}\left({I}\left({k}\right)\right)<{2}^{nd}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)-{1}^{st}\left({I}\left({k}\right)\right),0\right)\in ℝ$
23 19 22 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)\in ℝ$
24 1 2 23 fprodreclf ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)\in ℝ$
25 24 rexrd ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)\in {ℝ}^{*}$
26 16 rexrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {2}^{nd}\left({I}\left({k}\right)\right)\in {ℝ}^{*}$
27 icombl ${⊢}\left({1}^{st}\left({I}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({I}\left({k}\right)\right)\in {ℝ}^{*}\right)\to \left[{1}^{st}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)\right)\in \mathrm{dom}vol$
28 14 26 27 syl2anc ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to \left[{1}^{st}\left({I}\left({k}\right)\right),{2}^{nd}\left({I}\left({k}\right)\right)\right)\in \mathrm{dom}vol$
29 10 28 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to \left(\left[.\right)\circ {I}\right)\left({k}\right)\in \mathrm{dom}vol$
30 volge0 ${⊢}\left(\left[.\right)\circ {I}\right)\left({k}\right)\in \mathrm{dom}vol\to 0\le vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)$
31 29 30 syl ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to 0\le vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)$
32 1 2 23 31 fprodge0 ${⊢}{\phi }\to 0\le \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)$
33 24 ltpnfd ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)<\mathrm{+\infty }$
34 5 7 25 32 33 elicod ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)\in \left[0,\mathrm{+\infty }\right)$