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	ffvelcdmi	⊢ ( 𝑆 ∈ 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 ‘ 𝑆 ) )