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
|
sselid |
|- ( 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
|
sselid |
|- ( ( 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
|
sselid |
|- ( ( 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
|
sselid |
|- ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) ) |
99 |
95 98
|
sselid |
|- ( 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
|
sselid |
|- ( ( 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 ) ) ) ) ) ) |