Theorem ovnprodcl

Description: The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnprodcl.kph	⊢ Ⅎ 𝑘 𝜑
	ovnprodcl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnprodcl.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
	ovnprodcl.i	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
Assertion	ovnprodcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐹 ‘ 𝐼 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		ovnprodcl.kph	⊢ Ⅎ 𝑘 𝜑
2		ovnprodcl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		ovnprodcl.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
4		ovnprodcl.i	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
5	3 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
6		elmapi	⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝐹 ‘ 𝐼 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
7	5 6	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
8	1 2 7	hoiprodcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐹 ‘ 𝐼 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )