hoiprodcl3

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

Step	Hyp	Ref	Expression
1		hoiprodcl3.k	$⊢ Ⅎ k φ$
2		hoiprodcl3.x	$⊢ φ \to X \in Fin$
3		hoiprodcl3.a	$⊢ (φ \land k \in X) \to A \in ℝ$
4		hoiprodcl3.b	$⊢ (φ \land k \in X) \to B \in ℝ$
5		0xr	$⊢ 0 \in ℝ^{*}$
6	5	a1i	$⊢ φ \to 0 \in ℝ^{*}$
7		pnfxr	$⊢ +∞ \in ℝ^{*}$
8	7	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
9		volico	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) = if (A < B, B - A, 0)$
10	3 4 9	syl2anc	$⊢ (φ \land k \in X) \to vol ([A, B)) = if (A < B, B - A, 0)$
11	4 3	resubcld	$⊢ (φ \land k \in X) \to B - A \in ℝ$
12		0red	$⊢ (φ \land k \in X) \to 0 \in ℝ$
13	11 12	ifcld	$⊢ (φ \land k \in X) \to if (A < B, B - A, 0) \in ℝ$
14	10 13	eqeltrd	$⊢ (φ \land k \in X) \to vol ([A, B)) \in ℝ$
15	1 2 14	fprodreclf	$⊢ φ \to \prod_{k \in X} vol ([A, B)) \in ℝ$
16	15	rexrd	$⊢ φ \to \prod_{k \in X} vol ([A, B)) \in ℝ^{*}$
17	4	rexrd	$⊢ (φ \land k \in X) \to B \in ℝ^{*}$
18		icombl	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \in dom vol$
19	3 17 18	syl2anc	$⊢ (φ \land k \in X) \to [A, B) \in dom vol$
20		volge0	$⊢ [A, B) \in dom vol \to 0 \leq vol ([A, B))$
21	19 20	syl	$⊢ (φ \land k \in X) \to 0 \leq vol ([A, B))$
22	1 2 14 21	fprodge0	$⊢ φ \to 0 \leq \prod_{k \in X} vol ([A, B))$
23	15	ltpnfd	$⊢ φ \to \prod_{k \in X} vol ([A, B)) < +∞$
24	6 8 16 22 23	elicod	$⊢ φ \to \prod_{k \in X} vol ([A, B)) \in [0, +∞)$

Metamath Proof Explorer