Metamath Proof Explorer

Theorem hoidmvcl

Description: The dimensional volume of a multidimensional half-open interval is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvcl.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
hoidmvcl.x ⊢ φ → X ∈ Fin
hoidmvcl.a ⊢ φ → A : X ⟶ ℝ
hoidmvcl.b ⊢ φ → B : X ⟶ ℝ
Assertion hoidmvcl ⊢ φ → A L ⁡ X B ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 hoidmvcl.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
2 hoidmvcl.x ⊢ φ → X ∈ Fin
3 hoidmvcl.a ⊢ φ → A : X ⟶ ℝ
4 hoidmvcl.b ⊢ φ → B : X ⟶ ℝ
5 1 3 4 2 hoidmvval ⊢ φ → A L ⁡ X B = if X = ∅ 0 ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k
6 0e0icopnf ⊢ 0 ∈ 0 +∞
7 6 a1i ⊢ φ → 0 ∈ 0 +∞
8 0xr ⊢ 0 ∈ ℝ *
9 8 a1i ⊢ φ → 0 ∈ ℝ *
10 pnfxr ⊢ +∞ ∈ ℝ *
11 10 a1i ⊢ φ → +∞ ∈ ℝ *
12 3 ffvelcdmda ⊢ φ ∧ k ∈ X → A ⁡ k ∈ ℝ
13 4 ffvelcdmda ⊢ φ ∧ k ∈ X → B ⁡ k ∈ ℝ
14 volico ⊢ A ⁡ k ∈ ℝ ∧ B ⁡ k ∈ ℝ → vol ⁡ A ⁡ k B ⁡ k = if A ⁡ k < B ⁡ k B ⁡ k − A ⁡ k 0
15 12 13 14 syl2anc ⊢ φ ∧ k ∈ X → vol ⁡ A ⁡ k B ⁡ k = if A ⁡ k < B ⁡ k B ⁡ k − A ⁡ k 0
16 13 12 resubcld ⊢ φ ∧ k ∈ X → B ⁡ k − A ⁡ k ∈ ℝ
17 0red ⊢ φ ∧ k ∈ X → 0 ∈ ℝ
18 16 17 ifcld ⊢ φ ∧ k ∈ X → if A ⁡ k < B ⁡ k B ⁡ k − A ⁡ k 0 ∈ ℝ
19 15 18 eqeltrd ⊢ φ ∧ k ∈ X → vol ⁡ A ⁡ k B ⁡ k ∈ ℝ
20 2 19 fprodrecl ⊢ φ → ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k ∈ ℝ
21 20 rexrd ⊢ φ → ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k ∈ ℝ *
22 nfv ⊢ Ⅎ k φ
23 13 rexrd ⊢ φ ∧ k ∈ X → B ⁡ k ∈ ℝ *
24 icombl ⊢ A ⁡ k ∈ ℝ ∧ B ⁡ k ∈ ℝ * → A ⁡ k B ⁡ k ∈ dom ⁡ vol
25 12 23 24 syl2anc ⊢ φ ∧ k ∈ X → A ⁡ k B ⁡ k ∈ dom ⁡ vol
26 volge0 ⊢ A ⁡ k B ⁡ k ∈ dom ⁡ vol → 0 ≤ vol ⁡ A ⁡ k B ⁡ k
27 25 26 syl ⊢ φ ∧ k ∈ X → 0 ≤ vol ⁡ A ⁡ k B ⁡ k
28 22 2 19 27 fprodge0 ⊢ φ → 0 ≤ ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k
29 20 ltpnfd ⊢ φ → ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k < +∞
30 9 11 21 28 29 elicod ⊢ φ → ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k ∈ 0 +∞
31 7 30 ifcld ⊢ φ → if X = ∅ 0 ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k ∈ 0 +∞
32 5 31 eqeltrd ⊢ φ → A L ⁡ X B ∈ 0 +∞