Metamath Proof Explorer

Theorem hoidmvlelem5

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. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem5.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 ) ) ) ) ) )
hoidmvlelem5.f 
|- ( ph -> X e. Fin )
hoidmvlelem5.y 
|- ( ph -> Y C_ X )
hoidmvlelem5.z 
|- ( ph -> Z e. ( X \ Y ) )
hoidmvlelem5.w 
|- W = ( Y u. { Z } )
hoidmvlelem5.a 
|- ( ph -> A : W --> RR )
hoidmvlelem5.b 
|- ( ph -> B : W --> RR )
hoidmvlelem5.c 
|- ( ph -> C : NN --> ( RR ^m W ) )
hoidmvlelem5.d 
|- ( ph -> D : NN --> ( RR ^m W ) )
hoidmvlelem5.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 ) ) ) ) ) )
hoidmvlelem5.s 
|- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
hoidmvlelem5.n 
|- ( ph -> Y =/= (/) )
Assertion hoidmvlelem5 
|- ( ph -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmvlelem5.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 hoidmvlelem5.f 
 |-  ( ph -> X e. Fin )
3 hoidmvlelem5.y 
 |-  ( ph -> Y C_ X )
4 hoidmvlelem5.z 
 |-  ( ph -> Z e. ( X \ Y ) )
5 hoidmvlelem5.w 
 |-  W = ( Y u. { Z } )
6 hoidmvlelem5.a 
 |-  ( ph -> A : W --> RR )
7 hoidmvlelem5.b 
 |-  ( ph -> B : W --> RR )
8 hoidmvlelem5.c 
 |-  ( ph -> C : NN --> ( RR ^m W ) )
9 hoidmvlelem5.d 
 |-  ( ph -> D : NN --> ( RR ^m W ) )
10 hoidmvlelem5.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 ) ) ) ) ) )
11 hoidmvlelem5.s 
 |-  ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
12 hoidmvlelem5.n 
 |-  ( ph -> Y =/= (/) )
13 nfv 
 |-  F/ s ph
14 nfre1 
 |-  F/ s E. s e. W ( B ` s ) <_ ( A ` s )
15 13 14 nfan 
 |-  F/ s ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) )
16 ssfi 
 |-  ( ( X e. Fin /\ Y C_ X ) -> Y e. Fin )
17 2 3 16 syl2anc 
 |-  ( ph -> Y e. Fin )
18 snfi 
 |-  { Z } e. Fin
19 18 a1i 
 |-  ( ph -> { Z } e. Fin )
20 unfi 
 |-  ( ( Y e. Fin /\ { Z } e. Fin ) -> ( Y u. { Z } ) e. Fin )
21 17 19 20 syl2anc 
 |-  ( ph -> ( Y u. { Z } ) e. Fin )
22 5 21 eqeltrid 
 |-  ( ph -> W e. Fin )
23 22 adantr 
 |-  ( ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) ) -> W e. Fin )
24 6 adantr 
 |-  ( ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) ) -> A : W --> RR )
25 7 adantr 
 |-  ( ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) ) -> B : W --> RR )
26 simpr 
 |-  ( ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) ) -> E. s e. W ( B ` s ) <_ ( A ` s ) )
27 15 1 23 24 25 26 hoidmvval0 
 |-  ( ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) ) -> ( A ( L ` W ) B ) = 0 )
28 nnex 
 |-  NN e. _V
29 28 a1i 
 |-  ( ph -> NN e. _V )
30 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
31 22 adantr 
 |-  ( ( ph /\ j e. NN ) -> W e. Fin )
32 8 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
33 elmapi 
 |-  ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
34 32 33 syl 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
35 9 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
36 elmapi 
 |-  ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
37 35 36 syl 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
38 1 31 34 37 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,) +oo ) )
39 30 38 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,] +oo ) )
40 39 fmpttd 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) : NN --> ( 0 [,] +oo ) )
41 29 40 sge0ge0 
 |-  ( ph -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
42 41 adantr 
 |-  ( ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
43 27 42 eqbrtrd 
 |-  ( ( ph /\ E. s e. W ( B ` s ) <_ ( A ` s ) ) -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
44 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
45 1 22 6 7 hoidmvcl 
 |-  ( ph -> ( A ( L ` W ) B ) e. ( 0 [,) +oo ) )
46 44 45 sseldi 
 |-  ( ph -> ( A ( L ` W ) B ) e. RR* )
47 46 adantr 
 |-  ( ( ph /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( A ( L ` W ) B ) e. RR* )
48 29 40 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
49 48 adantr 
 |-  ( ( ph /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
50 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
51 50 45 sseldi 
 |-  ( ph -> ( A ( L ` W ) B ) e. RR )
52 ltpnf 
 |-  ( ( A ( L ` W ) B ) e. RR -> ( A ( L ` W ) B ) < +oo )
53 51 52 syl 
 |-  ( ph -> ( A ( L ` W ) B ) < +oo )
54 53 adantr 
 |-  ( ( ph /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( A ( L ` W ) B ) < +oo )
55 id 
 |-  ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo )
56 55 eqcomd 
 |-  ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo -> +oo = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
57 56 adantl 
 |-  ( ( ph /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> +oo = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
58 54 57 breqtrd 
 |-  ( ( ph /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( A ( L ` W ) B ) < ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
59 47 49 58 xrltled 
 |-  ( ( ph /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
60 59 adantlr 
 |-  ( ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
61 simpll 
 |-  ( ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ph )
62 simpr 
 |-  ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) -> -. E. s e. W ( B ` s ) <_ ( A ` s ) )
63 6 ffvelrnda 
 |-  ( ( ph /\ s e. W ) -> ( A ` s ) e. RR )
64 7 ffvelrnda 
 |-  ( ( ph /\ s e. W ) -> ( B ` s ) e. RR )
65 63 64 ltnled 
 |-  ( ( ph /\ s e. W ) -> ( ( A ` s ) < ( B ` s ) <-> -. ( B ` s ) <_ ( A ` s ) ) )
66 65 ralbidva 
 |-  ( ph -> ( A. s e. W ( A ` s ) < ( B ` s ) <-> A. s e. W -. ( B ` s ) <_ ( A ` s ) ) )
67 ralnex 
 |-  ( A. s e. W -. ( B ` s ) <_ ( A ` s ) <-> -. E. s e. W ( B ` s ) <_ ( A ` s ) )
68 67 a1i 
 |-  ( ph -> ( A. s e. W -. ( B ` s ) <_ ( A ` s ) <-> -. E. s e. W ( B ` s ) <_ ( A ` s ) ) )
69 66 68 bitrd 
 |-  ( ph -> ( A. s e. W ( A ` s ) < ( B ` s ) <-> -. E. s e. W ( B ` s ) <_ ( A ` s ) ) )
70 69 adantr 
 |-  ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) -> ( A. s e. W ( A ` s ) < ( B ` s ) <-> -. E. s e. W ( B ` s ) <_ ( A ` s ) ) )
71 62 70 mpbird 
 |-  ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) -> A. s e. W ( A ` s ) < ( B ` s ) )
72 71 adantr 
 |-  ( ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> A. s e. W ( A ` s ) < ( B ` s ) )
73 simpr 
 |-  ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo )
74 28 a1i 
 |-  ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> NN e. _V )
75 40 adantr 
 |-  ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) : NN --> ( 0 [,] +oo ) )
76 74 75 sge0repnf 
 |-  ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) )
77 73 76 mpbird 
 |-  ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
78 77 adantlr 
 |-  ( ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
79 simpll 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) /\ r e. RR+ ) -> ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) )
80 fveq2 
 |-  ( j = i -> ( C ` j ) = ( C ` i ) )
81 fveq2 
 |-  ( j = i -> ( D ` j ) = ( D ` i ) )
82 80 81 oveq12d 
 |-  ( j = i -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) = ( ( C ` i ) ( L ` W ) ( D ` i ) ) )
83 82 cbvmptv 
 |-  ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) = ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) )
84 83 fveq2i 
 |-  ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) )
85 84 eleq1i 
 |-  ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR <-> ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR )
86 85 biimpi 
 |-  ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR -> ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR )
87 86 ad2antlr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) /\ r e. RR+ ) -> ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR )
88 simpr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) /\ r e. RR+ ) -> r e. RR+ )
89 2 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> X e. Fin )
90 3 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> Y C_ X )
91 12 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> Y =/= (/) )
92 4 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> Z e. ( X \ Y ) )
93 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> A : W --> RR )
94 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> B : W --> RR )
95 fveq2 
 |-  ( s = k -> ( A ` s ) = ( A ` k ) )
96 fveq2 
 |-  ( s = k -> ( B ` s ) = ( B ` k ) )
97 95 96 breq12d 
 |-  ( s = k -> ( ( A ` s ) < ( B ` s ) <-> ( A ` k ) < ( B ` k ) ) )
98 97 cbvralvw 
 |-  ( A. s e. W ( A ` s ) < ( B ` s ) <-> A. k e. W ( A ` k ) < ( B ` k ) )
99 98 biimpi 
 |-  ( A. s e. W ( A ` s ) < ( B ` s ) -> A. k e. W ( A ` k ) < ( B ` k ) )
100 99 adantr 
 |-  ( ( A. s e. W ( A ` s ) < ( B ` s ) /\ k e. W ) -> A. k e. W ( A ` k ) < ( B ` k ) )
101 simpr 
 |-  ( ( A. s e. W ( A ` s ) < ( B ` s ) /\ k e. W ) -> k e. W )
102 rspa 
 |-  ( ( A. k e. W ( A ` k ) < ( B ` k ) /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
103 100 101 102 syl2anc 
 |-  ( ( A. s e. W ( A ` s ) < ( B ` s ) /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
104 103 ad5ant25 
 |-  ( ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
105 8 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> C : NN --> ( RR ^m W ) )
106 9 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> D : NN --> ( RR ^m W ) )
107 85 biimpri 
 |-  ( ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
108 107 ad2antlr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
109 fveq1 
 |-  ( d = c -> ( d ` i ) = ( c ` i ) )
110 109 breq1d 
 |-  ( d = c -> ( ( d ` i ) <_ x <-> ( c ` i ) <_ x ) )
111 110 109 ifbieq1d 
 |-  ( d = c -> if ( ( d ` i ) <_ x , ( d ` i ) , x ) = if ( ( c ` i ) <_ x , ( c ` i ) , x ) )
112 109 111 ifeq12d 
 |-  ( d = c -> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) = if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) )
113 112 mpteq2dv 
 |-  ( d = c -> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) = ( i e. W |-> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) ) )
114 eleq1w 
 |-  ( i = j -> ( i e. Y <-> j e. Y ) )
115 fveq2 
 |-  ( i = j -> ( c ` i ) = ( c ` j ) )
116 115 breq1d 
 |-  ( i = j -> ( ( c ` i ) <_ x <-> ( c ` j ) <_ x ) )
117 116 115 ifbieq1d 
 |-  ( i = j -> if ( ( c ` i ) <_ x , ( c ` i ) , x ) = if ( ( c ` j ) <_ x , ( c ` j ) , x ) )
118 114 115 117 ifbieq12d 
 |-  ( i = j -> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) = if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) )
119 118 cbvmptv 
 |-  ( i e. W |-> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) ) = ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) )
120 119 a1i 
 |-  ( d = c -> ( i e. W |-> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) ) = ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) )
121 113 120 eqtrd 
 |-  ( d = c -> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) = ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) )
122 121 cbvmptv 
 |-  ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) = ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) )
123 122 mpteq2i 
 |-  ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
124 eqid 
 |-  ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
125 simpr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> r e. RR+ )
126 oveq1 
 |-  ( w = z -> ( w - ( A ` Z ) ) = ( z - ( A ` Z ) ) )
127 126 oveq2d 
 |-  ( w = z -> ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( w - ( A ` Z ) ) ) = ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( z - ( A ` Z ) ) ) )
128 breq2 
 |-  ( w = x -> ( ( d ` i ) <_ w <-> ( d ` i ) <_ x ) )
129 eqidd 
 |-  ( w = x -> ( d ` i ) = ( d ` i ) )
130 id 
 |-  ( w = x -> w = x )
131 128 129 130 ifbieq12d 
 |-  ( w = x -> if ( ( d ` i ) <_ w , ( d ` i ) , w ) = if ( ( d ` i ) <_ x , ( d ` i ) , x ) )
132 131 ifeq2d 
 |-  ( w = x -> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) = if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) )
133 132 mpteq2dv 
 |-  ( w = x -> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) = ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) )
134 133 mpteq2dv 
 |-  ( w = x -> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) = ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) )
135 134 cbvmptv 
 |-  ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) = ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) )
136 135 a1i 
 |-  ( w = z -> ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) = ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) )
137 id 
 |-  ( w = z -> w = z )
138 136 137 fveq12d 
 |-  ( w = z -> ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) = ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) )
139 138 fveq1d 
 |-  ( w = z -> ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) = ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` l ) ) )
140 139 oveq2d 
 |-  ( w = z -> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) = ( ( C ` l ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` l ) ) ) )
141 140 mpteq2dv 
 |-  ( w = z -> ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) = ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` l ) ) ) ) )
142 fveq2 
 |-  ( l = j -> ( C ` l ) = ( C ` j ) )
143 2fveq3 
 |-  ( l = j -> ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` l ) ) = ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) )
144 142 143 oveq12d 
 |-  ( l = j -> ( ( C ` l ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` l ) ) ) = ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) )
145 144 cbvmptv 
 |-  ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` l ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) )
146 145 a1i 
 |-  ( w = z -> ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` l ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) ) )
147 141 146 eqtrd 
 |-  ( w = z -> ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) ) )
148 147 fveq2d 
 |-  ( w = z -> ( sum^ ` ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) ) ) )
149 148 oveq2d 
 |-  ( w = z -> ( ( 1 + r ) x. ( sum^ ` ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) ) ) = ( ( 1 + r ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) ) ) ) )
150 127 149 breq12d 
 |-  ( w = z -> ( ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( w - ( A ` Z ) ) ) <_ ( ( 1 + r ) x. ( sum^ ` ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) ) ) <-> ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + r ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) ) ) ) ) )
151 150 cbvrabv 
 |-  { w e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( w - ( A ` Z ) ) ) <_ ( ( 1 + r ) x. ( sum^ ` ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) ) ) } = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + r ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( ( x e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ x , ( d ` i ) , x ) ) ) ) ) ` z ) ` ( D ` j ) ) ) ) ) ) }
152 eqid 
 |-  sup ( { w e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( w - ( A ` Z ) ) ) <_ ( ( 1 + r ) x. ( sum^ ` ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) ) ) } , RR , < ) = sup ( { w e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) x. ( w - ( A ` Z ) ) ) <_ ( ( 1 + r ) x. ( sum^ ` ( l e. NN |-> ( ( C ` l ) ( L ` W ) ( ( ( w e. RR |-> ( d e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( d ` i ) , if ( ( d ` i ) <_ w , ( d ` i ) , w ) ) ) ) ) ` w ) ` ( D ` l ) ) ) ) ) ) } , RR , < )
153 10 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> 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 ) ) ) ) ) )
154 11 ad3antrrr 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
155 1 89 90 91 92 5 93 94 104 105 106 108 123 124 125 151 152 153 154 hoidmvlelem4 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR ) /\ r e. RR+ ) -> ( A ( L ` W ) B ) <_ ( ( 1 + r ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )
156 79 87 88 155 syl21anc 
 |-  ( ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) /\ r e. RR+ ) -> ( A ( L ` W ) B ) <_ ( ( 1 + r ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )
157 156 ralrimiva 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> A. r e. RR+ ( A ( L ` W ) B ) <_ ( ( 1 + r ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )
158 nfv 
 |-  F/ r ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
159 46 ad2antrr 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> ( A ( L ` W ) B ) e. RR* )
160 0xr 
 |-  0 e. RR*
161 160 a1i 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> 0 e. RR* )
162 pnfxr 
 |-  +oo e. RR*
163 162 a1i 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> +oo e. RR* )
164 48 ad2antrr 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
165 41 ad2antrr 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
166 ltpnf 
 |-  ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) < +oo )
167 166 adantl 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) < +oo )
168 161 163 164 165 167 elicod 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. ( 0 [,) +oo ) )
169 158 159 168 xralrple2 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> ( ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) <-> A. r e. RR+ ( A ( L ` W ) B ) <_ ( ( 1 + r ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) ) )
170 157 169 mpbird 
 |-  ( ( ( ph /\ A. s e. W ( A ` s ) < ( B ` s ) ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR ) -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
171 61 72 78 170 syl21anc 
 |-  ( ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) /\ -. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) = +oo ) -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
172 60 171 pm2.61dan 
 |-  ( ( ph /\ -. E. s e. W ( B ` s ) <_ ( A ` s ) ) -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
173 43 172 pm2.61dan 
 |-  ( ph -> ( A ( L ` W ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )