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 ∈ measures ⁡ S ∧ A ∈ S ∧ M ⁡ A ≤ 0 → M ⁡ A = 0

Proof

Step Hyp Ref Expression
1 simp3 ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ M ⁡ A ≤ 0 → M ⁡ A ≤ 0
2 measvxrge0 ⊢ M ∈ measures ⁡ S ∧ A ∈ S → M ⁡ A ∈ 0 +∞
3 elxrge0 ⊢ M ⁡ A ∈ 0 +∞ ↔ M ⁡ A ∈ ℝ * ∧ 0 ≤ M ⁡ A
4 2 3 sylib ⊢ M ∈ measures ⁡ S ∧ A ∈ S → M ⁡ A ∈ ℝ * ∧ 0 ≤ M ⁡ A
5 4 3adant3 ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ M ⁡ A ≤ 0 → M ⁡ A ∈ ℝ * ∧ 0 ≤ M ⁡ A
6 5 simprd ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ M ⁡ A ≤ 0 → 0 ≤ M ⁡ A
7 5 simpld ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ M ⁡ A ≤ 0 → M ⁡ A ∈ ℝ *
8 0xr ⊢ 0 ∈ ℝ *
9 xrletri3 ⊢ M ⁡ A ∈ ℝ * ∧ 0 ∈ ℝ * → M ⁡ A = 0 ↔ M ⁡ A ≤ 0 ∧ 0 ≤ M ⁡ A
10 7 8 9 sylancl ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ M ⁡ A ≤ 0 → M ⁡ A = 0 ↔ M ⁡ A ≤ 0 ∧ 0 ≤ M ⁡ A
11 1 6 10 mpbir2and ⊢ M ∈ measures ⁡ S ∧ A ∈ S ∧ M ⁡ A ≤ 0 → M ⁡ A = 0