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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 | |
|
2 | measvxrge0 | |
|
3 | elxrge0 | |
|
4 | 2 3 | sylib | |
5 | 4 | 3adant3 | |
6 | 5 | simprd | |
7 | 5 | simpld | |
8 | 0xr | |
|
9 | xrletri3 | |
|
10 | 7 8 9 | sylancl | |
11 | 1 6 10 | mpbir2and | |