Metamath Proof Explorer


Theorem areage0

Description: The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areage0 ( 𝑆 ∈ dom area → 0 ≤ ( area ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 areaf area : dom area ⟶ ( 0 [,) +∞ )
2 1 ffvelrni ( 𝑆 ∈ dom area → ( area ‘ 𝑆 ) ∈ ( 0 [,) +∞ ) )
3 elrege0 ( ( area ‘ 𝑆 ) ∈ ( 0 [,) +∞ ) ↔ ( ( area ‘ 𝑆 ) ∈ ℝ ∧ 0 ≤ ( area ‘ 𝑆 ) ) )
4 3 simprbi ( ( area ‘ 𝑆 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( area ‘ 𝑆 ) )
5 2 4 syl ( 𝑆 ∈ dom area → 0 ≤ ( area ‘ 𝑆 ) )