Metamath Proof Explorer

Theorem ovolscalem2

Description: Lemma for ovolshft . (Contributed by Mario Carneiro, 22-Mar-2014)

Ref Expression
Hypotheses ovolsca.1 
|- ( ph -> A C_ RR )
ovolsca.2 
|- ( ph -> C e. RR+ )
ovolsca.3 
|- ( ph -> B = { x e. RR | ( C x. x ) e. A } )
ovolsca.4 
|- ( ph -> ( vol* ` A ) e. RR )
Assertion ovolscalem2 
|- ( ph -> ( vol* ` B ) <_ ( ( vol* ` A ) / C ) )

Proof

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 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> A C_ RR )
6 4 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> ( vol* ` A ) e. RR )
7 rpmulcl 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> ( C x. y ) e. RR+ )
8 2 7 sylan 
 |-  ( ( ph /\ y e. RR+ ) -> ( C x. y ) e. RR+ )
9 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
10 9 ovolgelb 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ ( C x. y ) e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) )
11 5 6 8 10 syl3anc 
 |-  ( ( ph /\ y e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) )
12 1 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> A C_ RR )
13 2 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> C e. RR+ )
14 3 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> B = { x e. RR | ( C x. x ) e. A } )
15 4 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> ( vol* ` A ) e. RR )
16 2fveq3 
 |-  ( m = n -> ( 1st ` ( f ` m ) ) = ( 1st ` ( f ` n ) ) )
17 16 oveq1d 
 |-  ( m = n -> ( ( 1st ` ( f ` m ) ) / C ) = ( ( 1st ` ( f ` n ) ) / C ) )
18 2fveq3 
 |-  ( m = n -> ( 2nd ` ( f ` m ) ) = ( 2nd ` ( f ` n ) ) )
19 18 oveq1d 
 |-  ( m = n -> ( ( 2nd ` ( f ` m ) ) / C ) = ( ( 2nd ` ( f ` n ) ) / C ) )
20 17 19 opeq12d 
 |-  ( m = n -> <. ( ( 1st ` ( f ` m ) ) / C ) , ( ( 2nd ` ( f ` m ) ) / C ) >. = <. ( ( 1st ` ( f ` n ) ) / C ) , ( ( 2nd ` ( f ` n ) ) / C ) >. )
21 20 cbvmptv 
 |-  ( m e. NN |-> <. ( ( 1st ` ( f ` m ) ) / C ) , ( ( 2nd ` ( f ` m ) ) / C ) >. ) = ( n e. NN |-> <. ( ( 1st ` ( f ` n ) ) / C ) , ( ( 2nd ` ( f ` n ) ) / C ) >. )
22 elmapi 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
23 22 ad2antrl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
24 simprrl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> A C_ U. ran ( (,) o. f ) )
25 simplr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> y e. RR+ )
26 simprrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) )
27 12 13 14 15 9 21 23 24 25 26 ovolscalem1 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C x. y ) ) ) ) ) -> ( vol* ` B ) <_ ( ( ( vol* ` A ) / C ) + y ) )
28 11 27 rexlimddv 
 |-  ( ( ph /\ y e. RR+ ) -> ( vol* ` B ) <_ ( ( ( vol* ` A ) / C ) + y ) )
29 28 ralrimiva 
 |-  ( ph -> A. y e. RR+ ( vol* ` B ) <_ ( ( ( vol* ` A ) / C ) + y ) )
30 ssrab2 
 |-  { x e. RR | ( C x. x ) e. A } C_ RR
31 3 30 eqsstrdi 
 |-  ( ph -> B C_ RR )
32 ovolcl 
 |-  ( B C_ RR -> ( vol* ` B ) e. RR* )
33 31 32 syl 
 |-  ( ph -> ( vol* ` B ) e. RR* )
34 4 2 rerpdivcld 
 |-  ( ph -> ( ( vol* ` A ) / C ) e. RR )
35 xralrple 
 |-  ( ( ( vol* ` B ) e. RR* /\ ( ( vol* ` A ) / C ) e. RR ) -> ( ( vol* ` B ) <_ ( ( vol* ` A ) / C ) <-> A. y e. RR+ ( vol* ` B ) <_ ( ( ( vol* ` A ) / C ) + y ) ) )
36 33 34 35 syl2anc 
 |-  ( ph -> ( ( vol* ` B ) <_ ( ( vol* ` A ) / C ) <-> A. y e. RR+ ( vol* ` B ) <_ ( ( ( vol* ` A ) / C ) + y ) ) )
37 29 36 mpbird 
 |-  ( ph -> ( vol* ` B ) <_ ( ( vol* ` A ) / C ) )