Metamath Proof Explorer

Theorem ovolunlem1

Description: Lemma for ovolun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovolun.a 
|- ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
ovolun.b 
|- ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
ovolun.c 
|- ( ph -> C e. RR+ )
ovolun.s 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolun.t 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
ovolun.u 
|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ovolun.f1 
|- ( ph -> F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovolun.f2 
|- ( ph -> A C_ U. ran ( (,) o. F ) )
ovolun.f3 
|- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
ovolun.g1 
|- ( ph -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovolun.g2 
|- ( ph -> B C_ U. ran ( (,) o. G ) )
ovolun.g3 
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
ovolun.h 
|- H = ( n e. NN |-> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) )
Assertion ovolunlem1 
|- ( ph -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )

Proof

Step Hyp Ref Expression
1 ovolun.a 
 |-  ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
2 ovolun.b 
 |-  ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
3 ovolun.c 
 |-  ( ph -> C e. RR+ )
4 ovolun.s 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
5 ovolun.t 
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
6 ovolun.u 
 |-  U = seq 1 ( + , ( ( abs o. - ) o. H ) )
7 ovolun.f1 
 |-  ( ph -> F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
8 ovolun.f2 
 |-  ( ph -> A C_ U. ran ( (,) o. F ) )
9 ovolun.f3 
 |-  ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
10 ovolun.g1 
 |-  ( ph -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
11 ovolun.g2 
 |-  ( ph -> B C_ U. ran ( (,) o. G ) )
12 ovolun.g3 
 |-  ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
13 ovolun.h 
 |-  H = ( n e. NN |-> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) )
14 1 simpld 
 |-  ( ph -> A C_ RR )
15 2 simpld 
 |-  ( ph -> B C_ RR )
16 14 15 unssd 
 |-  ( ph -> ( A u. B ) C_ RR )
17 elovolmlem 
 |-  ( G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> G : NN --> ( <_ i^i ( RR X. RR ) ) )
18 10 17 sylib 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
19 18 adantr 
 |-  ( ( ph /\ n e. NN ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
20 19 ffvelcdmda 
 |-  ( ( ( ph /\ n e. NN ) /\ ( n / 2 ) e. NN ) -> ( G ` ( n / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
21 nneo 
 |-  ( n e. NN -> ( ( n / 2 ) e. NN <-> -. ( ( n + 1 ) / 2 ) e. NN ) )
22 21 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( n / 2 ) e. NN <-> -. ( ( n + 1 ) / 2 ) e. NN ) )
23 22 con2bid 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( n + 1 ) / 2 ) e. NN <-> -. ( n / 2 ) e. NN ) )
24 23 biimpar 
 |-  ( ( ( ph /\ n e. NN ) /\ -. ( n / 2 ) e. NN ) -> ( ( n + 1 ) / 2 ) e. NN )
25 elovolmlem 
 |-  ( F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> F : NN --> ( <_ i^i ( RR X. RR ) ) )
26 7 25 sylib 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
27 26 adantr 
 |-  ( ( ph /\ n e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
28 27 ffvelcdmda 
 |-  ( ( ( ph /\ n e. NN ) /\ ( ( n + 1 ) / 2 ) e. NN ) -> ( F ` ( ( n + 1 ) / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
29 24 28 syldan 
 |-  ( ( ( ph /\ n e. NN ) /\ -. ( n / 2 ) e. NN ) -> ( F ` ( ( n + 1 ) / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
30 20 29 ifclda 
 |-  ( ( ph /\ n e. NN ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) e. ( <_ i^i ( RR X. RR ) ) )
31 30 13 fmptd 
 |-  ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
32 eqid 
 |-  ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
33 32 6 ovolsf 
 |-  ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) )
34 31 33 syl 
 |-  ( ph -> U : NN --> ( 0 [,) +oo ) )
35 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
36 fss 
 |-  ( ( U : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> U : NN --> RR )
37 34 35 36 sylancl 
 |-  ( ph -> U : NN --> RR )
38 37 frnd 
 |-  ( ph -> ran U C_ RR )
39 1nn 
 |-  1 e. NN
40 1z 
 |-  1 e. ZZ
41 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( ( abs o. - ) o. H ) ) Fn ( ZZ>= ` 1 ) )
42 40 41 mp1i 
 |-  ( ph -> seq 1 ( + , ( ( abs o. - ) o. H ) ) Fn ( ZZ>= ` 1 ) )
43 6 fneq1i 
 |-  ( U Fn NN <-> seq 1 ( + , ( ( abs o. - ) o. H ) ) Fn NN )
44 nnuz 
 |-  NN = ( ZZ>= ` 1 )
45 44 fneq2i 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. H ) ) Fn NN <-> seq 1 ( + , ( ( abs o. - ) o. H ) ) Fn ( ZZ>= ` 1 ) )
46 43 45 bitri 
 |-  ( U Fn NN <-> seq 1 ( + , ( ( abs o. - ) o. H ) ) Fn ( ZZ>= ` 1 ) )
47 42 46 sylibr 
 |-  ( ph -> U Fn NN )
48 47 fndmd 
 |-  ( ph -> dom U = NN )
49 39 48 eleqtrrid 
 |-  ( ph -> 1 e. dom U )
50 49 ne0d 
 |-  ( ph -> dom U =/= (/) )
51 dm0rn0 
 |-  ( dom U = (/) <-> ran U = (/) )
52 51 necon3bii 
 |-  ( dom U =/= (/) <-> ran U =/= (/) )
53 50 52 sylib 
 |-  ( ph -> ran U =/= (/) )
54 1 simprd 
 |-  ( ph -> ( vol* ` A ) e. RR )
55 2 simprd 
 |-  ( ph -> ( vol* ` B ) e. RR )
56 54 55 readdcld 
 |-  ( ph -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
57 3 rpred 
 |-  ( ph -> C e. RR )
58 56 57 readdcld 
 |-  ( ph -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 ovolunlem1a 
 |-  ( ( ph /\ k e. NN ) -> ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
60 59 ralrimiva 
 |-  ( ph -> A. k e. NN ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
61 breq1 
 |-  ( z = ( U ` k ) -> ( z <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) <-> ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) )
62 61 ralrn 
 |-  ( U Fn NN -> ( A. z e. ran U z <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) <-> A. k e. NN ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) )
63 47 62 syl 
 |-  ( ph -> ( A. z e. ran U z <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) <-> A. k e. NN ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) )
64 60 63 mpbird 
 |-  ( ph -> A. z e. ran U z <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
65 brralrspcev 
 |-  ( ( ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR /\ A. z e. ran U z <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) -> E. k e. RR A. z e. ran U z <_ k )
66 58 64 65 syl2anc 
 |-  ( ph -> E. k e. RR A. z e. ran U z <_ k )
67 ressxr 
 |-  RR C_ RR*
68 38 67 sstrdi 
 |-  ( ph -> ran U C_ RR* )
69 supxrbnd2 
 |-  ( ran U C_ RR* -> ( E. k e. RR A. z e. ran U z <_ k <-> sup ( ran U , RR* , < ) < +oo ) )
70 68 69 syl 
 |-  ( ph -> ( E. k e. RR A. z e. ran U z <_ k <-> sup ( ran U , RR* , < ) < +oo ) )
71 66 70 mpbid 
 |-  ( ph -> sup ( ran U , RR* , < ) < +oo )
72 supxrbnd 
 |-  ( ( ran U C_ RR /\ ran U =/= (/) /\ sup ( ran U , RR* , < ) < +oo ) -> sup ( ran U , RR* , < ) e. RR )
73 38 53 71 72 syl3anc 
 |-  ( ph -> sup ( ran U , RR* , < ) e. RR )
74 nncn 
 |-  ( m e. NN -> m e. CC )
75 74 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
76 1cnd 
 |-  ( ( ph /\ m e. NN ) -> 1 e. CC )
77 75 2timesd 
 |-  ( ( ph /\ m e. NN ) -> ( 2 x. m ) = ( m + m ) )
78 77 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( 2 x. m ) - 1 ) = ( ( m + m ) - 1 ) )
79 75 75 76 78 assraddsubd 
 |-  ( ( ph /\ m e. NN ) -> ( ( 2 x. m ) - 1 ) = ( m + ( m - 1 ) ) )
80 simpr 
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
81 nnm1nn0 
 |-  ( m e. NN -> ( m - 1 ) e. NN0 )
82 nnnn0addcl 
 |-  ( ( m e. NN /\ ( m - 1 ) e. NN0 ) -> ( m + ( m - 1 ) ) e. NN )
83 80 81 82 syl2anc2 
 |-  ( ( ph /\ m e. NN ) -> ( m + ( m - 1 ) ) e. NN )
84 79 83 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( 2 x. m ) - 1 ) e. NN )
85 oveq1 
 |-  ( n = ( ( 2 x. m ) - 1 ) -> ( n / 2 ) = ( ( ( 2 x. m ) - 1 ) / 2 ) )
86 85 eleq1d 
 |-  ( n = ( ( 2 x. m ) - 1 ) -> ( ( n / 2 ) e. NN <-> ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN ) )
87 85 fveq2d 
 |-  ( n = ( ( 2 x. m ) - 1 ) -> ( G ` ( n / 2 ) ) = ( G ` ( ( ( 2 x. m ) - 1 ) / 2 ) ) )
88 oveq1 
 |-  ( n = ( ( 2 x. m ) - 1 ) -> ( n + 1 ) = ( ( ( 2 x. m ) - 1 ) + 1 ) )
89 88 fvoveq1d 
 |-  ( n = ( ( 2 x. m ) - 1 ) -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) )
90 86 87 89 ifbieq12d 
 |-  ( n = ( ( 2 x. m ) - 1 ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = if ( ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. m ) - 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) ) )
91 fvex 
 |-  ( G ` ( ( ( 2 x. m ) - 1 ) / 2 ) ) e. _V
92 fvex 
 |-  ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) e. _V
93 91 92 ifex 
 |-  if ( ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. m ) - 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) ) e. _V
94 90 13 93 fvmpt 
 |-  ( ( ( 2 x. m ) - 1 ) e. NN -> ( H ` ( ( 2 x. m ) - 1 ) ) = if ( ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. m ) - 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) ) )
95 84 94 syl 
 |-  ( ( ph /\ m e. NN ) -> ( H ` ( ( 2 x. m ) - 1 ) ) = if ( ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. m ) - 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) ) )
96 2nn 
 |-  2 e. NN
97 nnmulcl 
 |-  ( ( 2 e. NN /\ m e. NN ) -> ( 2 x. m ) e. NN )
98 96 80 97 sylancr 
 |-  ( ( ph /\ m e. NN ) -> ( 2 x. m ) e. NN )
99 98 nncnd 
 |-  ( ( ph /\ m e. NN ) -> ( 2 x. m ) e. CC )
100 ax-1cn 
 |-  1 e. CC
101 npcan 
 |-  ( ( ( 2 x. m ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. m ) - 1 ) + 1 ) = ( 2 x. m ) )
102 99 100 101 sylancl 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( 2 x. m ) - 1 ) + 1 ) = ( 2 x. m ) )
103 102 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) = ( ( 2 x. m ) / 2 ) )
104 2cn 
 |-  2 e. CC
105 2ne0 
 |-  2 =/= 0
106 divcan3 
 |-  ( ( m e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. m ) / 2 ) = m )
107 104 105 106 mp3an23 
 |-  ( m e. CC -> ( ( 2 x. m ) / 2 ) = m )
108 75 107 syl 
 |-  ( ( ph /\ m e. NN ) -> ( ( 2 x. m ) / 2 ) = m )
109 103 108 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) = m )
110 109 80 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) e. NN )
111 nneo 
 |-  ( ( ( 2 x. m ) - 1 ) e. NN -> ( ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN <-> -. ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) e. NN ) )
112 84 111 syl 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN <-> -. ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) e. NN ) )
113 112 con2bid 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) e. NN <-> -. ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN ) )
114 110 113 mpbid 
 |-  ( ( ph /\ m e. NN ) -> -. ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN )
115 114 iffalsed 
 |-  ( ( ph /\ m e. NN ) -> if ( ( ( ( 2 x. m ) - 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. m ) - 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) ) = ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) )
116 109 fveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( F ` ( ( ( ( 2 x. m ) - 1 ) + 1 ) / 2 ) ) = ( F ` m ) )
117 95 115 116 3eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( H ` ( ( 2 x. m ) - 1 ) ) = ( F ` m ) )
118 fveqeq2 
 |-  ( k = ( ( 2 x. m ) - 1 ) -> ( ( H ` k ) = ( F ` m ) <-> ( H ` ( ( 2 x. m ) - 1 ) ) = ( F ` m ) ) )
119 118 rspcev 
 |-  ( ( ( ( 2 x. m ) - 1 ) e. NN /\ ( H ` ( ( 2 x. m ) - 1 ) ) = ( F ` m ) ) -> E. k e. NN ( H ` k ) = ( F ` m ) )
120 84 117 119 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> E. k e. NN ( H ` k ) = ( F ` m ) )
121 fveq2 
 |-  ( ( H ` k ) = ( F ` m ) -> ( 1st ` ( H ` k ) ) = ( 1st ` ( F ` m ) ) )
122 121 breq1d 
 |-  ( ( H ` k ) = ( F ` m ) -> ( ( 1st ` ( H ` k ) ) < z <-> ( 1st ` ( F ` m ) ) < z ) )
123 fveq2 
 |-  ( ( H ` k ) = ( F ` m ) -> ( 2nd ` ( H ` k ) ) = ( 2nd ` ( F ` m ) ) )
124 123 breq2d 
 |-  ( ( H ` k ) = ( F ` m ) -> ( z < ( 2nd ` ( H ` k ) ) <-> z < ( 2nd ` ( F ` m ) ) ) )
125 122 124 anbi12d 
 |-  ( ( H ` k ) = ( F ` m ) -> ( ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) <-> ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) ) )
126 125 biimprcd 
 |-  ( ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) -> ( ( H ` k ) = ( F ` m ) -> ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
127 126 reximdv 
 |-  ( ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) -> ( E. k e. NN ( H ` k ) = ( F ` m ) -> E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
128 120 127 syl5com 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) -> E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
129 128 rexlimdva 
 |-  ( ph -> ( E. m e. NN ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) -> E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
130 129 ralimdv 
 |-  ( ph -> ( A. z e. A E. m e. NN ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) -> A. z e. A E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
131 ovolfioo 
 |-  ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U. ran ( (,) o. F ) <-> A. z e. A E. m e. NN ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) ) )
132 14 26 131 syl2anc 
 |-  ( ph -> ( A C_ U. ran ( (,) o. F ) <-> A. z e. A E. m e. NN ( ( 1st ` ( F ` m ) ) < z /\ z < ( 2nd ` ( F ` m ) ) ) ) )
133 ovolfioo 
 |-  ( ( A C_ RR /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U. ran ( (,) o. H ) <-> A. z e. A E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
134 14 31 133 syl2anc 
 |-  ( ph -> ( A C_ U. ran ( (,) o. H ) <-> A. z e. A E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
135 130 132 134 3imtr4d 
 |-  ( ph -> ( A C_ U. ran ( (,) o. F ) -> A C_ U. ran ( (,) o. H ) ) )
136 8 135 mpd 
 |-  ( ph -> A C_ U. ran ( (,) o. H ) )
137 oveq1 
 |-  ( n = ( 2 x. m ) -> ( n / 2 ) = ( ( 2 x. m ) / 2 ) )
138 137 eleq1d 
 |-  ( n = ( 2 x. m ) -> ( ( n / 2 ) e. NN <-> ( ( 2 x. m ) / 2 ) e. NN ) )
139 137 fveq2d 
 |-  ( n = ( 2 x. m ) -> ( G ` ( n / 2 ) ) = ( G ` ( ( 2 x. m ) / 2 ) ) )
140 oveq1 
 |-  ( n = ( 2 x. m ) -> ( n + 1 ) = ( ( 2 x. m ) + 1 ) )
141 140 fvoveq1d 
 |-  ( n = ( 2 x. m ) -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` ( ( ( 2 x. m ) + 1 ) / 2 ) ) )
142 138 139 141 ifbieq12d 
 |-  ( n = ( 2 x. m ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = if ( ( ( 2 x. m ) / 2 ) e. NN , ( G ` ( ( 2 x. m ) / 2 ) ) , ( F ` ( ( ( 2 x. m ) + 1 ) / 2 ) ) ) )
143 fvex 
 |-  ( G ` ( ( 2 x. m ) / 2 ) ) e. _V
144 fvex 
 |-  ( F ` ( ( ( 2 x. m ) + 1 ) / 2 ) ) e. _V
145 143 144 ifex 
 |-  if ( ( ( 2 x. m ) / 2 ) e. NN , ( G ` ( ( 2 x. m ) / 2 ) ) , ( F ` ( ( ( 2 x. m ) + 1 ) / 2 ) ) ) e. _V
146 142 13 145 fvmpt 
 |-  ( ( 2 x. m ) e. NN -> ( H ` ( 2 x. m ) ) = if ( ( ( 2 x. m ) / 2 ) e. NN , ( G ` ( ( 2 x. m ) / 2 ) ) , ( F ` ( ( ( 2 x. m ) + 1 ) / 2 ) ) ) )
147 98 146 syl 
 |-  ( ( ph /\ m e. NN ) -> ( H ` ( 2 x. m ) ) = if ( ( ( 2 x. m ) / 2 ) e. NN , ( G ` ( ( 2 x. m ) / 2 ) ) , ( F ` ( ( ( 2 x. m ) + 1 ) / 2 ) ) ) )
148 108 80 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( 2 x. m ) / 2 ) e. NN )
149 148 iftrued 
 |-  ( ( ph /\ m e. NN ) -> if ( ( ( 2 x. m ) / 2 ) e. NN , ( G ` ( ( 2 x. m ) / 2 ) ) , ( F ` ( ( ( 2 x. m ) + 1 ) / 2 ) ) ) = ( G ` ( ( 2 x. m ) / 2 ) ) )
150 108 fveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( G ` ( ( 2 x. m ) / 2 ) ) = ( G ` m ) )
151 147 149 150 3eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( H ` ( 2 x. m ) ) = ( G ` m ) )
152 fveqeq2 
 |-  ( k = ( 2 x. m ) -> ( ( H ` k ) = ( G ` m ) <-> ( H ` ( 2 x. m ) ) = ( G ` m ) ) )
153 152 rspcev 
 |-  ( ( ( 2 x. m ) e. NN /\ ( H ` ( 2 x. m ) ) = ( G ` m ) ) -> E. k e. NN ( H ` k ) = ( G ` m ) )
154 98 151 153 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> E. k e. NN ( H ` k ) = ( G ` m ) )
155 fveq2 
 |-  ( ( H ` k ) = ( G ` m ) -> ( 1st ` ( H ` k ) ) = ( 1st ` ( G ` m ) ) )
156 155 breq1d 
 |-  ( ( H ` k ) = ( G ` m ) -> ( ( 1st ` ( H ` k ) ) < z <-> ( 1st ` ( G ` m ) ) < z ) )
157 fveq2 
 |-  ( ( H ` k ) = ( G ` m ) -> ( 2nd ` ( H ` k ) ) = ( 2nd ` ( G ` m ) ) )
158 157 breq2d 
 |-  ( ( H ` k ) = ( G ` m ) -> ( z < ( 2nd ` ( H ` k ) ) <-> z < ( 2nd ` ( G ` m ) ) ) )
159 156 158 anbi12d 
 |-  ( ( H ` k ) = ( G ` m ) -> ( ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) <-> ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) ) )
160 159 biimprcd 
 |-  ( ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) -> ( ( H ` k ) = ( G ` m ) -> ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
161 160 reximdv 
 |-  ( ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) -> ( E. k e. NN ( H ` k ) = ( G ` m ) -> E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
162 154 161 syl5com 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) -> E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
163 162 rexlimdva 
 |-  ( ph -> ( E. m e. NN ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) -> E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
164 163 ralimdv 
 |-  ( ph -> ( A. z e. B E. m e. NN ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) -> A. z e. B E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
165 ovolfioo 
 |-  ( ( B C_ RR /\ G : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( B C_ U. ran ( (,) o. G ) <-> A. z e. B E. m e. NN ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) ) )
166 15 18 165 syl2anc 
 |-  ( ph -> ( B C_ U. ran ( (,) o. G ) <-> A. z e. B E. m e. NN ( ( 1st ` ( G ` m ) ) < z /\ z < ( 2nd ` ( G ` m ) ) ) ) )
167 ovolfioo 
 |-  ( ( B C_ RR /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( B C_ U. ran ( (,) o. H ) <-> A. z e. B E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
168 15 31 167 syl2anc 
 |-  ( ph -> ( B C_ U. ran ( (,) o. H ) <-> A. z e. B E. k e. NN ( ( 1st ` ( H ` k ) ) < z /\ z < ( 2nd ` ( H ` k ) ) ) ) )
169 164 166 168 3imtr4d 
 |-  ( ph -> ( B C_ U. ran ( (,) o. G ) -> B C_ U. ran ( (,) o. H ) ) )
170 11 169 mpd 
 |-  ( ph -> B C_ U. ran ( (,) o. H ) )
171 136 170 unssd 
 |-  ( ph -> ( A u. B ) C_ U. ran ( (,) o. H ) )
172 6 ovollb 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( A u. B ) C_ U. ran ( (,) o. H ) ) -> ( vol* ` ( A u. B ) ) <_ sup ( ran U , RR* , < ) )
173 31 171 172 syl2anc 
 |-  ( ph -> ( vol* ` ( A u. B ) ) <_ sup ( ran U , RR* , < ) )
174 ovollecl 
 |-  ( ( ( A u. B ) C_ RR /\ sup ( ran U , RR* , < ) e. RR /\ ( vol* ` ( A u. B ) ) <_ sup ( ran U , RR* , < ) ) -> ( vol* ` ( A u. B ) ) e. RR )
175 16 73 173 174 syl3anc 
 |-  ( ph -> ( vol* ` ( A u. B ) ) e. RR )
176 58 rexrd 
 |-  ( ph -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR* )
177 supxrleub 
 |-  ( ( ran U C_ RR* /\ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR* ) -> ( sup ( ran U , RR* , < ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) <-> A. z e. ran U z <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) )
178 68 176 177 syl2anc 
 |-  ( ph -> ( sup ( ran U , RR* , < ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) <-> A. z e. ran U z <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) ) )
179 64 178 mpbird 
 |-  ( ph -> sup ( ran U , RR* , < ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
180 175 73 58 173 179 letrd 
 |-  ( ph -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )