| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ovolsca.1 |
|- ( ph -> A C_ RR ) |
| 2 |
|
ovolsca.2 |
|- ( ph -> C e. RR+ ) |
| 3 |
|
ovolsca.3 |
|- ( ph -> B = { x e. RR | ( C x. x ) e. A } ) |
| 4 |
|
ovolsca.4 |
|- ( ph -> ( vol* ` A ) e. RR ) |
| 5 |
1 2 3 4
|
ovolscalem2 |
|- ( ph -> ( vol* ` B ) <_ ( ( vol* ` A ) / C ) ) |
| 6 |
4
|
recnd |
|- ( ph -> ( vol* ` A ) e. CC ) |
| 7 |
2
|
rpcnd |
|- ( ph -> C e. CC ) |
| 8 |
2
|
rpne0d |
|- ( ph -> C =/= 0 ) |
| 9 |
6 7 8
|
divrecd |
|- ( ph -> ( ( vol* ` A ) / C ) = ( ( vol* ` A ) x. ( 1 / C ) ) ) |
| 10 |
|
ssrab2 |
|- { x e. RR | ( C x. x ) e. A } C_ RR |
| 11 |
3 10
|
eqsstrdi |
|- ( ph -> B C_ RR ) |
| 12 |
2
|
rpreccld |
|- ( ph -> ( 1 / C ) e. RR+ ) |
| 13 |
1 2 3
|
sca2rab |
|- ( ph -> A = { y e. RR | ( ( 1 / C ) x. y ) e. B } ) |
| 14 |
4 2
|
rerpdivcld |
|- ( ph -> ( ( vol* ` A ) / C ) e. RR ) |
| 15 |
|
ovollecl |
|- ( ( B C_ RR /\ ( ( vol* ` A ) / C ) e. RR /\ ( vol* ` B ) <_ ( ( vol* ` A ) / C ) ) -> ( vol* ` B ) e. RR ) |
| 16 |
11 14 5 15
|
syl3anc |
|- ( ph -> ( vol* ` B ) e. RR ) |
| 17 |
11 12 13 16
|
ovolscalem2 |
|- ( ph -> ( vol* ` A ) <_ ( ( vol* ` B ) / ( 1 / C ) ) ) |
| 18 |
4 16 12
|
lemuldivd |
|- ( ph -> ( ( ( vol* ` A ) x. ( 1 / C ) ) <_ ( vol* ` B ) <-> ( vol* ` A ) <_ ( ( vol* ` B ) / ( 1 / C ) ) ) ) |
| 19 |
17 18
|
mpbird |
|- ( ph -> ( ( vol* ` A ) x. ( 1 / C ) ) <_ ( vol* ` B ) ) |
| 20 |
9 19
|
eqbrtrd |
|- ( ph -> ( ( vol* ` A ) / C ) <_ ( vol* ` B ) ) |
| 21 |
16 14
|
letri3d |
|- ( ph -> ( ( vol* ` B ) = ( ( vol* ` A ) / C ) <-> ( ( vol* ` B ) <_ ( ( vol* ` A ) / C ) /\ ( ( vol* ` A ) / C ) <_ ( vol* ` B ) ) ) ) |
| 22 |
5 20 21
|
mpbir2and |
|- ( ph -> ( vol* ` B ) = ( ( vol* ` A ) / C ) ) |