Metamath Proof Explorer


Theorem areaval

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

Ref Expression
Assertion areaval S dom area area S = vol S x dx

Proof

Step Hyp Ref Expression
1 simpl s = S x s = S
2 1 imaeq1d s = S x s x = S x
3 2 fveq2d s = S x vol s x = vol S x
4 3 itgeq2dv s = S vol s x dx = vol S x dx
5 dfarea area = s dom area vol s x dx
6 itgex vol S x dx V
7 4 5 6 fvmpt S dom area area S = vol S x dx