Metamath Proof Explorer

Theorem hoidmvlelem4

Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of Fremlin1 p. 29, case nonempty interval and dimension of the space greater than 1 . (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem4.l 
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
hoidmvlelem4.x 
|- ( ph -> X e. Fin )
hoidmvlelem4.y 
|- ( ph -> Y C_ X )
hoidmvlelem4.n 
|- ( ph -> Y =/= (/) )
hoidmvlelem4.z 
|- ( ph -> Z e. ( X \ Y ) )
hoidmvlelem4.w 
|- W = ( Y u. { Z } )
hoidmvlelem4.a 
|- ( ph -> A : W --> RR )
hoidmvlelem4.b 
|- ( ph -> B : W --> RR )
hoidmvlelem4.k 
|- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
hoidmvlelem4.c 
|- ( ph -> C : NN --> ( RR ^m W ) )
hoidmvlelem4.d 
|- ( ph -> D : NN --> ( RR ^m W ) )
hoidmvlelem4.r 
|- ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
hoidmvlelem4.h 
|- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
hoidmvlelem4.14 
|- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
hoidmvlelem4.e 
|- ( ph -> E e. RR+ )
hoidmvlelem4.u 
|- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
hoidmvlelem4.s 
|- S = sup ( U , RR , < )
hoidmvlelem4.i 
|- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
hoidmvlelem4.i2 
|- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
Assertion hoidmvlelem4 
|- ( ph -> ( A ( L ` W ) B ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmvlelem4.l 
 |-  L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
2 hoidmvlelem4.x 
 |-  ( ph -> X e. Fin )
3 hoidmvlelem4.y 
 |-  ( ph -> Y C_ X )
4 hoidmvlelem4.n 
 |-  ( ph -> Y =/= (/) )
5 hoidmvlelem4.z 
 |-  ( ph -> Z e. ( X \ Y ) )
6 hoidmvlelem4.w 
 |-  W = ( Y u. { Z } )
7 hoidmvlelem4.a 
 |-  ( ph -> A : W --> RR )
8 hoidmvlelem4.b 
 |-  ( ph -> B : W --> RR )
9 hoidmvlelem4.k 
 |-  ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
10 hoidmvlelem4.c 
 |-  ( ph -> C : NN --> ( RR ^m W ) )
11 hoidmvlelem4.d 
 |-  ( ph -> D : NN --> ( RR ^m W ) )
12 hoidmvlelem4.r 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
13 hoidmvlelem4.h 
 |-  H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
14 hoidmvlelem4.14 
 |-  G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
15 hoidmvlelem4.e 
 |-  ( ph -> E e. RR+ )
16 hoidmvlelem4.u 
 |-  U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
17 hoidmvlelem4.s 
 |-  S = sup ( U , RR , < )
18 hoidmvlelem4.i 
 |-  ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
19 hoidmvlelem4.i2 
 |-  ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
20 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
21 5 eldifad 
 |-  ( ph -> Z e. X )
22 snssi 
 |-  ( Z e. X -> { Z } C_ X )
23 21 22 syl 
 |-  ( ph -> { Z } C_ X )
24 3 23 unssd 
 |-  ( ph -> ( Y u. { Z } ) C_ X )
25 6 24 eqsstrid 
 |-  ( ph -> W C_ X )
26 ssfi 
 |-  ( ( X e. Fin /\ W C_ X ) -> W e. Fin )
27 2 25 26 syl2anc 
 |-  ( ph -> W e. Fin )
28 1 27 7 8 hoidmvcl 
 |-  ( ph -> ( A ( L ` W ) B ) e. ( 0 [,) +oo ) )
29 20 28 sseldi 
 |-  ( ph -> ( A ( L ` W ) B ) e. RR )
30 1red 
 |-  ( ph -> 1 e. RR )
31 15 rpred 
 |-  ( ph -> E e. RR )
32 30 31 readdcld 
 |-  ( ph -> ( 1 + E ) e. RR )
33 nfv 
 |-  F/ j ph
34 nnex 
 |-  NN e. _V
35 34 a1i 
 |-  ( ph -> NN e. _V )
36 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
37 27 adantr 
 |-  ( ( ph /\ j e. NN ) -> W e. Fin )
38 10 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
39 elmapi 
 |-  ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
40 38 39 syl 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
41 eleq1 
 |-  ( j = h -> ( j e. Y <-> h e. Y ) )
42 fveq2 
 |-  ( j = h -> ( c ` j ) = ( c ` h ) )
43 42 breq1d 
 |-  ( j = h -> ( ( c ` j ) <_ x <-> ( c ` h ) <_ x ) )
44 43 42 ifbieq1d 
 |-  ( j = h -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` h ) <_ x , ( c ` h ) , x ) )
45 41 42 44 ifbieq12d 
 |-  ( j = h -> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) = if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) )
46 45 cbvmptv 
 |-  ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) = ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) )
47 46 mpteq2i 
 |-  ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) = ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) )
48 47 mpteq2i 
 |-  ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) ) = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) ) )
49 13 48 eqtri 
 |-  H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) ) )
50 snidg 
 |-  ( Z e. ( X \ Y ) -> Z e. { Z } )
51 5 50 syl 
 |-  ( ph -> Z e. { Z } )
52 elun2 
 |-  ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
53 51 52 syl 
 |-  ( ph -> Z e. ( Y u. { Z } ) )
54 6 a1i 
 |-  ( ph -> W = ( Y u. { Z } ) )
55 54 eqcomd 
 |-  ( ph -> ( Y u. { Z } ) = W )
56 53 55 eleqtrd 
 |-  ( ph -> Z e. W )
57 8 56 ffvelrnd 
 |-  ( ph -> ( B ` Z ) e. RR )
58 57 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( B ` Z ) e. RR )
59 11 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
60 elmapi 
 |-  ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
61 59 60 syl 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
62 49 58 37 61 hsphoif 
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) : W --> RR )
63 1 37 40 62 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
64 36 63 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
65 33 35 64 sge0clmpt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) )
66 33 35 64 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) e. RR* )
67 pnfxr 
 |-  +oo e. RR*
68 67 a1i 
 |-  ( ph -> +oo e. RR* )
69 12 rexrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
70 1 37 40 61 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,) +oo ) )
71 36 70 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,] +oo ) )
72 5 eldifbd 
 |-  ( ph -> -. Z e. Y )
73 56 72 eldifd 
 |-  ( ph -> Z e. ( W \ Y ) )
74 73 adantr 
 |-  ( ( ph /\ j e. NN ) -> Z e. ( W \ Y ) )
75 1 37 74 6 58 49 40 61 hsphoidmvle 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
76 33 35 64 71 75 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
77 12 ltpnfd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) < +oo )
78 66 69 68 76 77 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) < +oo )
79 66 68 78 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) =/= +oo )
80 ge0xrre 
 |-  ( ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) =/= +oo ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) e. RR )
81 65 79 80 syl2anc 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) e. RR )
82 32 81 remulcld 
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) e. RR )
83 32 12 remulcld 
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) e. RR )
84 56 ancli 
 |-  ( ph -> ( ph /\ Z e. W ) )
85 eleq1 
 |-  ( k = Z -> ( k e. W <-> Z e. W ) )
86 85 anbi2d 
 |-  ( k = Z -> ( ( ph /\ k e. W ) <-> ( ph /\ Z e. W ) ) )
87 fveq2 
 |-  ( k = Z -> ( A ` k ) = ( A ` Z ) )
88 fveq2 
 |-  ( k = Z -> ( B ` k ) = ( B ` Z ) )
89 87 88 breq12d 
 |-  ( k = Z -> ( ( A ` k ) < ( B ` k ) <-> ( A ` Z ) < ( B ` Z ) ) )
90 86 89 imbi12d 
 |-  ( k = Z -> ( ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) ) <-> ( ( ph /\ Z e. W ) -> ( A ` Z ) < ( B ` Z ) ) ) )
91 90 9 vtoclg 
 |-  ( Z e. W -> ( ( ph /\ Z e. W ) -> ( A ` Z ) < ( B ` Z ) ) )
92 56 84 91 sylc 
 |-  ( ph -> ( A ` Z ) < ( B ` Z ) )
93 1 2 3 5 6 7 8 10 11 12 13 14 15 16 17 92 hoidmvlelem1 
 |-  ( ph -> S e. U )
94 57 rexrd 
 |-  ( ph -> ( B ` Z ) e. RR* )
95 iccssxr 
 |-  ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR*
96 ssrab2 
 |-  { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } C_ ( ( A ` Z ) [,] ( B ` Z ) )
97 16 96 eqsstri 
 |-  U C_ ( ( A ` Z ) [,] ( B ` Z ) )
98 97 93 sseldi 
 |-  ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) )
99 95 98 sseldi 
 |-  ( ph -> S e. RR* )
100 simpl 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> ph )
101 simpr 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> -. ( B ` Z ) <_ S )
102 7 56 ffvelrnd 
 |-  ( ph -> ( A ` Z ) e. RR )
103 102 57 iccssred 
 |-  ( ph -> ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR )
104 103 98 sseldd 
 |-  ( ph -> S e. RR )
105 104 adantr 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> S e. RR )
106 100 57 syl 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> ( B ` Z ) e. RR )
107 105 106 ltnled 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> ( S < ( B ` Z ) <-> -. ( B ` Z ) <_ S ) )
108 101 107 mpbird 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> S < ( B ` Z ) )
109 2 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> X e. Fin )
110 3 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> Y C_ X )
111 5 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> Z e. ( X \ Y ) )
112 7 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> A : W --> RR )
113 8 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> B : W --> RR )
114 9 adantlr 
 |-  ( ( ( ph /\ S < ( B ` Z ) ) /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
115 eqid 
 |-  ( y e. Y |-> 0 ) = ( y e. Y |-> 0 )
116 10 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> C : NN --> ( RR ^m W ) )
117 fveq2 
 |-  ( i = j -> ( C ` i ) = ( C ` j ) )
118 117 fveq1d 
 |-  ( i = j -> ( ( C ` i ) ` Z ) = ( ( C ` j ) ` Z ) )
119 fveq2 
 |-  ( i = j -> ( D ` i ) = ( D ` j ) )
120 119 fveq1d 
 |-  ( i = j -> ( ( D ` i ) ` Z ) = ( ( D ` j ) ` Z ) )
121 118 120 oveq12d 
 |-  ( i = j -> ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
122 121 eleq2d 
 |-  ( i = j -> ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) <-> S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
123 117 reseq1d 
 |-  ( i = j -> ( ( C ` i ) |` Y ) = ( ( C ` j ) |` Y ) )
124 122 123 ifbieq1d 
 |-  ( i = j -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , ( y e. Y |-> 0 ) ) )
125 124 cbvmptv 
 |-  ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , ( y e. Y |-> 0 ) ) )
126 11 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> D : NN --> ( RR ^m W ) )
127 119 reseq1d 
 |-  ( i = j -> ( ( D ` i ) |` Y ) = ( ( D ` j ) |` Y ) )
128 122 127 ifbieq1d 
 |-  ( i = j -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , ( y e. Y |-> 0 ) ) )
129 128 cbvmptv 
 |-  ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , ( y e. Y |-> 0 ) ) )
130 12 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
131 15 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> E e. RR+ )
132 93 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> S e. U )
133 simpr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> S < ( B ` Z ) )
134 biid 
 |-  ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
135 eqidd 
 |-  ( w = y -> 0 = 0 )
136 135 cbvmptv 
 |-  ( w e. Y |-> 0 ) = ( y e. Y |-> 0 )
137 134 136 ifbieq2i 
 |-  if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( w e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) )
138 137 mpteq2i 
 |-  ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) = ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
139 138 a1i 
 |-  ( l = j -> ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) = ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) )
140 id 
 |-  ( l = j -> l = j )
141 139 140 fveq12d 
 |-  ( l = j -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) ` l ) = ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` j ) )
142 134 136 ifbieq2i 
 |-  if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( w e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) )
143 142 mpteq2i 
 |-  ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) = ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
144 143 a1i 
 |-  ( l = j -> ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) = ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) )
145 144 140 fveq12d 
 |-  ( l = j -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) ` l ) = ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` j ) )
146 141 145 oveq12d 
 |-  ( l = j -> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) ` l ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) ` l ) ) = ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` j ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` j ) ) )
147 146 cbvmptv 
 |-  ( l e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) ` l ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( w e. Y |-> 0 ) ) ) ` l ) ) ) = ( j e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` j ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` j ) ) )
148 18 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
149 19 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
150 eqid 
 |-  ( x e. X_ y e. Y ( ( A ` y ) [,) ( B ` y ) ) |-> ( y e. W |-> if ( y e. Y , ( x ` y ) , S ) ) ) = ( x e. X_ y e. Y ( ( A ` y ) [,) ( B ` y ) ) |-> ( y e. W |-> if ( y e. Y , ( x ` y ) , S ) ) )
151 fveq2 
 |-  ( y = k -> ( A ` y ) = ( A ` k ) )
152 fveq2 
 |-  ( y = k -> ( B ` y ) = ( B ` k ) )
153 151 152 oveq12d 
 |-  ( y = k -> ( ( A ` y ) [,) ( B ` y ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
154 153 cbvixpv 
 |-  X_ y e. Y ( ( A ` y ) [,) ( B ` y ) ) = X_ k e. Y ( ( A ` k ) [,) ( B ` k ) )
155 eleq1 
 |-  ( y = k -> ( y e. Y <-> k e. Y ) )
156 fveq2 
 |-  ( y = k -> ( x ` y ) = ( x ` k ) )
157 155 156 ifbieq1d 
 |-  ( y = k -> if ( y e. Y , ( x ` y ) , S ) = if ( k e. Y , ( x ` k ) , S ) )
158 157 cbvmptv 
 |-  ( y e. W |-> if ( y e. Y , ( x ` y ) , S ) ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) )
159 154 158 mpteq12i 
 |-  ( x e. X_ y e. Y ( ( A ` y ) [,) ( B ` y ) ) |-> ( y e. W |-> if ( y e. Y , ( x ` y ) , S ) ) ) = ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) |-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
160 150 159 eqtri 
 |-  ( x e. X_ y e. Y ( ( A ` y ) [,) ( B ` y ) ) |-> ( y e. W |-> if ( y e. Y , ( x ` y ) , S ) ) ) = ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) |-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
161 1 109 110 111 6 112 113 114 115 116 125 126 129 130 13 14 131 16 132 133 147 148 149 160 hoidmvlelem3 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> E. u e. U S < u )
162 100 108 161 syl2anc 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> E. u e. U S < u )
163 97 a1i 
 |-  ( ph -> U C_ ( ( A ` Z ) [,] ( B ` Z ) ) )
164 163 103 sstrd 
 |-  ( ph -> U C_ RR )
165 164 adantr 
 |-  ( ( ph /\ u e. U ) -> U C_ RR )
166 ne0i 
 |-  ( u e. U -> U =/= (/) )
167 166 adantl 
 |-  ( ( ph /\ u e. U ) -> U =/= (/) )
168 102 rexrd 
 |-  ( ph -> ( A ` Z ) e. RR* )
169 168 adantr 
 |-  ( ( ph /\ u e. U ) -> ( A ` Z ) e. RR* )
170 94 adantr 
 |-  ( ( ph /\ u e. U ) -> ( B ` Z ) e. RR* )
171 163 sselda 
 |-  ( ( ph /\ u e. U ) -> u e. ( ( A ` Z ) [,] ( B ` Z ) ) )
172 iccleub 
 |-  ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ u e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> u <_ ( B ` Z ) )
173 169 170 171 172 syl3anc 
 |-  ( ( ph /\ u e. U ) -> u <_ ( B ` Z ) )
174 173 ralrimiva 
 |-  ( ph -> A. u e. U u <_ ( B ` Z ) )
175 brralrspcev 
 |-  ( ( ( B ` Z ) e. RR /\ A. u e. U u <_ ( B ` Z ) ) -> E. y e. RR A. u e. U u <_ y )
176 57 174 175 syl2anc 
 |-  ( ph -> E. y e. RR A. u e. U u <_ y )
177 176 adantr 
 |-  ( ( ph /\ u e. U ) -> E. y e. RR A. u e. U u <_ y )
178 simpr 
 |-  ( ( ph /\ u e. U ) -> u e. U )
179 suprub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. y e. RR A. u e. U u <_ y ) /\ u e. U ) -> u <_ sup ( U , RR , < ) )
180 165 167 177 178 179 syl31anc 
 |-  ( ( ph /\ u e. U ) -> u <_ sup ( U , RR , < ) )
181 180 17 breqtrrdi 
 |-  ( ( ph /\ u e. U ) -> u <_ S )
182 181 ralrimiva 
 |-  ( ph -> A. u e. U u <_ S )
183 165 178 sseldd 
 |-  ( ( ph /\ u e. U ) -> u e. RR )
184 104 adantr 
 |-  ( ( ph /\ u e. U ) -> S e. RR )
185 183 184 lenltd 
 |-  ( ( ph /\ u e. U ) -> ( u <_ S <-> -. S < u ) )
186 185 ralbidva 
 |-  ( ph -> ( A. u e. U u <_ S <-> A. u e. U -. S < u ) )
187 182 186 mpbid 
 |-  ( ph -> A. u e. U -. S < u )
188 ralnex 
 |-  ( A. u e. U -. S < u <-> -. E. u e. U S < u )
189 187 188 sylib 
 |-  ( ph -> -. E. u e. U S < u )
190 189 adantr 
 |-  ( ( ph /\ S < ( B ` Z ) ) -> -. E. u e. U S < u )
191 100 108 190 syl2anc 
 |-  ( ( ph /\ -. ( B ` Z ) <_ S ) -> -. E. u e. U S < u )
192 162 191 condan 
 |-  ( ph -> ( B ` Z ) <_ S )
193 iccleub 
 |-  ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ S e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> S <_ ( B ` Z ) )
194 168 94 98 193 syl3anc 
 |-  ( ph -> S <_ ( B ` Z ) )
195 94 99 192 194 xrletrid 
 |-  ( ph -> ( B ` Z ) = S )
196 16 eqcomi 
 |-  { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } = U
197 196 a1i 
 |-  ( ph -> { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } = U )
198 195 197 eleq12d 
 |-  ( ph -> ( ( B ` Z ) e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } <-> S e. U ) )
199 93 198 mpbird 
 |-  ( ph -> ( B ` Z ) e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
200 oveq1 
 |-  ( z = ( B ` Z ) -> ( z - ( A ` Z ) ) = ( ( B ` Z ) - ( A ` Z ) ) )
201 200 oveq2d 
 |-  ( z = ( B ` Z ) -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
202 fveq2 
 |-  ( z = ( B ` Z ) -> ( H ` z ) = ( H ` ( B ` Z ) ) )
203 202 fveq1d 
 |-  ( z = ( B ` Z ) -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) )
204 203 oveq2d 
 |-  ( z = ( B ` Z ) -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) )
205 204 mpteq2dv 
 |-  ( z = ( B ` Z ) -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) )
206 205 fveq2d 
 |-  ( z = ( B ` Z ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) )
207 206 oveq2d 
 |-  ( z = ( B ` Z ) -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) )
208 201 207 breq12d 
 |-  ( z = ( B ` Z ) -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) )
209 208 elrab 
 |-  ( ( B ` Z ) e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } <-> ( ( B ` Z ) e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) )
210 199 209 sylib 
 |-  ( ph -> ( ( B ` Z ) e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) )
211 210 simprd 
 |-  ( ph -> ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) )
212 2 3 ssfid 
 |-  ( ph -> Y e. Fin )
213 eqid 
 |-  prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) )
214 1 212 5 72 6 7 8 213 hoiprodp1 
 |-  ( ph -> ( A ( L ` W ) B ) = ( prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) )
215 eqidd 
 |-  ( ph -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
216 7 adantr 
 |-  ( ( ph /\ k e. Y ) -> A : W --> RR )
217 ssun1 
 |-  Y C_ ( Y u. { Z } )
218 6 eqcomi 
 |-  ( Y u. { Z } ) = W
219 217 218 sseqtri 
 |-  Y C_ W
220 simpr 
 |-  ( ( ph /\ k e. Y ) -> k e. Y )
221 219 220 sseldi 
 |-  ( ( ph /\ k e. Y ) -> k e. W )
222 216 221 ffvelrnd 
 |-  ( ( ph /\ k e. Y ) -> ( A ` k ) e. RR )
223 8 adantr 
 |-  ( ( ph /\ k e. Y ) -> B : W --> RR )
224 223 221 ffvelrnd 
 |-  ( ( ph /\ k e. Y ) -> ( B ` k ) e. RR )
225 221 9 syldan 
 |-  ( ( ph /\ k e. Y ) -> ( A ` k ) < ( B ` k ) )
226 222 224 225 volicon0 
 |-  ( ( ph /\ k e. Y ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( ( B ` k ) - ( A ` k ) ) )
227 226 prodeq2dv 
 |-  ( ph -> prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
228 14 a1i 
 |-  ( ph -> G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) )
229 219 a1i 
 |-  ( ph -> Y C_ W )
230 7 229 fssresd 
 |-  ( ph -> ( A |` Y ) : Y --> RR )
231 8 229 fssresd 
 |-  ( ph -> ( B |` Y ) : Y --> RR )
232 1 212 4 230 231 hoidmvn0val 
 |-  ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) )
233 fvres 
 |-  ( k e. Y -> ( ( A |` Y ) ` k ) = ( A ` k ) )
234 fvres 
 |-  ( k e. Y -> ( ( B |` Y ) ` k ) = ( B ` k ) )
235 233 234 oveq12d 
 |-  ( k e. Y -> ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
236 235 fveq2d 
 |-  ( k e. Y -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
237 236 adantl 
 |-  ( ( ph /\ k e. Y ) -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
238 volico 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
239 222 224 238 syl2anc 
 |-  ( ( ph /\ k e. Y ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
240 239 226 eqtr3d 
 |-  ( ( ph /\ k e. Y ) -> if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) = ( ( B ` k ) - ( A ` k ) ) )
241 237 239 240 3eqtrd 
 |-  ( ( ph /\ k e. Y ) -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( ( B ` k ) - ( A ` k ) ) )
242 241 prodeq2dv 
 |-  ( ph -> prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
243 228 232 242 3eqtrd 
 |-  ( ph -> G = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
244 215 227 243 3eqtr4d 
 |-  ( ph -> prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = G )
245 102 57 92 volicon0 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) = ( ( B ` Z ) - ( A ` Z ) ) )
246 244 245 oveq12d 
 |-  ( ph -> ( prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) = ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
247 214 246 eqtrd 
 |-  ( ph -> ( A ( L ` W ) B ) = ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) )
248 247 breq1d 
 |-  ( ph -> ( ( A ( L ` W ) B ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( ( B ` Z ) - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) ) )
249 211 248 mpbird 
 |-  ( ph -> ( A ( L ` W ) B ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) )
250 0le1 
 |-  0 <_ 1
251 250 a1i 
 |-  ( ph -> 0 <_ 1 )
252 15 rpge0d 
 |-  ( ph -> 0 <_ E )
253 30 31 251 252 addge0d 
 |-  ( ph -> 0 <_ ( 1 + E ) )
254 81 12 32 253 76 lemul2ad 
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` ( B ` Z ) ) ` ( D ` j ) ) ) ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )
255 29 82 83 249 254 letrd 
 |-  ( ph -> ( A ( L ` W ) B ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )