Metamath Proof Explorer

Theorem ioombl1lem4

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 16-Jun-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 ioombl1lem4 
|- ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( ( vol* ` E ) + C ) )

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 inss1 
 |-  ( E i^i B ) C_ E
17 ovolsscl 
 |-  ( ( ( E i^i B ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i B ) ) e. RR )
18 16 3 4 17 mp3an2i 
 |-  ( ph -> ( vol* ` ( E i^i B ) ) e. RR )
19 difss 
 |-  ( E \ B ) C_ E
20 ovolsscl 
 |-  ( ( ( E \ B ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ B ) ) e. RR )
21 19 3 4 20 mp3an2i 
 |-  ( ph -> ( vol* ` ( E \ B ) ) e. RR )
22 18 21 readdcld 
 |-  ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) e. RR )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem2 
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR )
24 5 rpred 
 |-  ( ph -> C e. RR )
25 4 24 readdcld 
 |-  ( ph -> ( ( vol* ` E ) + C ) e. RR )
26 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 ) ) ) )
27 26 simpld 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
28 eqid 
 |-  ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
29 28 7 ovolsf 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) )
30 27 29 syl 
 |-  ( ph -> T : NN --> ( 0 [,) +oo ) )
31 30 frnd 
 |-  ( ph -> ran T C_ ( 0 [,) +oo ) )
32 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
33 31 32 sstrdi 
 |-  ( ph -> ran T C_ RR )
34 1nn 
 |-  1 e. NN
35 30 fdmd 
 |-  ( ph -> dom T = NN )
36 34 35 eleqtrrid 
 |-  ( ph -> 1 e. dom T )
37 36 ne0d 
 |-  ( ph -> dom T =/= (/) )
38 dm0rn0 
 |-  ( dom T = (/) <-> ran T = (/) )
39 38 necon3bii 
 |-  ( dom T =/= (/) <-> ran T =/= (/) )
40 37 39 sylib 
 |-  ( ph -> ran T =/= (/) )
41 30 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) e. ( 0 [,) +oo ) )
42 32 41 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) e. RR )
43 eqid 
 |-  ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
44 43 6 ovolsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
45 9 44 syl 
 |-  ( ph -> S : NN --> ( 0 [,) +oo ) )
46 45 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( S ` j ) e. ( 0 [,) +oo ) )
47 32 46 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( S ` j ) e. RR )
48 23 adantr 
 |-  ( ( ph /\ j e. NN ) -> sup ( ran S , RR* , < ) e. RR )
49 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
50 nnuz 
 |-  NN = ( ZZ>= ` 1 )
51 49 50 eleqtrdi 
 |-  ( ( ph /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
52 simpl 
 |-  ( ( ph /\ j e. NN ) -> ph )
53 elfznn 
 |-  ( n e. ( 1 ... j ) -> n e. NN )
54 28 ovolfsf 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
55 27 54 syl 
 |-  ( ph -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
56 55 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) )
57 32 56 sselid 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR )
58 52 53 57 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. RR )
59 43 ovolfsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
60 9 59 syl 
 |-  ( ph -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
61 60 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. ( 0 [,) +oo ) )
62 elrege0 
 |-  ( ( ( ( abs o. - ) o. F ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. F ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) )
63 61 62 sylib 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. F ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` n ) ) )
64 63 simpld 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
65 52 53 64 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
66 26 simprd 
 |-  ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
67 eqid 
 |-  ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
68 67 ovolfsf 
 |-  ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
69 66 68 syl 
 |-  ( ph -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
70 69 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. ( 0 [,) +oo ) )
71 elrege0 
 |-  ( ( ( ( abs o. - ) o. H ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. H ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) )
72 70 71 sylib 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. H ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` n ) ) )
73 72 simprd 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` n ) )
74 72 simpld 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR )
75 57 74 addge01d 
 |-  ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( ( abs o. - ) o. H ) ` n ) <-> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) )
76 73 75 mpbid 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
77 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem3 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) = ( ( ( abs o. - ) o. F ) ` n ) )
78 76 77 breqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
79 52 53 78 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
80 51 58 65 79 serle 
 |-  ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) )
81 7 fveq1i 
 |-  ( T ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j )
82 6 fveq1i 
 |-  ( S ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j )
83 80 81 82 3brtr4g 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) <_ ( S ` j ) )
84 1zzd 
 |-  ( ph -> 1 e. ZZ )
85 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( abs o. - ) o. F ) ` n ) )
86 63 simprd 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) )
87 45 frnd 
 |-  ( ph -> ran S C_ ( 0 [,) +oo ) )
88 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
89 87 88 sstrdi 
 |-  ( ph -> ran S C_ RR* )
90 89 adantr 
 |-  ( ( ph /\ k e. NN ) -> ran S C_ RR* )
91 45 ffnd 
 |-  ( ph -> S Fn NN )
92 fnfvelrn 
 |-  ( ( S Fn NN /\ k e. NN ) -> ( S ` k ) e. ran S )
93 91 92 sylan 
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) e. ran S )
94 supxrub 
 |-  ( ( ran S C_ RR* /\ ( S ` k ) e. ran S ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) )
95 90 93 94 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) <_ sup ( ran S , RR* , < ) )
96 95 ralrimiva 
 |-  ( ph -> A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) )
97 brralrspcev 
 |-  ( ( sup ( ran S , RR* , < ) e. RR /\ A. k e. NN ( S ` k ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. k e. NN ( S ` k ) <_ x )
98 23 96 97 syl2anc 
 |-  ( ph -> E. x e. RR A. k e. NN ( S ` k ) <_ x )
99 50 6 84 85 64 86 98 isumsup2 
 |-  ( ph -> S ~~> sup ( ran S , RR , < ) )
100 87 32 sstrdi 
 |-  ( ph -> ran S C_ RR )
101 45 fdmd 
 |-  ( ph -> dom S = NN )
102 34 101 eleqtrrid 
 |-  ( ph -> 1 e. dom S )
103 102 ne0d 
 |-  ( ph -> dom S =/= (/) )
104 dm0rn0 
 |-  ( dom S = (/) <-> ran S = (/) )
105 104 necon3bii 
 |-  ( dom S =/= (/) <-> ran S =/= (/) )
106 103 105 sylib 
 |-  ( ph -> ran S =/= (/) )
107 breq1 
 |-  ( z = ( S ` k ) -> ( z <_ x <-> ( S ` k ) <_ x ) )
108 107 ralrn 
 |-  ( S Fn NN -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
109 91 108 syl 
 |-  ( ph -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
110 109 rexbidv 
 |-  ( ph -> ( E. x e. RR A. z e. ran S z <_ x <-> E. x e. RR A. k e. NN ( S ` k ) <_ x ) )
111 98 110 mpbird 
 |-  ( ph -> E. x e. RR A. z e. ran S z <_ x )
112 supxrre 
 |-  ( ( ran S C_ RR /\ ran S =/= (/) /\ E. x e. RR A. z e. ran S z <_ x ) -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
113 100 106 111 112 syl3anc 
 |-  ( ph -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
114 99 113 breqtrrd 
 |-  ( ph -> S ~~> sup ( ran S , RR* , < ) )
115 114 adantr 
 |-  ( ( ph /\ j e. NN ) -> S ~~> sup ( ran S , RR* , < ) )
116 6 115 eqbrtrrid 
 |-  ( ( ph /\ j e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. F ) ) ~~> sup ( ran S , RR* , < ) )
117 64 adantlr 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) e. RR )
118 86 adantlr 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` n ) )
119 50 49 116 117 118 climserle 
 |-  ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) <_ sup ( ran S , RR* , < ) )
120 82 119 eqbrtrid 
 |-  ( ( ph /\ j e. NN ) -> ( S ` j ) <_ sup ( ran S , RR* , < ) )
121 42 47 48 83 120 letrd 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) <_ sup ( ran S , RR* , < ) )
122 121 ralrimiva 
 |-  ( ph -> A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) )
123 brralrspcev 
 |-  ( ( sup ( ran S , RR* , < ) e. RR /\ A. j e. NN ( T ` j ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. j e. NN ( T ` j ) <_ x )
124 23 122 123 syl2anc 
 |-  ( ph -> E. x e. RR A. j e. NN ( T ` j ) <_ x )
125 30 ffnd 
 |-  ( ph -> T Fn NN )
126 breq1 
 |-  ( z = ( T ` j ) -> ( z <_ x <-> ( T ` j ) <_ x ) )
127 126 ralrn 
 |-  ( T Fn NN -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) )
128 125 127 syl 
 |-  ( ph -> ( A. z e. ran T z <_ x <-> A. j e. NN ( T ` j ) <_ x ) )
129 128 rexbidv 
 |-  ( ph -> ( E. x e. RR A. z e. ran T z <_ x <-> E. x e. RR A. j e. NN ( T ` j ) <_ x ) )
130 124 129 mpbird 
 |-  ( ph -> E. x e. RR A. z e. ran T z <_ x )
131 33 40 130 suprcld 
 |-  ( ph -> sup ( ran T , RR , < ) e. RR )
132 67 8 ovolsf 
 |-  ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) )
133 66 132 syl 
 |-  ( ph -> U : NN --> ( 0 [,) +oo ) )
134 133 frnd 
 |-  ( ph -> ran U C_ ( 0 [,) +oo ) )
135 134 32 sstrdi 
 |-  ( ph -> ran U C_ RR )
136 133 fdmd 
 |-  ( ph -> dom U = NN )
137 34 136 eleqtrrid 
 |-  ( ph -> 1 e. dom U )
138 137 ne0d 
 |-  ( ph -> dom U =/= (/) )
139 dm0rn0 
 |-  ( dom U = (/) <-> ran U = (/) )
140 139 necon3bii 
 |-  ( dom U =/= (/) <-> ran U =/= (/) )
141 138 140 sylib 
 |-  ( ph -> ran U =/= (/) )
142 133 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( U ` j ) e. ( 0 [,) +oo ) )
143 32 142 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( U ` j ) e. RR )
144 52 53 74 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. RR )
145 elrege0 
 |-  ( ( ( ( abs o. - ) o. G ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) )
146 56 145 sylib 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` n ) ) )
147 146 simprd 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. G ) ` n ) )
148 74 57 addge02d 
 |-  ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( ( abs o. - ) o. G ) ` n ) <-> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) ) )
149 147 148 mpbid 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
150 149 77 breqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
151 52 53 150 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) <_ ( ( ( abs o. - ) o. F ) ` n ) )
152 51 144 65 151 serle 
 |-  ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) <_ ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) )
153 8 fveq1i 
 |-  ( U ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j )
154 152 153 82 3brtr4g 
 |-  ( ( ph /\ j e. NN ) -> ( U ` j ) <_ ( S ` j ) )
155 143 47 48 154 120 letrd 
 |-  ( ( ph /\ j e. NN ) -> ( U ` j ) <_ sup ( ran S , RR* , < ) )
156 155 ralrimiva 
 |-  ( ph -> A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) )
157 brralrspcev 
 |-  ( ( sup ( ran S , RR* , < ) e. RR /\ A. j e. NN ( U ` j ) <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. j e. NN ( U ` j ) <_ x )
158 23 156 157 syl2anc 
 |-  ( ph -> E. x e. RR A. j e. NN ( U ` j ) <_ x )
159 133 ffnd 
 |-  ( ph -> U Fn NN )
160 breq1 
 |-  ( z = ( U ` j ) -> ( z <_ x <-> ( U ` j ) <_ x ) )
161 160 ralrn 
 |-  ( U Fn NN -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) )
162 159 161 syl 
 |-  ( ph -> ( A. z e. ran U z <_ x <-> A. j e. NN ( U ` j ) <_ x ) )
163 162 rexbidv 
 |-  ( ph -> ( E. x e. RR A. z e. ran U z <_ x <-> E. x e. RR A. j e. NN ( U ` j ) <_ x ) )
164 158 163 mpbird 
 |-  ( ph -> E. x e. RR A. z e. ran U z <_ x )
165 135 141 164 suprcld 
 |-  ( ph -> sup ( ran U , RR , < ) e. RR )
166 ssralv 
 |-  ( ( E i^i B ) C_ E -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
167 16 166 ax-mp 
 |-  ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) )
168 12 breq1i 
 |-  ( P < x <-> ( 1st ` ( F ` n ) ) < x )
169 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 ) ) ) )
170 9 169 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
171 170 simp1d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR )
172 12 171 eqeltrid 
 |-  ( ( ph /\ n e. NN ) -> P e. RR )
173 172 adantlr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> P e. RR )
174 16 3 sstrid 
 |-  ( ph -> ( E i^i B ) C_ RR )
175 174 sselda 
 |-  ( ( ph /\ x e. ( E i^i B ) ) -> x e. RR )
176 175 adantr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> x e. RR )
177 ltle 
 |-  ( ( P e. RR /\ x e. RR ) -> ( P < x -> P <_ x ) )
178 173 176 177 syl2anc 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) )
179 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
180 opex 
 |-  <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. e. _V
181 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 >. )
182 179 180 181 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) = <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. )
183 182 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( 1st ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
184 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. RR )
185 184 172 ifcld 
 |-  ( ( ph /\ n e. NN ) -> if ( P <_ A , A , P ) e. RR )
186 170 simp2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR )
187 13 186 eqeltrid 
 |-  ( ( ph /\ n e. NN ) -> Q e. RR )
188 185 187 ifcld 
 |-  ( ( ph /\ n e. NN ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
189 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 ) )
190 188 187 189 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 ) )
191 183 190 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
192 191 ad2ant2r 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( 1st ` ( G ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
193 188 ad2ant2r 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) e. RR )
194 185 ad2ant2r 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) e. RR )
195 174 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( E i^i B ) C_ RR )
196 simplr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. ( E i^i B ) )
197 195 196 sseldd 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. RR )
198 187 ad2ant2r 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> Q e. RR )
199 min1 
 |-  ( ( if ( P <_ A , A , P ) e. RR /\ Q e. RR ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ if ( P <_ A , A , P ) )
200 194 198 199 syl2anc 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ if ( P <_ A , A , P ) )
201 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A e. RR )
202 elinel2 
 |-  ( x e. ( E i^i B ) -> x e. B )
203 202 ad2antlr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> x e. B )
204 2 rexrd 
 |-  ( ph -> A e. RR* )
205 pnfxr 
 |-  +oo e. RR*
206 elioo2 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
207 204 205 206 sylancl 
 |-  ( ph -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
208 1 eleq2i 
 |-  ( x e. B <-> x e. ( A (,) +oo ) )
209 ltpnf 
 |-  ( x e. RR -> x < +oo )
210 209 adantr 
 |-  ( ( x e. RR /\ A < x ) -> x < +oo )
211 210 pm4.71i 
 |-  ( ( x e. RR /\ A < x ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) )
212 df-3an 
 |-  ( ( x e. RR /\ A < x /\ x < +oo ) <-> ( ( x e. RR /\ A < x ) /\ x < +oo ) )
213 211 212 bitr4i 
 |-  ( ( x e. RR /\ A < x ) <-> ( x e. RR /\ A < x /\ x < +oo ) )
214 207 208 213 3bitr4g 
 |-  ( ph -> ( x e. B <-> ( x e. RR /\ A < x ) ) )
215 simpr 
 |-  ( ( x e. RR /\ A < x ) -> A < x )
216 214 215 biimtrdi 
 |-  ( ph -> ( x e. B -> A < x ) )
217 216 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( x e. B -> A < x ) )
218 203 217 mpd 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A < x )
219 201 197 218 ltled 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> A <_ x )
220 simprr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> P <_ x )
221 breq1 
 |-  ( A = if ( P <_ A , A , P ) -> ( A <_ x <-> if ( P <_ A , A , P ) <_ x ) )
222 breq1 
 |-  ( P = if ( P <_ A , A , P ) -> ( P <_ x <-> if ( P <_ A , A , P ) <_ x ) )
223 221 222 ifboth 
 |-  ( ( A <_ x /\ P <_ x ) -> if ( P <_ A , A , P ) <_ x )
224 219 220 223 syl2anc 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( P <_ A , A , P ) <_ x )
225 193 194 197 200 224 letrd 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) <_ x )
226 192 225 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ ( n e. NN /\ P <_ x ) ) -> ( 1st ` ( G ` n ) ) <_ x )
227 226 expr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P <_ x -> ( 1st ` ( G ` n ) ) <_ x ) )
228 178 227 syld 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( P < x -> ( 1st ` ( G ` n ) ) <_ x ) )
229 168 228 biimtrrid 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( G ` n ) ) <_ x ) )
230 13 breq2i 
 |-  ( x < Q <-> x < ( 2nd ` ( F ` n ) ) )
231 187 adantlr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> Q e. RR )
232 ltle 
 |-  ( ( x e. RR /\ Q e. RR ) -> ( x < Q -> x <_ Q ) )
233 176 231 232 syl2anc 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) )
234 230 233 biimtrrid 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ Q ) )
235 182 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) )
236 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 )
237 188 187 236 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` <. if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) , Q >. ) = Q )
238 235 237 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q )
239 238 adantlr 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = Q )
240 239 breq2d 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x <_ ( 2nd ` ( G ` n ) ) <-> x <_ Q ) )
241 234 240 sylibrd 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( G ` n ) ) ) )
242 229 241 anim12d 
 |-  ( ( ( ph /\ x e. ( E i^i B ) ) /\ n e. NN ) -> ( ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
243 242 reximdva 
 |-  ( ( ph /\ x e. ( E i^i B ) ) -> ( E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
244 243 ralimdva 
 |-  ( ph -> ( A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
245 167 244 syl5 
 |-  ( ph -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
246 ovolfioo 
 |-  ( ( E C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( E C_ U. ran ( (,) o. F ) <-> A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
247 3 9 246 syl2anc 
 |-  ( ph -> ( E C_ U. ran ( (,) o. F ) <-> A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
248 ovolficc 
 |-  ( ( ( E i^i B ) C_ RR /\ G : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( E i^i B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
249 174 27 248 syl2anc 
 |-  ( ph -> ( ( E i^i B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( E i^i B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
250 245 247 249 3imtr4d 
 |-  ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E i^i B ) C_ U. ran ( [,] o. G ) ) )
251 10 250 mpd 
 |-  ( ph -> ( E i^i B ) C_ U. ran ( [,] o. G ) )
252 7 ovollb2 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( E i^i B ) C_ U. ran ( [,] o. G ) ) -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR* , < ) )
253 27 251 252 syl2anc 
 |-  ( ph -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR* , < ) )
254 supxrre 
 |-  ( ( ran T C_ RR /\ ran T =/= (/) /\ E. x e. RR A. z e. ran T z <_ x ) -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
255 33 40 130 254 syl3anc 
 |-  ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
256 253 255 breqtrd 
 |-  ( ph -> ( vol* ` ( E i^i B ) ) <_ sup ( ran T , RR , < ) )
257 ssralv 
 |-  ( ( E \ B ) C_ E -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) )
258 19 257 ax-mp 
 |-  ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) )
259 172 adantlr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> P e. RR )
260 19 3 sstrid 
 |-  ( ph -> ( E \ B ) C_ RR )
261 260 sselda 
 |-  ( ( ph /\ x e. ( E \ B ) ) -> x e. RR )
262 261 adantr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> x e. RR )
263 259 262 177 syl2anc 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( P < x -> P <_ x ) )
264 168 263 biimtrrid 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> P <_ x ) )
265 opex 
 |-  <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. e. _V
266 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 ) >. )
267 179 265 266 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( H ` n ) = <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. )
268 267 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
269 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 )
270 172 188 269 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) = P )
271 268 270 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P )
272 271 adantlr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( 1st ` ( H ` n ) ) = P )
273 272 breq1d 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( H ` n ) ) <_ x <-> P <_ x ) )
274 264 273 sylibrd 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) < x -> ( 1st ` ( H ` n ) ) <_ x ) )
275 187 adantlr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> Q e. RR )
276 262 275 232 syl2anc 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ Q ) )
277 260 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( E \ B ) C_ RR )
278 simplr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. ( E \ B ) )
279 277 278 sseldd 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x e. RR )
280 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A e. RR )
281 172 ad2ant2r 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> P e. RR )
282 280 281 ifcld 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> if ( P <_ A , A , P ) e. RR )
283 eldifn 
 |-  ( x e. ( E \ B ) -> -. x e. B )
284 283 ad2antlr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. x e. B )
285 279 biantrurd 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> ( x e. RR /\ A < x ) ) )
286 214 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( x e. B <-> ( x e. RR /\ A < x ) ) )
287 285 286 bitr4d 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( A < x <-> x e. B ) )
288 284 287 mtbird 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> -. A < x )
289 279 280 288 nltled 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ A )
290 max2 
 |-  ( ( P e. RR /\ A e. RR ) -> A <_ if ( P <_ A , A , P ) )
291 281 280 290 syl2anc 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> A <_ if ( P <_ A , A , P ) )
292 279 280 282 289 291 letrd 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ if ( P <_ A , A , P ) )
293 simprr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ Q )
294 breq2 
 |-  ( if ( P <_ A , A , P ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( x <_ if ( P <_ A , A , P ) <-> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
295 breq2 
 |-  ( Q = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) -> ( x <_ Q <-> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) ) )
296 294 295 ifboth 
 |-  ( ( x <_ if ( P <_ A , A , P ) /\ x <_ Q ) -> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
297 292 293 296 syl2anc 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
298 267 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = ( 2nd ` <. P , if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) >. ) )
299 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 ) )
300 172 188 299 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 ) )
301 298 300 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
302 301 ad2ant2r 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> ( 2nd ` ( H ` n ) ) = if ( if ( P <_ A , A , P ) <_ Q , if ( P <_ A , A , P ) , Q ) )
303 297 302 breqtrrd 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ ( n e. NN /\ x <_ Q ) ) -> x <_ ( 2nd ` ( H ` n ) ) )
304 303 expr 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x <_ Q -> x <_ ( 2nd ` ( H ` n ) ) ) )
305 276 304 syld 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < Q -> x <_ ( 2nd ` ( H ` n ) ) ) )
306 230 305 biimtrrid 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( x < ( 2nd ` ( F ` n ) ) -> x <_ ( 2nd ` ( H ` n ) ) ) )
307 274 306 anim12d 
 |-  ( ( ( ph /\ x e. ( E \ B ) ) /\ n e. NN ) -> ( ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
308 307 reximdva 
 |-  ( ( ph /\ x e. ( E \ B ) ) -> ( E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
309 308 ralimdva 
 |-  ( ph -> ( A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
310 258 309 syl5 
 |-  ( ph -> ( A. x e. E E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) -> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
311 ovolficc 
 |-  ( ( ( E \ B ) C_ RR /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( E \ B ) C_ U. ran ( [,] o. H ) <-> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
312 260 66 311 syl2anc 
 |-  ( ph -> ( ( E \ B ) C_ U. ran ( [,] o. H ) <-> A. x e. ( E \ B ) E. n e. NN ( ( 1st ` ( H ` n ) ) <_ x /\ x <_ ( 2nd ` ( H ` n ) ) ) ) )
313 310 247 312 3imtr4d 
 |-  ( ph -> ( E C_ U. ran ( (,) o. F ) -> ( E \ B ) C_ U. ran ( [,] o. H ) ) )
314 10 313 mpd 
 |-  ( ph -> ( E \ B ) C_ U. ran ( [,] o. H ) )
315 8 ovollb2 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( E \ B ) C_ U. ran ( [,] o. H ) ) -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) )
316 66 314 315 syl2anc 
 |-  ( ph -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR* , < ) )
317 supxrre 
 |-  ( ( ran U C_ RR /\ ran U =/= (/) /\ E. x e. RR A. z e. ran U z <_ x ) -> sup ( ran U , RR* , < ) = sup ( ran U , RR , < ) )
318 135 141 164 317 syl3anc 
 |-  ( ph -> sup ( ran U , RR* , < ) = sup ( ran U , RR , < ) )
319 316 318 breqtrd 
 |-  ( ph -> ( vol* ` ( E \ B ) ) <_ sup ( ran U , RR , < ) )
320 18 21 131 165 256 319 le2addd 
 |-  ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) )
321 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( ( abs o. - ) o. G ) ` n ) )
322 50 7 84 321 57 147 124 isumsup2 
 |-  ( ph -> T ~~> sup ( ran T , RR , < ) )
323 seqex 
 |-  seq 1 ( + , ( ( abs o. - ) o. F ) ) e. _V
324 6 323 eqeltri 
 |-  S e. _V
325 324 a1i 
 |-  ( ph -> S e. _V )
326 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) = ( ( ( abs o. - ) o. H ) ` n ) )
327 50 8 84 326 74 73 158 isumsup2 
 |-  ( ph -> U ~~> sup ( ran U , RR , < ) )
328 42 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) e. CC )
329 143 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( U ` j ) e. CC )
330 57 recnd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC )
331 52 53 330 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. G ) ` n ) e. CC )
332 74 recnd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC )
333 52 53 332 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. H ) ` n ) e. CC )
334 77 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
335 52 53 334 syl2an 
 |-  ( ( ( ph /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( ( ( abs o. - ) o. G ) ` n ) + ( ( ( abs o. - ) o. H ) ` n ) ) )
336 51 331 333 335 seradd 
 |-  ( ( ph /\ j e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` j ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) + ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) ) )
337 81 153 oveq12i 
 |-  ( ( T ` j ) + ( U ` j ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` j ) + ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` j ) )
338 336 82 337 3eqtr4g 
 |-  ( ( ph /\ j e. NN ) -> ( S ` j ) = ( ( T ` j ) + ( U ` j ) ) )
339 50 84 322 325 327 328 329 338 climadd 
 |-  ( ph -> S ~~> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) )
340 climuni 
 |-  ( ( S ~~> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) /\ S ~~> sup ( ran S , RR* , < ) ) -> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) = sup ( ran S , RR* , < ) )
341 339 114 340 syl2anc 
 |-  ( ph -> ( sup ( ran T , RR , < ) + sup ( ran U , RR , < ) ) = sup ( ran S , RR* , < ) )
342 320 341 breqtrd 
 |-  ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ sup ( ran S , RR* , < ) )
343 22 23 25 342 11 letrd 
 |-  ( ph -> ( ( vol* ` ( E i^i B ) ) + ( vol* ` ( E \ B ) ) ) <_ ( ( vol* ` E ) + C ) )