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 
|- ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> ( M ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> ( M ` A ) <_ 0 )
2 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( M ` A ) e. ( 0 [,] +oo ) )
3 elxrge0 
 |-  ( ( M ` A ) e. ( 0 [,] +oo ) <-> ( ( M ` A ) e. RR* /\ 0 <_ ( M ` A ) ) )
4 2 3 sylib 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( ( M ` A ) e. RR* /\ 0 <_ ( M ` A ) ) )
5 4 3adant3 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> ( ( M ` A ) e. RR* /\ 0 <_ ( M ` A ) ) )
6 5 simprd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> 0 <_ ( M ` A ) )
7 5 simpld 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> ( M ` A ) e. RR* )
8 0xr 
 |-  0 e. RR*
9 xrletri3 
 |-  ( ( ( M ` A ) e. RR* /\ 0 e. RR* ) -> ( ( M ` A ) = 0 <-> ( ( M ` A ) <_ 0 /\ 0 <_ ( M ` A ) ) ) )
10 7 8 9 sylancl 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> ( ( M ` A ) = 0 <-> ( ( M ` A ) <_ 0 /\ 0 <_ ( M ` A ) ) ) )
11 1 6 10 mpbir2and 
 |-  ( ( M e. ( measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> ( M ` A ) = 0 )