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 φ$
	hoiprodcl.2	$⊢ φ \to X \in Fin$
	hoiprodcl.3	$⊢ φ \to I : X ⟶ ℝ^{2}$
Assertion	hoiprodcl	$⊢ φ \to \prod_{k \in X} vol (([.) \circ I) (k)) \in [0, +∞)$

Proof

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

Metamath Proof Explorer

Theorem hoiprodcl

Proof