Metamath Proof Explorer

Theorem ioombl1lem3

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 ioombl1lem3 
|- ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) = ( ( ( abs o. - ) o. F ) ` n ) )

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 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 ) ) ) )
17 9 16 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
18 17 simp2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR )
19 13 18 eqeltrid 
 |-  ( ( ph /\ n e. NN ) -> Q e. RR )
20 19 recnd 
 |-  ( ( ph /\ n e. NN ) -> Q e. CC )
21 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. RR )
22 17 simp1d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR )
23 12 22 eqeltrid 
 |-  ( ( ph /\ n e. NN ) -> P e. RR )
24 21 23 ifcld 
 |-  ( ( ph /\ n e. NN ) -> if ( P <_ A , A , P ) e. RR )
25 24 19 ifcld 
 |-  ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
26 25 recnd 
 |-  ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. CC )
27 23 recnd 
 |-  ( ( ph /\ n e. NN ) -> P e. CC )
28 20 26 27 npncand 
 |-  ( ( ph /\ n e. NN ) -> ( ( Q - if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) + ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) - P ) ) = ( Q - P ) )
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem1 
 |-  ( ph -> ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) )
30 29 simpld 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
31 eqid 
 |-  ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
32 31 ovolfsval 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) )
33 30 32 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) )
34 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
35 opex 
 |-  <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V
36 14 fvmpt2 
 |-  ( ( n e. NN /\ <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
37 34 35 36 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
38 37 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
39 op2ndg 
 |-  ( ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR /\ Q e. RR ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q )
40 25 19 39 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q )
41 38 40 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q )
42 37 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
43 op1stg 
 |-  ( ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR /\ Q e. RR ) -> ( 1st ` <. 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 ) )
44 25 19 43 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` <. 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 ) )
45 42 44 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
46 41 45 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) = ( Q - if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
47 33 46 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( Q - if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
48 29 simprd 
 |-  ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
49 eqid 
 |-  ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
50 49 ovolfsval 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) = ( ( 2nd ` ( H ` n ) ) - ( 1st ` ( H ` n ) ) ) )
51 48 50 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) = ( ( 2nd ` ( H ` n ) ) - ( 1st ` ( H ` n ) ) ) )
52 opex 
 |-  <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V
53 15 fvmpt2 
 |-  ( ( n e. NN /\ <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
54 34 52 53 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
55 54 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
56 op2ndg 
 |-  ( ( P e. RR /\ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) -> ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
57 23 25 56 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
58 55 57 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
59 54 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
60 op1stg 
 |-  ( ( P e. RR /\ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P )
61 23 25 60 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P )
62 59 61 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P )
63 58 62 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( H ` n ) ) - ( 1st ` ( H ` n ) ) ) = ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) - P ) )
64 51 63 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) = ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) - P ) )
65 47 64 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) = ( ( Q - if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) + ( if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) - P ) ) )
66 eqid 
 |-  ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
67 66 ovolfsval 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) )
68 9 67 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) )
69 13 12 oveq12i 
 |-  ( Q - P ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) )
70 68 69 eqtr4di 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( Q - P ) )
71 28 65 70 3eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) = ( ( ( abs o. - ) o. F ) ` n ) )