# 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 𝑘 𝜑
hoiprodcl.2 ( 𝜑𝑋 ∈ Fin )
hoiprodcl.3 ( 𝜑𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
Assertion hoiprodcl ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )

### Proof

Step Hyp Ref Expression
1 hoiprodcl.1 𝑘 𝜑
2 hoiprodcl.2 ( 𝜑𝑋 ∈ Fin )
3 hoiprodcl.3 ( 𝜑𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
4 0xr 0 ∈ ℝ*
5 4 a1i ( 𝜑 → 0 ∈ ℝ* )
6 pnfxr +∞ ∈ ℝ*
7 6 a1i ( 𝜑 → +∞ ∈ ℝ* )
8 3 adantr ( ( 𝜑𝑘𝑋 ) → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
9 simpr ( ( 𝜑𝑘𝑋 ) → 𝑘𝑋 )
10 8 9 fvovco ( ( 𝜑𝑘𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) )
11 10 fveq2d ( ( 𝜑𝑘𝑋 ) → ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) = ( vol ‘ ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) ) )
12 3 ffvelrnda ( ( 𝜑𝑘𝑋 ) → ( 𝐼𝑘 ) ∈ ( ℝ × ℝ ) )
13 xp1st ( ( 𝐼𝑘 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
14 12 13 syl ( ( 𝜑𝑘𝑋 ) → ( 1st ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
15 xp2nd ( ( 𝐼𝑘 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
16 12 15 syl ( ( 𝜑𝑘𝑋 ) → ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
17 volico ( ( ( 1st ‘ ( 𝐼𝑘 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ ℝ ) → ( vol ‘ ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) ) = if ( ( 1st ‘ ( 𝐼𝑘 ) ) < ( 2nd ‘ ( 𝐼𝑘 ) ) , ( ( 2nd ‘ ( 𝐼𝑘 ) ) − ( 1st ‘ ( 𝐼𝑘 ) ) ) , 0 ) )
18 14 16 17 syl2anc ( ( 𝜑𝑘𝑋 ) → ( vol ‘ ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) ) = if ( ( 1st ‘ ( 𝐼𝑘 ) ) < ( 2nd ‘ ( 𝐼𝑘 ) ) , ( ( 2nd ‘ ( 𝐼𝑘 ) ) − ( 1st ‘ ( 𝐼𝑘 ) ) ) , 0 ) )
19 11 18 eqtrd ( ( 𝜑𝑘𝑋 ) → ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) = if ( ( 1st ‘ ( 𝐼𝑘 ) ) < ( 2nd ‘ ( 𝐼𝑘 ) ) , ( ( 2nd ‘ ( 𝐼𝑘 ) ) − ( 1st ‘ ( 𝐼𝑘 ) ) ) , 0 ) )
20 16 14 resubcld ( ( 𝜑𝑘𝑋 ) → ( ( 2nd ‘ ( 𝐼𝑘 ) ) − ( 1st ‘ ( 𝐼𝑘 ) ) ) ∈ ℝ )
21 0red ( ( 𝜑𝑘𝑋 ) → 0 ∈ ℝ )
22 20 21 ifcld ( ( 𝜑𝑘𝑋 ) → if ( ( 1st ‘ ( 𝐼𝑘 ) ) < ( 2nd ‘ ( 𝐼𝑘 ) ) , ( ( 2nd ‘ ( 𝐼𝑘 ) ) − ( 1st ‘ ( 𝐼𝑘 ) ) ) , 0 ) ∈ ℝ )
23 19 22 eqeltrd ( ( 𝜑𝑘𝑋 ) → ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ℝ )
24 1 2 23 fprodreclf ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ℝ )
25 24 rexrd ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ℝ* )
26 16 rexrd ( ( 𝜑𝑘𝑋 ) → ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ ℝ* )
27 icombl ( ( ( 1st ‘ ( 𝐼𝑘 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ ℝ* ) → ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) ∈ dom vol )
28 14 26 27 syl2anc ( ( 𝜑𝑘𝑋 ) → ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) ∈ dom vol )
29 10 28 eqeltrd ( ( 𝜑𝑘𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ dom vol )
30 volge0 ( ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ dom vol → 0 ≤ ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
31 29 30 syl ( ( 𝜑𝑘𝑋 ) → 0 ≤ ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
32 1 2 23 31 fprodge0 ( 𝜑 → 0 ≤ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) )
33 24 ltpnfd ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) < +∞ )
34 5 7 25 32 33 elicod ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )