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	⊢ Ⅎ 𝑘 𝜑
	hoiprodcl3.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hoiprodcl3.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
	hoiprodcl3.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
Assertion	hoiprodcl3	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		hoiprodcl3.k	⊢ Ⅎ 𝑘 𝜑
2		hoiprodcl3.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hoiprodcl3.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
4		hoiprodcl3.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
5		0xr	⊢ 0 ∈ ℝ^*
6	5	a1i	⊢ ( 𝜑 → 0 ∈ ℝ^* )
7		pnfxr	⊢ +∞ ∈ ℝ^*
8	7	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ^* )
9		volico	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
10	3 4 9	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
11	4 3	resubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
12		0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 0 ∈ ℝ )
13	11 12	ifcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) ∈ ℝ )
14	10 13	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
15	1 2 14	fprodreclf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
16	15	rexrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ^* )
17	4	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ^* )
18		icombl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
19	3 17 18	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
20		volge0	⊢ ( ( 𝐴 [,) 𝐵 ) ∈ dom vol → 0 ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
21	19 20	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 0 ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
22	1 2 14 21	fprodge0	⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
23	15	ltpnfd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 [,) 𝐵 ) ) < +∞ )
24	6 8 16 22 23	elicod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ( 0 [,) +∞ ) )

Metamath Proof Explorer

Theorem hoiprodcl3

Proof