Metamath Proof Explorer


Theorem areaf

Description: Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areaf area : dom area 0 +∞

Proof

Step Hyp Ref Expression
1 dfarea area = s dom area vol s x dx
2 areambl s dom area x s x dom vol vol s x
3 2 simprd s dom area x vol s x
4 dmarea s dom area s 2 x s x vol -1 x vol s x 𝐿 1
5 4 simp3bi s dom area x vol s x 𝐿 1
6 3 5 itgrecl s dom area vol s x dx
7 2 simpld s dom area x s x dom vol
8 mblss s x dom vol s x
9 ovolge0 s x 0 vol * s x
10 7 8 9 3syl s dom area x 0 vol * s x
11 mblvol s x dom vol vol s x = vol * s x
12 7 11 syl s dom area x vol s x = vol * s x
13 10 12 breqtrrd s dom area x 0 vol s x
14 5 3 13 itgge0 s dom area 0 vol s x dx
15 elrege0 vol s x dx 0 +∞ vol s x dx 0 vol s x dx
16 6 14 15 sylanbrc s dom area vol s x dx 0 +∞
17 1 16 fmpti area : dom area 0 +∞