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 ffvelrni 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