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