Metamath Proof Explorer

Theorem iccvonmbl

Description: Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iccvonmbl.x ⊢ φ → X ∈ Fin
iccvonmbl.s ⊢ S = dom ⁡ voln ⁡ X
iccvonmbl.a ⊢ φ → A : X ⟶ ℝ
iccvonmbl.b ⊢ φ → B : X ⟶ ℝ
Assertion iccvonmbl ⊢ φ → ⨉ i ∈ X A ⁡ i B ⁡ i ∈ S

Proof

Step Hyp Ref Expression
1 iccvonmbl.x ⊢ φ → X ∈ Fin
2 iccvonmbl.s ⊢ S = dom ⁡ voln ⁡ X
3 iccvonmbl.a ⊢ φ → A : X ⟶ ℝ
4 iccvonmbl.b ⊢ φ → B : X ⟶ ℝ
5 fveq2 ⊢ j = i → A ⁡ j = A ⁡ i
6 5 oveq1d ⊢ j = i → A ⁡ j − 1 n = A ⁡ i − 1 n
7 6 cbvmptv ⊢ j ∈ X ⟼ A ⁡ j − 1 n = i ∈ X ⟼ A ⁡ i − 1 n
8 7 mpteq2i ⊢ n ∈ ℕ ⟼ j ∈ X ⟼ A ⁡ j − 1 n = n ∈ ℕ ⟼ i ∈ X ⟼ A ⁡ i − 1 n
9 fveq2 ⊢ j = i → B ⁡ j = B ⁡ i
10 9 oveq1d ⊢ j = i → B ⁡ j + 1 n = B ⁡ i + 1 n
11 10 cbvmptv ⊢ j ∈ X ⟼ B ⁡ j + 1 n = i ∈ X ⟼ B ⁡ i + 1 n
12 11 mpteq2i ⊢ n ∈ ℕ ⟼ j ∈ X ⟼ B ⁡ j + 1 n = n ∈ ℕ ⟼ i ∈ X ⟼ B ⁡ i + 1 n
13 1 2 3 4 8 12 iccvonmbllem ⊢ φ → ⨉ i ∈ X A ⁡ i B ⁡ i ∈ S