Metamath Proof Explorer

Theorem ioombl1lem1

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses ioombl1.b 
|- B = ( A (,) +oo )
ioombl1.a 
|- ( ph -> A e. RR )
ioombl1.e 
|- ( ph -> E C_ RR )
ioombl1.v 
|- ( ph -> ( vol* ` E ) e. RR )
ioombl1.c 
|- ( ph -> C e. RR+ )
ioombl1.s 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ioombl1.t 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
ioombl1.u 
|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ioombl1.f1 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ioombl1.f2 
|- ( ph -> E C_ U. ran ( (,) o. F ) )
ioombl1.f3 
|- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) )
ioombl1.p 
|- P = ( 1st ` ( F ` n ) )
ioombl1.q 
|- Q = ( 2nd ` ( F ` n ) )
ioombl1.g 
|- G = ( n e. NN |-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
ioombl1.h 
|- H = ( n e. NN |-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
Assertion ioombl1lem1 
|- ( ph -> ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) )

Proof

Step Hyp Ref Expression
1 ioombl1.b 
 |-  B = ( A (,) +oo )
2 ioombl1.a 
 |-  ( ph -> A e. RR )
3 ioombl1.e 
 |-  ( ph -> E C_ RR )
4 ioombl1.v 
 |-  ( ph -> ( vol* ` E ) e. RR )
5 ioombl1.c 
 |-  ( ph -> C e. RR+ )
6 ioombl1.s 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
7 ioombl1.t 
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
8 ioombl1.u 
 |-  U = seq 1 ( + , ( ( abs o. - ) o. H ) )
9 ioombl1.f1 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
10 ioombl1.f2 
 |-  ( ph -> E C_ U. ran ( (,) o. F ) )
11 ioombl1.f3 
 |-  ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` E ) + C ) )
12 ioombl1.p 
 |-  P = ( 1st ` ( F ` n ) )
13 ioombl1.q 
 |-  Q = ( 2nd ` ( F ` n ) )
14 ioombl1.g 
 |-  G = ( n e. NN |-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
15 ioombl1.h 
 |-  H = ( n e. NN |-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
16 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. RR )
17 ovolfcl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
18 9 17 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
19 18 simp1d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR )
20 12 19 eqeltrid 
 |-  ( ( ph /\ n e. NN ) -> P e. RR )
21 16 20 ifcld 
 |-  ( ( ph /\ n e. NN ) -> if ( P <_ A , A , P ) e. RR )
22 18 simp2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR )
23 13 22 eqeltrid 
 |-  ( ( ph /\ n e. NN ) -> Q e. RR )
24 min2 
 |-  ( ( if ( P <_ A , A , P ) e. RR /\ Q e. RR ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ Q )
25 21 23 24 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ Q )
26 df-br 
 |-  ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ Q <-> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. <_ )
27 25 26 sylib 
 |-  ( ( ph /\ n e. NN ) -> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. <_ )
28 21 23 ifcld 
 |-  ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
29 28 23 opelxpd 
 |-  ( ( ph /\ n e. NN ) -> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. ( RR X. RR ) )
30 27 29 elind 
 |-  ( ( ph /\ n e. NN ) -> <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. ( <_ i^i ( RR X. RR ) ) )
31 30 14 fmptd 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
32 max1 
 |-  ( ( P e. RR /\ A e. RR ) -> P <_ if ( P <_ A , A , P ) )
33 20 16 32 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> P <_ if ( P <_ A , A , P ) )
34 18 simp3d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) )
35 34 12 13 3brtr4g 
 |-  ( ( ph /\ n e. NN ) -> P <_ Q )
36 breq2 
 |-  ( if ( P <_ A , A , P ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( P <_ if ( P <_ A , A , P ) <-> P <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
37 breq2 
 |-  ( Q = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( P <_ Q <-> P <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
38 36 37 ifboth 
 |-  ( ( P <_ if ( P <_ A , A , P ) /\ P <_ Q ) -> P <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
39 33 35 38 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> P <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
40 df-br 
 |-  ( P <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <-> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. <_ )
41 39 40 sylib 
 |-  ( ( ph /\ n e. NN ) -> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. <_ )
42 20 28 opelxpd 
 |-  ( ( ph /\ n e. NN ) -> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. ( RR X. RR ) )
43 41 42 elind 
 |-  ( ( ph /\ n e. NN ) -> <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. ( <_ i^i ( RR X. RR ) ) )
44 43 15 fmptd 
 |-  ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
45 31 44 jca 
 |-  ( ph -> ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) )