Metamath Proof Explorer

Theorem ovolunlem2

Description: Lemma for ovolun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovolun.a 
|- ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
ovolun.b 
|- ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
ovolun.c 
|- ( ph -> C e. RR+ )
Assertion ovolunlem2 
|- ( ph -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )

Proof

Step Hyp Ref Expression
1 ovolun.a 
 |-  ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
2 ovolun.b 
 |-  ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
3 ovolun.c 
 |-  ( ph -> C e. RR+ )
4 1 simpld 
 |-  ( ph -> A C_ RR )
5 1 simprd 
 |-  ( ph -> ( vol* ` A ) e. RR )
6 3 rphalfcld 
 |-  ( ph -> ( C / 2 ) e. RR+ )
7 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. g ) ) = seq 1 ( + , ( ( abs o. - ) o. g ) )
8 7 ovolgelb 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ ( C / 2 ) e. RR+ ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) )
9 4 5 6 8 syl3anc 
 |-  ( ph -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) )
10 2 simpld 
 |-  ( ph -> B C_ RR )
11 2 simprd 
 |-  ( ph -> ( vol* ` B ) e. RR )
12 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. h ) ) = seq 1 ( + , ( ( abs o. - ) o. h ) )
13 12 ovolgelb 
 |-  ( ( B C_ RR /\ ( vol* ` B ) e. RR /\ ( C / 2 ) e. RR+ ) -> E. h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) )
14 10 11 6 13 syl3anc 
 |-  ( ph -> E. h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) )
15 reeanv 
 |-  ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) E. h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) <-> ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ E. h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) )
16 1 3ad2ant1 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
17 2 3ad2ant1 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
18 3 3ad2ant1 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> C e. RR+ )
19 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. ( n e. NN |-> if ( ( n / 2 ) e. NN , ( h ` ( n / 2 ) ) , ( g ` ( ( n + 1 ) / 2 ) ) ) ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( n e. NN |-> if ( ( n / 2 ) e. NN , ( h ` ( n / 2 ) ) , ( g ` ( ( n + 1 ) / 2 ) ) ) ) ) )
20 simp2l 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
21 simp3ll 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> A C_ U. ran ( (,) o. g ) )
22 simp3lr 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
23 simp2r 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
24 simp3rl 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> B C_ U. ran ( (,) o. h ) )
25 simp3rr 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
26 eqid 
 |-  ( n e. NN |-> if ( ( n / 2 ) e. NN , ( h ` ( n / 2 ) ) , ( g ` ( ( n + 1 ) / 2 ) ) ) ) = ( n e. NN |-> if ( ( n / 2 ) e. NN , ( h ` ( n / 2 ) ) , ( g ` ( ( n + 1 ) / 2 ) ) ) )
27 16 17 18 7 12 19 20 21 22 23 24 25 26 ovolunlem1 
 |-  ( ( ph /\ ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) /\ ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
28 27 3exp 
 |-  ( ph -> ( ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) ) )
29 28 rexlimdvv 
 |-  ( ph -> ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) E. h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) )
30 15 29 syl5bir 
 |-  ( ph -> ( ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) /\ E. h e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. h ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. h ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) )
31 9 14 30 mp2and 
 |-  ( ph -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )