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 ) )