| Step |
Hyp |
Ref |
Expression |
| 1 |
|
itg2lea.1 |
|- ( ph -> F : RR --> ( 0 [,] +oo ) ) |
| 2 |
|
itg2lea.2 |
|- ( ph -> G : RR --> ( 0 [,] +oo ) ) |
| 3 |
|
itg2lea.3 |
|- ( ph -> A C_ RR ) |
| 4 |
|
itg2lea.4 |
|- ( ph -> ( vol* ` A ) = 0 ) |
| 5 |
|
itg2eqa.5 |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) = ( G ` x ) ) |
| 6 |
|
itg2cl |
|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* ) |
| 7 |
1 6
|
syl |
|- ( ph -> ( S.2 ` F ) e. RR* ) |
| 8 |
|
itg2cl |
|- ( G : RR --> ( 0 [,] +oo ) -> ( S.2 ` G ) e. RR* ) |
| 9 |
2 8
|
syl |
|- ( ph -> ( S.2 ` G ) e. RR* ) |
| 10 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
| 11 |
|
eldifi |
|- ( x e. ( RR \ A ) -> x e. RR ) |
| 12 |
|
ffvelcdm |
|- ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,] +oo ) ) |
| 13 |
1 11 12
|
syl2an |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) e. ( 0 [,] +oo ) ) |
| 14 |
10 13
|
sselid |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) e. RR* ) |
| 15 |
14
|
xrleidd |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( F ` x ) ) |
| 16 |
15 5
|
breqtrd |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) ) |
| 17 |
1 2 3 4 16
|
itg2lea |
|- ( ph -> ( S.2 ` F ) <_ ( S.2 ` G ) ) |
| 18 |
5 15
|
eqbrtrrd |
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( G ` x ) <_ ( F ` x ) ) |
| 19 |
2 1 3 4 18
|
itg2lea |
|- ( ph -> ( S.2 ` G ) <_ ( S.2 ` F ) ) |
| 20 |
7 9 17 19
|
xrletrid |
|- ( ph -> ( S.2 ` F ) = ( S.2 ` G ) ) |