# Metamath Proof Explorer

## Theorem volicc

Description: The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion volicc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to vol\left(\left[{A},{B}\right]\right)={B}-{A}$

### Proof

Step Hyp Ref Expression
1 iccmbl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\in \mathrm{dom}vol$
2 mblvol ${⊢}\left[{A},{B}\right]\in \mathrm{dom}vol\to vol\left(\left[{A},{B}\right]\right)={vol}^{*}\left(\left[{A},{B}\right]\right)$
3 1 2 syl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to vol\left(\left[{A},{B}\right]\right)={vol}^{*}\left(\left[{A},{B}\right]\right)$
4 3 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to vol\left(\left[{A},{B}\right]\right)={vol}^{*}\left(\left[{A},{B}\right]\right)$
5 ovolicc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to {vol}^{*}\left(\left[{A},{B}\right]\right)={B}-{A}$
6 4 5 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to vol\left(\left[{A},{B}\right]\right)={B}-{A}$