Metamath Proof Explorer


Theorem measle0

Description: If the measure of a given set is bounded by zero, it is zero. (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Assertion measle0 MmeasuresSASMA0MA=0

Proof

Step Hyp Ref Expression
1 simp3 MmeasuresSASMA0MA0
2 measvxrge0 MmeasuresSASMA0+∞
3 elxrge0 MA0+∞MA*0MA
4 2 3 sylib MmeasuresSASMA*0MA
5 4 3adant3 MmeasuresSASMA0MA*0MA
6 5 simprd MmeasuresSASMA00MA
7 5 simpld MmeasuresSASMA0MA*
8 0xr 0*
9 xrletri3 MA*0*MA=0MA00MA
10 7 8 9 sylancl MmeasuresSASMA0MA=0MA00MA
11 1 6 10 mpbir2and MmeasuresSASMA0MA=0