Metamath Proof Explorer

Theorem areacl

Description: The area of a measurable region is a real number. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areacl ⊢ S ∈ dom ⁡ area → area ⁡ S ∈ ℝ

Proof

Step Hyp Ref Expression
1 areaf ⊢ area : dom ⁡ area ⟶ 0 +∞
2 1 ffvelcdmi ⊢ S ∈ dom ⁡ area → area ⁡ S ∈ 0 +∞
3 elrege0 ⊢ area ⁡ S ∈ 0 +∞ ↔ area ⁡ S ∈ ℝ ∧ 0 ≤ area ⁡ S
4 3 simplbi ⊢ area ⁡ S ∈ 0 +∞ → area ⁡ S ∈ ℝ
5 2 4 syl ⊢ S ∈ dom ⁡ area → area ⁡ S ∈ ℝ