Metamath Proof Explorer


Theorem measge0

Description: A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018)

Ref Expression
Assertion measge0 MmeasuresSAS0MA

Proof

Step Hyp Ref Expression
1 measvxrge0 MmeasuresSASMA0+∞
2 elxrge0 MA0+∞MA*0MA
3 1 2 sylib MmeasuresSASMA*0MA
4 3 simprd MmeasuresSAS0MA