Metamath Proof Explorer


Theorem hoidmvlelem2

Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem2.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 ) ) ) ) ) )
hoidmvlelem2.x
|- ( ph -> X e. Fin )
hoidmvlelem2.y
|- ( ph -> Y C_ X )
hoidmvlelem2.z
|- ( ph -> Z e. ( X \ Y ) )
hoidmvlelem2.w
|- W = ( Y u. { Z } )
hoidmvlelem2.a
|- ( ph -> A : W --> RR )
hoidmvlelem2.b
|- ( ph -> B : W --> RR )
hoidmvlelem2.c
|- ( ph -> C : NN --> ( RR ^m W ) )
hoidmvlelem2.f
|- F = ( y e. Y |-> 0 )
hoidmvlelem2.j
|- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
hoidmvlelem2.d
|- ( ph -> D : NN --> ( RR ^m W ) )
hoidmvlelem2.k
|- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
hoidmvlelem2.r
|- ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
hoidmvlelem2.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 ) ) ) ) )
hoidmvlelem2.g
|- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
hoidmvlelem2.e
|- ( ph -> E e. RR+ )
hoidmvlelem2.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 ) ) ) ) ) ) }
hoidmvlelem2.su
|- ( ph -> S e. U )
hoidmvlelem2.sb
|- ( ph -> S < ( B ` Z ) )
hoidmvlelem2.p
|- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
hoidmvlelem2.m
|- ( ph -> M e. NN )
hoidmvlelem2.le
|- ( ph -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) )
hoidmvlelem2.O
|- O = ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )
hoidmvlelem2.v
|- V = ( { ( B ` Z ) } u. O )
hoidmvlelem2.q
|- Q = inf ( V , RR , < )
Assertion hoidmvlelem2
|- ( ph -> E. u e. U S < u )

Proof

Step Hyp Ref Expression
1 hoidmvlelem2.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 hoidmvlelem2.x
 |-  ( ph -> X e. Fin )
3 hoidmvlelem2.y
 |-  ( ph -> Y C_ X )
4 hoidmvlelem2.z
 |-  ( ph -> Z e. ( X \ Y ) )
5 hoidmvlelem2.w
 |-  W = ( Y u. { Z } )
6 hoidmvlelem2.a
 |-  ( ph -> A : W --> RR )
7 hoidmvlelem2.b
 |-  ( ph -> B : W --> RR )
8 hoidmvlelem2.c
 |-  ( ph -> C : NN --> ( RR ^m W ) )
9 hoidmvlelem2.f
 |-  F = ( y e. Y |-> 0 )
10 hoidmvlelem2.j
 |-  J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
11 hoidmvlelem2.d
 |-  ( ph -> D : NN --> ( RR ^m W ) )
12 hoidmvlelem2.k
 |-  K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
13 hoidmvlelem2.r
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
14 hoidmvlelem2.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 ) ) ) ) )
15 hoidmvlelem2.g
 |-  G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
16 hoidmvlelem2.e
 |-  ( ph -> E e. RR+ )
17 hoidmvlelem2.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 ) ) ) ) ) ) }
18 hoidmvlelem2.su
 |-  ( ph -> S e. U )
19 hoidmvlelem2.sb
 |-  ( ph -> S < ( B ` Z ) )
20 hoidmvlelem2.p
 |-  P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
21 hoidmvlelem2.m
 |-  ( ph -> M e. NN )
22 hoidmvlelem2.le
 |-  ( ph -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) )
23 hoidmvlelem2.O
 |-  O = ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )
24 hoidmvlelem2.v
 |-  V = ( { ( B ` Z ) } u. O )
25 hoidmvlelem2.q
 |-  Q = inf ( V , RR , < )
26 snidg
 |-  ( Z e. ( X \ Y ) -> Z e. { Z } )
27 4 26 syl
 |-  ( ph -> Z e. { Z } )
28 elun2
 |-  ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
29 27 28 syl
 |-  ( ph -> Z e. ( Y u. { Z } ) )
30 29 5 eleqtrrdi
 |-  ( ph -> Z e. W )
31 6 30 ffvelrnd
 |-  ( ph -> ( A ` Z ) e. RR )
32 7 30 ffvelrnd
 |-  ( ph -> ( B ` Z ) e. RR )
33 32 snssd
 |-  ( ph -> { ( B ` Z ) } C_ RR )
34 nfv
 |-  F/ i ph
35 eqid
 |-  ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) = ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )
36 simpl
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ph )
37 fz1ssnn
 |-  ( 1 ... M ) C_ NN
38 elrabi
 |-  ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> i e. ( 1 ... M ) )
39 37 38 sselid
 |-  ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> i e. NN )
40 39 adantl
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> i e. NN )
41 eleq1w
 |-  ( j = i -> ( j e. NN <-> i e. NN ) )
42 41 anbi2d
 |-  ( j = i -> ( ( ph /\ j e. NN ) <-> ( ph /\ i e. NN ) ) )
43 fveq2
 |-  ( j = i -> ( D ` j ) = ( D ` i ) )
44 43 fveq1d
 |-  ( j = i -> ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
45 44 eleq1d
 |-  ( j = i -> ( ( ( D ` j ) ` Z ) e. RR <-> ( ( D ` i ) ` Z ) e. RR ) )
46 42 45 imbi12d
 |-  ( j = i -> ( ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR ) <-> ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR ) ) )
47 11 ffvelrnda
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
48 elmapi
 |-  ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
49 47 48 syl
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
50 30 adantr
 |-  ( ( ph /\ j e. NN ) -> Z e. W )
51 49 50 ffvelrnd
 |-  ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR )
52 46 51 chvarvv
 |-  ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR )
53 36 40 52 syl2anc
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( D ` i ) ` Z ) e. RR )
54 34 35 53 rnmptssd
 |-  ( ph -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) C_ RR )
55 23 54 eqsstrid
 |-  ( ph -> O C_ RR )
56 33 55 unssd
 |-  ( ph -> ( { ( B ` Z ) } u. O ) C_ RR )
57 24 56 eqsstrid
 |-  ( ph -> V C_ RR )
58 ltso
 |-  < Or RR
59 58 a1i
 |-  ( ph -> < Or RR )
60 snfi
 |-  { ( B ` Z ) } e. Fin
61 60 a1i
 |-  ( ph -> { ( B ` Z ) } e. Fin )
62 fzfi
 |-  ( 1 ... M ) e. Fin
63 rabfi
 |-  ( ( 1 ... M ) e. Fin -> { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin )
64 62 63 ax-mp
 |-  { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin
65 64 a1i
 |-  ( ph -> { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin )
66 35 rnmptfi
 |-  ( { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) e. Fin )
67 65 66 syl
 |-  ( ph -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) e. Fin )
68 23 67 eqeltrid
 |-  ( ph -> O e. Fin )
69 unfi
 |-  ( ( { ( B ` Z ) } e. Fin /\ O e. Fin ) -> ( { ( B ` Z ) } u. O ) e. Fin )
70 61 68 69 syl2anc
 |-  ( ph -> ( { ( B ` Z ) } u. O ) e. Fin )
71 24 70 eqeltrid
 |-  ( ph -> V e. Fin )
72 fvex
 |-  ( B ` Z ) e. _V
73 72 snid
 |-  ( B ` Z ) e. { ( B ` Z ) }
74 elun1
 |-  ( ( B ` Z ) e. { ( B ` Z ) } -> ( B ` Z ) e. ( { ( B ` Z ) } u. O ) )
75 73 74 ax-mp
 |-  ( B ` Z ) e. ( { ( B ` Z ) } u. O )
76 24 eqcomi
 |-  ( { ( B ` Z ) } u. O ) = V
77 75 76 eleqtri
 |-  ( B ` Z ) e. V
78 77 a1i
 |-  ( ph -> ( B ` Z ) e. V )
79 ne0i
 |-  ( ( B ` Z ) e. V -> V =/= (/) )
80 78 79 syl
 |-  ( ph -> V =/= (/) )
81 fiinfcl
 |-  ( ( < Or RR /\ ( V e. Fin /\ V =/= (/) /\ V C_ RR ) ) -> inf ( V , RR , < ) e. V )
82 59 71 80 57 81 syl13anc
 |-  ( ph -> inf ( V , RR , < ) e. V )
83 25 82 eqeltrid
 |-  ( ph -> Q e. V )
84 57 83 sseldd
 |-  ( ph -> Q e. RR )
85 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 ) )
86 17 85 eqsstri
 |-  U C_ ( ( A ` Z ) [,] ( B ` Z ) )
87 86 a1i
 |-  ( ph -> U C_ ( ( A ` Z ) [,] ( B ` Z ) ) )
88 31 32 iccssred
 |-  ( ph -> ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR )
89 87 88 sstrd
 |-  ( ph -> U C_ RR )
90 89 18 sseldd
 |-  ( ph -> S e. RR )
91 31 rexrd
 |-  ( ph -> ( A ` Z ) e. RR* )
92 32 rexrd
 |-  ( ph -> ( B ` Z ) e. RR* )
93 86 18 sselid
 |-  ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) )
94 iccgelb
 |-  ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ S e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> ( A ` Z ) <_ S )
95 91 92 93 94 syl3anc
 |-  ( ph -> ( A ` Z ) <_ S )
96 19 adantr
 |-  ( ( ph /\ x = ( B ` Z ) ) -> S < ( B ` Z ) )
97 id
 |-  ( x = ( B ` Z ) -> x = ( B ` Z ) )
98 97 eqcomd
 |-  ( x = ( B ` Z ) -> ( B ` Z ) = x )
99 98 adantl
 |-  ( ( ph /\ x = ( B ` Z ) ) -> ( B ` Z ) = x )
100 96 99 breqtrd
 |-  ( ( ph /\ x = ( B ` Z ) ) -> S < x )
101 100 adantlr
 |-  ( ( ( ph /\ x e. V ) /\ x = ( B ` Z ) ) -> S < x )
102 simpll
 |-  ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> ph )
103 id
 |-  ( x e. V -> x e. V )
104 103 24 eleqtrdi
 |-  ( x e. V -> x e. ( { ( B ` Z ) } u. O ) )
105 104 adantr
 |-  ( ( x e. V /\ -. x = ( B ` Z ) ) -> x e. ( { ( B ` Z ) } u. O ) )
106 elsni
 |-  ( x e. { ( B ` Z ) } -> x = ( B ` Z ) )
107 106 con3i
 |-  ( -. x = ( B ` Z ) -> -. x e. { ( B ` Z ) } )
108 107 adantl
 |-  ( ( x e. V /\ -. x = ( B ` Z ) ) -> -. x e. { ( B ` Z ) } )
109 elunnel1
 |-  ( ( x e. ( { ( B ` Z ) } u. O ) /\ -. x e. { ( B ` Z ) } ) -> x e. O )
110 105 108 109 syl2anc
 |-  ( ( x e. V /\ -. x = ( B ` Z ) ) -> x e. O )
111 110 adantll
 |-  ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> x e. O )
112 id
 |-  ( x e. O -> x e. O )
113 112 23 eleqtrdi
 |-  ( x e. O -> x e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) )
114 vex
 |-  x e. _V
115 35 elrnmpt
 |-  ( x e. _V -> ( x e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) <-> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) ) )
116 114 115 ax-mp
 |-  ( x e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) <-> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
117 113 116 sylib
 |-  ( x e. O -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
118 117 adantl
 |-  ( ( ph /\ x e. O ) -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
119 fveq2
 |-  ( j = i -> ( C ` j ) = ( C ` i ) )
120 119 fveq1d
 |-  ( j = i -> ( ( C ` j ) ` Z ) = ( ( C ` i ) ` Z ) )
121 120 eleq1d
 |-  ( j = i -> ( ( ( C ` j ) ` Z ) e. RR <-> ( ( C ` i ) ` Z ) e. RR ) )
122 42 121 imbi12d
 |-  ( j = i -> ( ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR ) <-> ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR ) ) )
123 8 ffvelrnda
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
124 elmapi
 |-  ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
125 123 124 syl
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
126 125 50 ffvelrnd
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR )
127 122 126 chvarvv
 |-  ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR )
128 127 rexrd
 |-  ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR* )
129 36 40 128 syl2anc
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( C ` i ) ` Z ) e. RR* )
130 52 rexrd
 |-  ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR* )
131 36 40 130 syl2anc
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( D ` i ) ` Z ) e. RR* )
132 120 44 oveq12d
 |-  ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
133 132 eleq2d
 |-  ( j = i -> ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
134 133 elrab
 |-  ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } <-> ( i e. ( 1 ... M ) /\ S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
135 134 biimpi
 |-  ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( i e. ( 1 ... M ) /\ S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
136 135 simprd
 |-  ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
137 136 adantl
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
138 icoltub
 |-  ( ( ( ( C ` i ) ` Z ) e. RR* /\ ( ( D ` i ) ` Z ) e. RR* /\ S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) -> S < ( ( D ` i ) ` Z ) )
139 129 131 137 138 syl3anc
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> S < ( ( D ` i ) ` Z ) )
140 139 3adant3
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> S < ( ( D ` i ) ` Z ) )
141 id
 |-  ( x = ( ( D ` i ) ` Z ) -> x = ( ( D ` i ) ` Z ) )
142 141 eqcomd
 |-  ( x = ( ( D ` i ) ` Z ) -> ( ( D ` i ) ` Z ) = x )
143 142 3ad2ant3
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> ( ( D ` i ) ` Z ) = x )
144 140 143 breqtrd
 |-  ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> S < x )
145 144 3exp
 |-  ( ph -> ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( x = ( ( D ` i ) ` Z ) -> S < x ) ) )
146 145 adantr
 |-  ( ( ph /\ x e. O ) -> ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( x = ( ( D ` i ) ` Z ) -> S < x ) ) )
147 146 rexlimdv
 |-  ( ( ph /\ x e. O ) -> ( E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) -> S < x ) )
148 118 147 mpd
 |-  ( ( ph /\ x e. O ) -> S < x )
149 102 111 148 syl2anc
 |-  ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> S < x )
150 101 149 pm2.61dan
 |-  ( ( ph /\ x e. V ) -> S < x )
151 150 ralrimiva
 |-  ( ph -> A. x e. V S < x )
152 breq2
 |-  ( x = inf ( V , RR , < ) -> ( S < x <-> S < inf ( V , RR , < ) ) )
153 152 rspcva
 |-  ( ( inf ( V , RR , < ) e. V /\ A. x e. V S < x ) -> S < inf ( V , RR , < ) )
154 82 151 153 syl2anc
 |-  ( ph -> S < inf ( V , RR , < ) )
155 25 eqcomi
 |-  inf ( V , RR , < ) = Q
156 155 a1i
 |-  ( ph -> inf ( V , RR , < ) = Q )
157 154 156 breqtrd
 |-  ( ph -> S < Q )
158 31 90 84 95 157 lelttrd
 |-  ( ph -> ( A ` Z ) < Q )
159 31 84 158 ltled
 |-  ( ph -> ( A ` Z ) <_ Q )
160 fiminre
 |-  ( ( V C_ RR /\ V e. Fin /\ V =/= (/) ) -> E. x e. V A. y e. V x <_ y )
161 57 71 80 160 syl3anc
 |-  ( ph -> E. x e. V A. y e. V x <_ y )
162 lbinfle
 |-  ( ( V C_ RR /\ E. x e. V A. y e. V x <_ y /\ ( B ` Z ) e. V ) -> inf ( V , RR , < ) <_ ( B ` Z ) )
163 57 161 78 162 syl3anc
 |-  ( ph -> inf ( V , RR , < ) <_ ( B ` Z ) )
164 25 163 eqbrtrid
 |-  ( ph -> Q <_ ( B ` Z ) )
165 31 32 84 159 164 eliccd
 |-  ( ph -> Q e. ( ( A ` Z ) [,] ( B ` Z ) ) )
166 84 recnd
 |-  ( ph -> Q e. CC )
167 90 recnd
 |-  ( ph -> S e. CC )
168 31 recnd
 |-  ( ph -> ( A ` Z ) e. CC )
169 166 167 168 npncand
 |-  ( ph -> ( ( Q - S ) + ( S - ( A ` Z ) ) ) = ( Q - ( A ` Z ) ) )
170 169 eqcomd
 |-  ( ph -> ( Q - ( A ` Z ) ) = ( ( Q - S ) + ( S - ( A ` Z ) ) ) )
171 170 oveq2d
 |-  ( ph -> ( G x. ( Q - ( A ` Z ) ) ) = ( G x. ( ( Q - S ) + ( S - ( A ` Z ) ) ) ) )
172 rge0ssre
 |-  ( 0 [,) +oo ) C_ RR
173 2 3 ssfid
 |-  ( ph -> Y e. Fin )
174 ssun1
 |-  Y C_ ( Y u. { Z } )
175 174 5 sseqtrri
 |-  Y C_ W
176 175 a1i
 |-  ( ph -> Y C_ W )
177 6 176 fssresd
 |-  ( ph -> ( A |` Y ) : Y --> RR )
178 7 176 fssresd
 |-  ( ph -> ( B |` Y ) : Y --> RR )
179 1 173 177 178 hoidmvcl
 |-  ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. ( 0 [,) +oo ) )
180 15 179 eqeltrid
 |-  ( ph -> G e. ( 0 [,) +oo ) )
181 172 180 sselid
 |-  ( ph -> G e. RR )
182 181 recnd
 |-  ( ph -> G e. CC )
183 166 167 subcld
 |-  ( ph -> ( Q - S ) e. CC )
184 167 168 subcld
 |-  ( ph -> ( S - ( A ` Z ) ) e. CC )
185 182 183 184 adddid
 |-  ( ph -> ( G x. ( ( Q - S ) + ( S - ( A ` Z ) ) ) ) = ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) )
186 182 183 mulcld
 |-  ( ph -> ( G x. ( Q - S ) ) e. CC )
187 182 184 mulcld
 |-  ( ph -> ( G x. ( S - ( A ` Z ) ) ) e. CC )
188 186 187 addcomd
 |-  ( ph -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) = ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) )
189 171 185 188 3eqtrd
 |-  ( ph -> ( G x. ( Q - ( A ` Z ) ) ) = ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) )
190 84 90 jca
 |-  ( ph -> ( Q e. RR /\ S e. RR ) )
191 resubcl
 |-  ( ( Q e. RR /\ S e. RR ) -> ( Q - S ) e. RR )
192 190 191 syl
 |-  ( ph -> ( Q - S ) e. RR )
193 181 192 jca
 |-  ( ph -> ( G e. RR /\ ( Q - S ) e. RR ) )
194 remulcl
 |-  ( ( G e. RR /\ ( Q - S ) e. RR ) -> ( G x. ( Q - S ) ) e. RR )
195 193 194 syl
 |-  ( ph -> ( G x. ( Q - S ) ) e. RR )
196 90 31 jca
 |-  ( ph -> ( S e. RR /\ ( A ` Z ) e. RR ) )
197 resubcl
 |-  ( ( S e. RR /\ ( A ` Z ) e. RR ) -> ( S - ( A ` Z ) ) e. RR )
198 196 197 syl
 |-  ( ph -> ( S - ( A ` Z ) ) e. RR )
199 181 198 jca
 |-  ( ph -> ( G e. RR /\ ( S - ( A ` Z ) ) e. RR ) )
200 remulcl
 |-  ( ( G e. RR /\ ( S - ( A ` Z ) ) e. RR ) -> ( G x. ( S - ( A ` Z ) ) ) e. RR )
201 199 200 syl
 |-  ( ph -> ( G x. ( S - ( A ` Z ) ) ) e. RR )
202 195 201 jca
 |-  ( ph -> ( ( G x. ( Q - S ) ) e. RR /\ ( G x. ( S - ( A ` Z ) ) ) e. RR ) )
203 readdcl
 |-  ( ( ( G x. ( Q - S ) ) e. RR /\ ( G x. ( S - ( A ` Z ) ) ) e. RR ) -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) e. RR )
204 202 203 syl
 |-  ( ph -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) e. RR )
205 188 204 eqeltrrd
 |-  ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) e. RR )
206 1red
 |-  ( ph -> 1 e. RR )
207 16 rpred
 |-  ( ph -> E e. RR )
208 206 207 readdcld
 |-  ( ph -> ( 1 + E ) e. RR )
209 4 eldifbd
 |-  ( ph -> -. Z e. Y )
210 30 209 eldifd
 |-  ( ph -> Z e. ( W \ Y ) )
211 1 173 210 5 8 11 13 14 90 sge0hsphoire
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
212 208 211 remulcld
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
213 fzfid
 |-  ( ph -> ( 1 ... M ) e. Fin )
214 192 adantr
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - S ) e. RR )
215 simpl
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ph )
216 elfznn
 |-  ( j e. ( 1 ... M ) -> j e. NN )
217 216 adantl
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> j e. NN )
218 id
 |-  ( j e. NN -> j e. NN )
219 ovexd
 |-  ( j e. NN -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V )
220 20 fvmpt2
 |-  ( ( j e. NN /\ ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
221 218 219 220 syl2anc
 |-  ( j e. NN -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
222 221 adantl
 |-  ( ( ph /\ j e. NN ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
223 173 adantr
 |-  ( ( ph /\ j e. NN ) -> Y e. Fin )
224 175 a1i
 |-  ( ( ph /\ j e. NN ) -> Y C_ W )
225 125 224 fssresd
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) |` Y ) : Y --> RR )
226 225 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) |` Y ) : Y --> RR )
227 iftrue
 |-  ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
228 227 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
229 228 feq1d
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR <-> ( ( C ` j ) |` Y ) : Y --> RR ) )
230 226 229 mpbird
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
231 0red
 |-  ( ( ph /\ y e. Y ) -> 0 e. RR )
232 231 9 fmptd
 |-  ( ph -> F : Y --> RR )
233 232 ad2antrr
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F : Y --> RR )
234 iffalse
 |-  ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
235 234 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
236 235 feq1d
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR <-> F : Y --> RR ) )
237 233 236 mpbird
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
238 230 237 pm2.61dan
 |-  ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
239 simpr
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
240 fvex
 |-  ( C ` j ) e. _V
241 240 resex
 |-  ( ( C ` j ) |` Y ) e. _V
242 241 a1i
 |-  ( ph -> ( ( C ` j ) |` Y ) e. _V )
243 2 3 ssexd
 |-  ( ph -> Y e. _V )
244 mptexg
 |-  ( Y e. _V -> ( y e. Y |-> 0 ) e. _V )
245 243 244 syl
 |-  ( ph -> ( y e. Y |-> 0 ) e. _V )
246 9 245 eqeltrid
 |-  ( ph -> F e. _V )
247 242 246 ifcld
 |-  ( ph -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
248 247 adantr
 |-  ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
249 10 fvmpt2
 |-  ( ( j e. NN /\ if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
250 239 248 249 syl2anc
 |-  ( ( ph /\ j e. NN ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
251 250 feq1d
 |-  ( ( ph /\ j e. NN ) -> ( ( J ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR ) )
252 238 251 mpbird
 |-  ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR )
253 49 224 fssresd
 |-  ( ( ph /\ j e. NN ) -> ( ( D ` j ) |` Y ) : Y --> RR )
254 253 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( D ` j ) |` Y ) : Y --> RR )
255 iftrue
 |-  ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
256 255 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
257 256 feq1d
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR <-> ( ( D ` j ) |` Y ) : Y --> RR ) )
258 254 257 mpbird
 |-  ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR )
259 iffalse
 |-  ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = F )
260 259 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = F )
261 260 feq1d
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR <-> F : Y --> RR ) )
262 233 261 mpbird
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR )
263 258 262 pm2.61dan
 |-  ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR )
264 fvex
 |-  ( D ` j ) e. _V
265 264 resex
 |-  ( ( D ` j ) |` Y ) e. _V
266 265 a1i
 |-  ( ph -> ( ( D ` j ) |` Y ) e. _V )
267 266 246 ifcld
 |-  ( ph -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
268 267 adantr
 |-  ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
269 12 fvmpt2
 |-  ( ( j e. NN /\ if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
270 239 268 269 syl2anc
 |-  ( ( ph /\ j e. NN ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
271 270 feq1d
 |-  ( ( ph /\ j e. NN ) -> ( ( K ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR ) )
272 263 271 mpbird
 |-  ( ( ph /\ j e. NN ) -> ( K ` j ) : Y --> RR )
273 1 223 252 272 hoidmvcl
 |-  ( ( ph /\ j e. NN ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. ( 0 [,) +oo ) )
274 222 273 eqeltrd
 |-  ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) )
275 172 274 sselid
 |-  ( ( ph /\ j e. NN ) -> ( P ` j ) e. RR )
276 215 217 275 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( P ` j ) e. RR )
277 214 276 remulcld
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( Q - S ) x. ( P ` j ) ) e. RR )
278 213 277 fsumrecl
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) e. RR )
279 208 278 remulcld
 |-  ( ph -> ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
280 212 279 readdcld
 |-  ( ph -> ( ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) e. RR )
281 1 173 210 5 8 11 13 14 84 sge0hsphoire
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR )
282 208 281 remulcld
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) e. RR )
283 18 17 eleqtrdi
 |-  ( ph -> S 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 ) ) ) ) ) ) } )
284 oveq1
 |-  ( z = S -> ( z - ( A ` Z ) ) = ( S - ( A ` Z ) ) )
285 284 oveq2d
 |-  ( z = S -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( S - ( A ` Z ) ) ) )
286 fveq2
 |-  ( z = S -> ( H ` z ) = ( H ` S ) )
287 286 fveq1d
 |-  ( z = S -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` S ) ` ( D ` j ) ) )
288 287 oveq2d
 |-  ( z = S -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
289 288 mpteq2dv
 |-  ( z = S -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) )
290 289 fveq2d
 |-  ( z = S -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) )
291 290 oveq2d
 |-  ( z = S -> ( ( 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 ` S ) ` ( D ` j ) ) ) ) ) ) )
292 285 291 breq12d
 |-  ( z = S -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
293 292 elrab
 |-  ( S 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. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
294 283 293 sylib
 |-  ( ph -> ( S e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
295 294 simprd
 |-  ( ph -> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
296 213 276 fsumrecl
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( P ` j ) e. RR )
297 208 296 remulcld
 |-  ( ph -> ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) e. RR )
298 0red
 |-  ( ph -> 0 e. RR )
299 90 84 posdifd
 |-  ( ph -> ( S < Q <-> 0 < ( Q - S ) ) )
300 157 299 mpbid
 |-  ( ph -> 0 < ( Q - S ) )
301 298 192 300 ltled
 |-  ( ph -> 0 <_ ( Q - S ) )
302 181 297 192 301 22 lemul1ad
 |-  ( ph -> ( G x. ( Q - S ) ) <_ ( ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) x. ( Q - S ) ) )
303 208 recnd
 |-  ( ph -> ( 1 + E ) e. CC )
304 296 recnd
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( P ` j ) e. CC )
305 303 304 183 mulassd
 |-  ( ph -> ( ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) x. ( Q - S ) ) = ( ( 1 + E ) x. ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) ) )
306 276 recnd
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( P ` j ) e. CC )
307 213 183 306 fsummulc1
 |-  ( ph -> ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( P ` j ) x. ( Q - S ) ) )
308 183 adantr
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - S ) e. CC )
309 306 308 mulcomd
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( P ` j ) x. ( Q - S ) ) = ( ( Q - S ) x. ( P ` j ) ) )
310 309 sumeq2dv
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) )
311 307 310 eqtrd
 |-  ( ph -> ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) )
312 311 oveq2d
 |-  ( ph -> ( ( 1 + E ) x. ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) ) = ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
313 305 312 eqtrd
 |-  ( ph -> ( ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) x. ( Q - S ) ) = ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
314 302 313 breqtrd
 |-  ( ph -> ( G x. ( Q - S ) ) <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
315 201 195 212 279 295 314 leadd12dd
 |-  ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) <_ ( ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
316 nnsplit
 |-  ( M e. NN -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
317 21 316 syl
 |-  ( ph -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
318 uncom
 |-  ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) )
319 318 a1i
 |-  ( ph -> ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) )
320 317 319 eqtr2d
 |-  ( ph -> ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) = NN )
321 320 eqcomd
 |-  ( ph -> NN = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) )
322 321 mpteq1d
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) = ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) )
323 322 fveq2d
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) )
324 nfv
 |-  F/ j ph
325 fvexd
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) e. _V )
326 ovexd
 |-  ( ph -> ( 1 ... M ) e. _V )
327 incom
 |-  ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = ( ( 1 ... M ) i^i ( ZZ>= ` ( M + 1 ) ) )
328 nnuzdisj
 |-  ( ( 1 ... M ) i^i ( ZZ>= ` ( M + 1 ) ) ) = (/)
329 327 328 eqtri
 |-  ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = (/)
330 329 a1i
 |-  ( ph -> ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = (/) )
331 icossicc
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
332 ssid
 |-  ( 0 [,) +oo ) C_ ( 0 [,) +oo )
333 simpl
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ph )
334 21 peano2nnd
 |-  ( ph -> ( M + 1 ) e. NN )
335 uznnssnn
 |-  ( ( M + 1 ) e. NN -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
336 334 335 syl
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
337 336 adantr
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
338 simpr
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. ( ZZ>= ` ( M + 1 ) ) )
339 337 338 sseldd
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. NN )
340 snfi
 |-  { Z } e. Fin
341 340 a1i
 |-  ( ph -> { Z } e. Fin )
342 unfi
 |-  ( ( Y e. Fin /\ { Z } e. Fin ) -> ( Y u. { Z } ) e. Fin )
343 173 341 342 syl2anc
 |-  ( ph -> ( Y u. { Z } ) e. Fin )
344 5 343 eqeltrid
 |-  ( ph -> W e. Fin )
345 344 adantr
 |-  ( ( ph /\ j e. NN ) -> W e. Fin )
346 eleq1w
 |-  ( j = l -> ( j e. Y <-> l e. Y ) )
347 fveq2
 |-  ( j = l -> ( c ` j ) = ( c ` l ) )
348 347 breq1d
 |-  ( j = l -> ( ( c ` j ) <_ x <-> ( c ` l ) <_ x ) )
349 348 347 ifbieq1d
 |-  ( j = l -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` l ) <_ x , ( c ` l ) , x ) )
350 346 347 349 ifbieq12d
 |-  ( j = l -> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) = if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) )
351 350 cbvmptv
 |-  ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) = ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) )
352 351 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 ) |-> ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) ) )
353 352 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 ) |-> ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) ) ) )
354 14 353 eqtri
 |-  H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) ) ) )
355 90 adantr
 |-  ( ( ph /\ j e. NN ) -> S e. RR )
356 354 355 345 49 hsphoif
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` S ) ` ( D ` j ) ) : W --> RR )
357 1 345 125 356 hoidmvcl
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
358 333 339 357 syl2anc
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
359 332 358 sselid
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
360 331 359 sselid
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
361 215 217 357 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
362 331 361 sselid
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
363 324 325 326 330 360 362 sge0splitmpt
 |-  ( ph -> ( sum^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
364 nnex
 |-  NN e. _V
365 364 a1i
 |-  ( ph -> NN e. _V )
366 331 357 sselid
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
367 324 365 366 211 336 sge0ssrempt
 |-  ( ph -> ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
368 37 a1i
 |-  ( ph -> ( 1 ... M ) C_ NN )
369 324 365 366 211 368 sge0ssrempt
 |-  ( ph -> ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
370 rexadd
 |-  ( ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR /\ ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR ) -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
371 367 369 370 syl2anc
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
372 323 363 371 3eqtrd
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
373 372 oveq2d
 |-  ( ph -> ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
374 373 oveq1d
 |-  ( ph -> ( ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( ( 1 + E ) x. ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
375 372 211 eqeltrrd
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
376 375 recnd
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. CC )
377 278 recnd
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) e. CC )
378 303 376 377 adddid
 |-  ( ph -> ( ( 1 + E ) x. ( ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( ( 1 + E ) x. ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
379 378 eqcomd
 |-  ( ph -> ( ( ( 1 + E ) x. ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( 1 + E ) x. ( ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
380 367 recnd
 |-  ( ph -> ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. CC )
381 369 recnd
 |-  ( ph -> ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. CC )
382 380 381 377 addassd
 |-  ( ph -> ( ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
383 213 361 sge0fsummpt
 |-  ( ph -> ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
384 383 oveq1d
 |-  ( ph -> ( ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = ( sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
385 ax-resscn
 |-  RR C_ CC
386 172 385 sstri
 |-  ( 0 [,) +oo ) C_ CC
387 386 357 sselid
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. CC )
388 215 217 387 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. CC )
389 192 adantr
 |-  ( ( ph /\ j e. NN ) -> ( Q - S ) e. RR )
390 389 275 remulcld
 |-  ( ( ph /\ j e. NN ) -> ( ( Q - S ) x. ( P ` j ) ) e. RR )
391 390 recnd
 |-  ( ( ph /\ j e. NN ) -> ( ( Q - S ) x. ( P ` j ) ) e. CC )
392 217 391 syldan
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( Q - S ) x. ( P ` j ) ) e. CC )
393 213 388 392 fsumadd
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
394 393 eqcomd
 |-  ( ph -> ( sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) )
395 384 394 eqtrd
 |-  ( ph -> ( ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) )
396 395 oveq2d
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) )
397 382 396 eqtrd
 |-  ( ph -> ( ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) )
398 397 oveq2d
 |-  ( ph -> ( ( 1 + E ) x. ( ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( 1 + E ) x. ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) ) )
399 374 379 398 3eqtrd
 |-  ( ph -> ( ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( 1 + E ) x. ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) ) )
400 172 357 sselid
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. RR )
401 400 390 readdcld
 |-  ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
402 215 217 401 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
403 213 402 fsumrecl
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
404 367 403 readdcld
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) e. RR )
405 0le1
 |-  0 <_ 1
406 405 a1i
 |-  ( ph -> 0 <_ 1 )
407 16 rpge0d
 |-  ( ph -> 0 <_ E )
408 206 207 406 407 addge0d
 |-  ( ph -> 0 <_ ( 1 + E ) )
409 84 adantr
 |-  ( ( ph /\ j e. NN ) -> Q e. RR )
410 354 409 345 49 hsphoif
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` Q ) ` ( D ` j ) ) : W --> RR )
411 1 345 125 410 hoidmvcl
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
412 331 411 sselid
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
413 324 365 412 281 336 sge0ssrempt
 |-  ( ph -> ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR )
414 172 411 sselid
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. RR )
415 215 217 414 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. RR )
416 213 415 fsumrecl
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. RR )
417 333 339 412 syl2anc
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
418 210 adantr
 |-  ( ( ph /\ j e. NN ) -> Z e. ( W \ Y ) )
419 90 84 157 ltled
 |-  ( ph -> S <_ Q )
420 419 adantr
 |-  ( ( ph /\ j e. NN ) -> S <_ Q )
421 1 345 418 5 355 409 420 354 125 49 hsphoidmvle2
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
422 333 339 421 syl2anc
 |-  ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
423 324 325 360 417 422 sge0lempt
 |-  ( ph -> ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) <_ ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
424 215 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) = 0 ) -> ph )
425 217 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) = 0 ) -> j e. NN )
426 simpr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) = 0 ) -> ( P ` j ) = 0 )
427 oveq2
 |-  ( ( P ` j ) = 0 -> ( ( Q - S ) x. ( P ` j ) ) = ( ( Q - S ) x. 0 ) )
428 427 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( Q - S ) x. ( P ` j ) ) = ( ( Q - S ) x. 0 ) )
429 183 mul01d
 |-  ( ph -> ( ( Q - S ) x. 0 ) = 0 )
430 429 ad2antrr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( Q - S ) x. 0 ) = 0 )
431 428 430 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( Q - S ) x. ( P ` j ) ) = 0 )
432 431 oveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + 0 ) )
433 387 addid1d
 |-  ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + 0 ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
434 433 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + 0 ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
435 432 434 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
436 421 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
437 435 436 eqbrtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
438 424 425 426 437 syl21anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) = 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
439 simpl
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( P ` j ) = 0 ) -> ( ph /\ j e. ( 1 ... M ) ) )
440 neqne
 |-  ( -. ( P ` j ) = 0 -> ( P ` j ) =/= 0 )
441 440 adantl
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( P ` j ) = 0 ) -> ( P ` j ) =/= 0 )
442 402 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
443 215 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ph )
444 217 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> j e. NN )
445 simpr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( P ` j ) =/= 0 )
446 4 adantr
 |-  ( ( ph /\ j e. NN ) -> Z e. ( X \ Y ) )
447 209 adantr
 |-  ( ( ph /\ j e. NN ) -> -. Z e. Y )
448 eqid
 |-  prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) )
449 1 223 446 447 5 125 356 448 hoiprodp1
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) = ( prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) x. ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) ) ) )
450 449 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) = ( prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) x. ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) ) ) )
451 222 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
452 223 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> Y e. Fin )
453 222 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
454 fveq2
 |-  ( Y = (/) -> ( L ` Y ) = ( L ` (/) ) )
455 454 oveqd
 |-  ( Y = (/) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` j ) ( L ` (/) ) ( K ` j ) ) )
456 455 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` j ) ( L ` (/) ) ( K ` j ) ) )
457 252 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( J ` j ) : Y --> RR )
458 id
 |-  ( Y = (/) -> Y = (/) )
459 458 eqcomd
 |-  ( Y = (/) -> (/) = Y )
460 459 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> (/) = Y )
461 460 feq2d
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( J ` j ) : (/) --> RR <-> ( J ` j ) : Y --> RR ) )
462 457 461 mpbird
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( J ` j ) : (/) --> RR )
463 272 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( K ` j ) : Y --> RR )
464 460 feq2d
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( K ` j ) : (/) --> RR <-> ( K ` j ) : Y --> RR ) )
465 463 464 mpbird
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( K ` j ) : (/) --> RR )
466 1 462 465 hoidmv0val
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( J ` j ) ( L ` (/) ) ( K ` j ) ) = 0 )
467 453 456 466 3eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( P ` j ) = 0 )
468 467 adantlr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ Y = (/) ) -> ( P ` j ) = 0 )
469 neneq
 |-  ( ( P ` j ) =/= 0 -> -. ( P ` j ) = 0 )
470 469 ad2antlr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ Y = (/) ) -> -. ( P ` j ) = 0 )
471 468 470 pm2.65da
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> -. Y = (/) )
472 471 neqned
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> Y =/= (/) )
473 252 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( J ` j ) : Y --> RR )
474 272 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( K ` j ) : Y --> RR )
475 1 452 472 473 474 hoidmvn0val
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = prod_ k e. Y ( vol ` ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) )
476 250 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
477 222 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
478 250 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
479 478 235 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( J ` j ) = F )
480 270 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
481 480 260 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( K ` j ) = F )
482 479 481 oveq12d
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( F ( L ` Y ) F ) )
483 1 173 232 hoidmvval0b
 |-  ( ph -> ( F ( L ` Y ) F ) = 0 )
484 483 ad2antrr
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( F ( L ` Y ) F ) = 0 )
485 477 482 484 3eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( P ` j ) = 0 )
486 485 adantlr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( P ` j ) = 0 )
487 469 ad2antlr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> -. ( P ` j ) = 0 )
488 486 487 condan
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
489 488 iftrued
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
490 476 489 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( J ` j ) = ( ( C ` j ) |` Y ) )
491 490 fveq1d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( J ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
492 491 adantr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( J ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
493 fvres
 |-  ( k e. Y -> ( ( ( C ` j ) |` Y ) ` k ) = ( ( C ` j ) ` k ) )
494 493 adantl
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( ( C ` j ) |` Y ) ` k ) = ( ( C ` j ) ` k ) )
495 492 494 eqtrd
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( J ` j ) ` k ) = ( ( C ` j ) ` k ) )
496 270 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
497 488 255 syl
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
498 496 497 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( K ` j ) = ( ( D ` j ) |` Y ) )
499 498 fveq1d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( K ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
500 499 adantr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( K ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
501 fvres
 |-  ( k e. Y -> ( ( ( D ` j ) |` Y ) ` k ) = ( ( D ` j ) ` k ) )
502 501 adantl
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( ( D ` j ) |` Y ) ` k ) = ( ( D ` j ) ` k ) )
503 500 502 eqtrd
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( K ` j ) ` k ) = ( ( D ` j ) ` k ) )
504 495 503 oveq12d
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
505 504 fveq2d
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( vol ` ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) = ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
506 505 prodeq2dv
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> prod_ k e. Y ( vol ` ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
507 475 506 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
508 355 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> S e. RR )
509 345 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> W e. Fin )
510 49 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( D ` j ) : W --> RR )
511 elun1
 |-  ( k e. Y -> k e. ( Y u. { Z } ) )
512 511 5 eleqtrrdi
 |-  ( k e. Y -> k e. W )
513 512 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> k e. W )
514 354 508 509 510 513 hsphoival
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( H ` S ) ` ( D ` j ) ) ` k ) = if ( k e. Y , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ S , ( ( D ` j ) ` k ) , S ) ) )
515 iftrue
 |-  ( k e. Y -> if ( k e. Y , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ S , ( ( D ` j ) ` k ) , S ) ) = ( ( D ` j ) ` k ) )
516 515 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> if ( k e. Y , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ S , ( ( D ` j ) ` k ) , S ) ) = ( ( D ` j ) ` k ) )
517 514 516 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( H ` S ) ` ( D ` j ) ) ` k ) = ( ( D ` j ) ` k ) )
518 517 oveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
519 518 fveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) = ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
520 519 prodeq2dv
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
521 520 eqcomd
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) )
522 521 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) )
523 451 507 522 3eqtrrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) = ( P ` j ) )
524 354 355 345 49 50 hsphoival
 |-  ( ( ph /\ j e. NN ) -> ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) = if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) ) )
525 209 iffalsed
 |-  ( ph -> if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) ) = if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) )
526 525 adantr
 |-  ( ( ph /\ j e. NN ) -> if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) ) = if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) )
527 524 526 eqtrd
 |-  ( ( ph /\ j e. NN ) -> ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) = if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) )
528 527 oveq2d
 |-  ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) ) )
529 528 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) ) )
530 126 rexrd
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR* )
531 530 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) e. RR* )
532 51 rexrd
 |-  ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR* )
533 532 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. RR* )
534 icoltub
 |-  ( ( ( ( C ` j ) ` Z ) e. RR* /\ ( ( D ` j ) ` Z ) e. RR* /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> S < ( ( D ` j ) ` Z ) )
535 531 533 488 534 syl3anc
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> S < ( ( D ` j ) ` Z ) )
536 355 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> S e. RR )
537 51 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. RR )
538 536 537 ltnled
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( S < ( ( D ` j ) ` Z ) <-> -. ( ( D ` j ) ` Z ) <_ S ) )
539 535 538 mpbid
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> -. ( ( D ` j ) ` Z ) <_ S )
540 539 iffalsed
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) = S )
541 540 oveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ` Z ) [,) if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) ) = ( ( ( C ` j ) ` Z ) [,) S ) )
542 529 541 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) S ) )
543 542 fveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) S ) ) )
544 volico
 |-  ( ( ( ( C ` j ) ` Z ) e. RR /\ S e. RR ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) S ) ) = if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) )
545 126 536 544 syl2an
 |-  ( ( ( ph /\ j e. NN ) /\ ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) S ) ) = if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) )
546 545 anabss5
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) S ) ) = if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) )
547 iftrue
 |-  ( ( ( C ` j ) ` Z ) < S -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = ( S - ( ( C ` j ) ` Z ) ) )
548 547 adantl
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ ( ( C ` j ) ` Z ) < S ) -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = ( S - ( ( C ` j ) ` Z ) ) )
549 iffalse
 |-  ( -. ( ( C ` j ) ` Z ) < S -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = 0 )
550 549 adantl
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = 0 )
551 simpll
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ph /\ j e. NN ) )
552 icogelb
 |-  ( ( ( ( C ` j ) ` Z ) e. RR* /\ ( ( D ` j ) ` Z ) e. RR* /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) ` Z ) <_ S )
553 531 533 488 552 syl3anc
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) <_ S )
554 553 adantr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( C ` j ) ` Z ) <_ S )
555 simpr
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> -. ( ( C ` j ) ` Z ) < S )
556 554 555 jca
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( ( C ` j ) ` Z ) <_ S /\ -. ( ( C ` j ) ` Z ) < S ) )
557 551 126 syl
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( C ` j ) ` Z ) e. RR )
558 551 355 syl
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> S e. RR )
559 557 558 eqleltd
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( ( C ` j ) ` Z ) = S <-> ( ( ( C ` j ) ` Z ) <_ S /\ -. ( ( C ` j ) ` Z ) < S ) ) )
560 556 559 mpbird
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( C ` j ) ` Z ) = S )
561 id
 |-  ( ( ( C ` j ) ` Z ) = S -> ( ( C ` j ) ` Z ) = S )
562 561 eqcomd
 |-  ( ( ( C ` j ) ` Z ) = S -> S = ( ( C ` j ) ` Z ) )
563 562 oveq1d
 |-  ( ( ( C ` j ) ` Z ) = S -> ( S - ( ( C ` j ) ` Z ) ) = ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) )
564 563 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ ( ( C ` j ) ` Z ) = S ) -> ( S - ( ( C ` j ) ` Z ) ) = ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) )
565 385 126 sselid
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. CC )
566 565 subidd
 |-  ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) = 0 )
567 566 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( ( C ` j ) ` Z ) = S ) -> ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) = 0 )
568 564 567 eqtr2d
 |-  ( ( ( ph /\ j e. NN ) /\ ( ( C ` j ) ` Z ) = S ) -> 0 = ( S - ( ( C ` j ) ` Z ) ) )
569 551 560 568 syl2anc
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> 0 = ( S - ( ( C ` j ) ` Z ) ) )
570 550 569 eqtrd
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = ( S - ( ( C ` j ) ` Z ) ) )
571 548 570 pm2.61dan
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = ( S - ( ( C ` j ) ` Z ) ) )
572 543 546 571 3eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) ) = ( S - ( ( C ` j ) ` Z ) ) )
573 523 572 oveq12d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) ) x. ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) ) ) = ( ( P ` j ) x. ( S - ( ( C ` j ) ` Z ) ) ) )
574 386 274 sselid
 |-  ( ( ph /\ j e. NN ) -> ( P ` j ) e. CC )
575 355 126 resubcld
 |-  ( ( ph /\ j e. NN ) -> ( S - ( ( C ` j ) ` Z ) ) e. RR )
576 575 recnd
 |-  ( ( ph /\ j e. NN ) -> ( S - ( ( C ` j ) ` Z ) ) e. CC )
577 574 576 mulcomd
 |-  ( ( ph /\ j e. NN ) -> ( ( P ` j ) x. ( S - ( ( C ` j ) ` Z ) ) ) = ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
578 577 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( P ` j ) x. ( S - ( ( C ` j ) ` Z ) ) ) = ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
579 450 573 578 3eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) = ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
580 579 oveq1d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) + ( ( Q - S ) x. ( P ` j ) ) ) )
581 183 adantr
 |-  ( ( ph /\ j e. NN ) -> ( Q - S ) e. CC )
582 576 581 574 adddird
 |-  ( ( ph /\ j e. NN ) -> ( ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) x. ( P ` j ) ) = ( ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) + ( ( Q - S ) x. ( P ` j ) ) ) )
583 582 eqcomd
 |-  ( ( ph /\ j e. NN ) -> ( ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) x. ( P ` j ) ) )
584 583 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) x. ( P ` j ) ) )
585 576 581 addcomd
 |-  ( ( ph /\ j e. NN ) -> ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) = ( ( Q - S ) + ( S - ( ( C ` j ) ` Z ) ) ) )
586 166 adantr
 |-  ( ( ph /\ j e. NN ) -> Q e. CC )
587 167 adantr
 |-  ( ( ph /\ j e. NN ) -> S e. CC )
588 586 587 565 npncand
 |-  ( ( ph /\ j e. NN ) -> ( ( Q - S ) + ( S - ( ( C ` j ) ` Z ) ) ) = ( Q - ( ( C ` j ) ` Z ) ) )
589 585 588 eqtrd
 |-  ( ( ph /\ j e. NN ) -> ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) = ( Q - ( ( C ` j ) ` Z ) ) )
590 589 oveq1d
 |-  ( ( ph /\ j e. NN ) -> ( ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) x. ( P ` j ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
591 590 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) x. ( P ` j ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
592 580 584 591 3eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
593 443 444 445 592 syl21anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
594 eqid
 |-  prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) )
595 1 223 50 447 5 125 410 594 hoiprodp1
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) = ( prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) x. ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) ) ) )
596 215 217 595 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) = ( prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) x. ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) ) ) )
597 596 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) = ( prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) x. ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) ) ) )
598 507 eqcomd
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
599 409 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> Q e. RR )
600 354 599 509 510 513 hsphoival
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) = if ( k e. Y , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Q , ( ( D ` j ) ` k ) , Q ) ) )
601 iftrue
 |-  ( k e. Y -> if ( k e. Y , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Q , ( ( D ` j ) ` k ) , Q ) ) = ( ( D ` j ) ` k ) )
602 601 adantl
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> if ( k e. Y , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Q , ( ( D ` j ) ` k ) , Q ) ) = ( ( D ` j ) ` k ) )
603 600 602 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) = ( ( D ` j ) ` k ) )
604 603 oveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
605 604 fveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) = ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
606 605 prodeq2dv
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
607 606 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) = prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
608 598 607 451 3eqtr4d
 |-  ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) = ( P ` j ) )
609 443 444 445 608 syl21anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) = ( P ` j ) )
610 354 409 345 49 50 hsphoival
 |-  ( ( ph /\ j e. NN ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) = if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) ) )
611 217 610 syldan
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) = if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) ) )
612 611 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) = if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) ) )
613 209 iffalsed
 |-  ( ph -> if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) ) = if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) )
614 613 ad2antrr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> if ( Z e. Y , ( ( D ` j ) ` Z ) , if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) ) = if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) )
615 217 51 syldan
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) ` Z ) e. RR )
616 615 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) e. RR )
617 simpr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) = Q )
618 616 617 eqled
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) <_ Q )
619 618 iftrued
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = ( ( D ` j ) ` Z ) )
620 619 617 eqtrd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = Q )
621 620 adantlr
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ ( ( D ` j ) ` Z ) = Q ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = Q )
622 84 adantr
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> Q e. RR )
623 622 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q e. RR )
624 623 adantlr
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q e. RR )
625 615 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) e. RR )
626 625 adantlr
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) e. RR )
627 25 a1i
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> Q = inf ( V , RR , < ) )
628 443 57 syl
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> V C_ RR )
629 161 ad2antrr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> E. x e. V A. y e. V x <_ y )
630 simplr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> j e. ( 1 ... M ) )
631 216 488 sylanl2
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
632 630 631 jca
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( j e. ( 1 ... M ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
633 rabid
 |-  ( j e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } <-> ( j e. ( 1 ... M ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
634 632 633 sylibr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> j e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } )
635 eqidd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) = ( ( D ` j ) ` Z ) )
636 fveq2
 |-  ( i = j -> ( D ` i ) = ( D ` j ) )
637 636 fveq1d
 |-  ( i = j -> ( ( D ` i ) ` Z ) = ( ( D ` j ) ` Z ) )
638 637 eqeq2d
 |-  ( i = j -> ( ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) <-> ( ( D ` j ) ` Z ) = ( ( D ` j ) ` Z ) ) )
639 638 rspcev
 |-  ( ( j e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ ( ( D ` j ) ` Z ) = ( ( D ` j ) ` Z ) ) -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
640 634 635 639 syl2anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
641 fvexd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. _V )
642 35 640 641 elrnmptd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) )
643 642 23 eleqtrrdi
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. O )
644 elun2
 |-  ( ( ( D ` j ) ` Z ) e. O -> ( ( D ` j ) ` Z ) e. ( { ( B ` Z ) } u. O ) )
645 643 644 syl
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. ( { ( B ` Z ) } u. O ) )
646 76 a1i
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( { ( B ` Z ) } u. O ) = V )
647 645 646 eleqtrd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. V )
648 lbinfle
 |-  ( ( V C_ RR /\ E. x e. V A. y e. V x <_ y /\ ( ( D ` j ) ` Z ) e. V ) -> inf ( V , RR , < ) <_ ( ( D ` j ) ` Z ) )
649 628 629 647 648 syl3anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> inf ( V , RR , < ) <_ ( ( D ` j ) ` Z ) )
650 627 649 eqbrtrd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> Q <_ ( ( D ` j ) ` Z ) )
651 650 adantr
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q <_ ( ( D ` j ) ` Z ) )
652 neqne
 |-  ( -. ( ( D ` j ) ` Z ) = Q -> ( ( D ` j ) ` Z ) =/= Q )
653 652 adantl
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) =/= Q )
654 624 626 651 653 leneltd
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q < ( ( D ` j ) ` Z ) )
655 624 626 ltnled
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( Q < ( ( D ` j ) ` Z ) <-> -. ( ( D ` j ) ` Z ) <_ Q ) )
656 654 655 mpbid
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> -. ( ( D ` j ) ` Z ) <_ Q )
657 656 iffalsed
 |-  ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = Q )
658 621 657 pm2.61dan
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = Q )
659 612 614 658 3eqtrd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) = Q )
660 659 oveq2d
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) Q ) )
661 660 fveq2d
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) Q ) ) )
662 215 217 126 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ` Z ) e. RR )
663 662 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) e. RR )
664 443 84 syl
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> Q e. RR )
665 volico
 |-  ( ( ( ( C ` j ) ` Z ) e. RR /\ Q e. RR ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) Q ) ) = if ( ( ( C ` j ) ` Z ) < Q , ( Q - ( ( C ` j ) ` Z ) ) , 0 ) )
666 663 664 665 syl2anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) Q ) ) = if ( ( ( C ` j ) ` Z ) < Q , ( Q - ( ( C ` j ) ` Z ) ) , 0 ) )
667 443 90 syl
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> S e. RR )
668 443 444 445 553 syl21anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) <_ S )
669 443 157 syl
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> S < Q )
670 663 667 664 668 669 lelttrd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) < Q )
671 670 iftrued
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> if ( ( ( C ` j ) ` Z ) < Q , ( Q - ( ( C ` j ) ` Z ) ) , 0 ) = ( Q - ( ( C ` j ) ` Z ) ) )
672 661 666 671 3eqtrd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) ) = ( Q - ( ( C ` j ) ` Z ) ) )
673 609 672 oveq12d
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( prod_ k e. Y ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) ) x. ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) ) ) = ( ( P ` j ) x. ( Q - ( ( C ` j ) ` Z ) ) ) )
674 215 166 syl
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> Q e. CC )
675 385 662 sselid
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ` Z ) e. CC )
676 674 675 subcld
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - ( ( C ` j ) ` Z ) ) e. CC )
677 306 676 mulcomd
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( P ` j ) x. ( Q - ( ( C ` j ) ` Z ) ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
678 677 adantr
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( P ` j ) x. ( Q - ( ( C ` j ) ` Z ) ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
679 597 673 678 3eqtrd
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
680 593 679 eqtr4d
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
681 442 680 eqled
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
682 439 441 681 syl2anc
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( P ` j ) = 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
683 438 682 pm2.61dan
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
684 213 402 415 683 fsumle
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) <_ sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
685 367 403 413 416 423 684 leadd12dd
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) <_ ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) )
686 321 mpteq1d
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) = ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) )
687 686 fveq2d
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
688 217 412 syldan
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
689 324 325 326 330 417 688 sge0splitmpt
 |-  ( ph -> ( sum^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
690 687 689 eqtrd
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
691 215 217 411 syl2anc
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
692 213 691 sge0fsummpt
 |-  ( ph -> ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) = sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
693 692 416 eqeltrd
 |-  ( ph -> ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR )
694 rexadd
 |-  ( ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR /\ ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR ) -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
695 413 693 694 syl2anc
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
696 692 oveq2d
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) = ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) )
697 690 695 696 3eqtrrd
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
698 685 697 breqtrd
 |-  ( ph -> ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
699 404 281 208 408 698 lemul2ad
 |-  ( ph -> ( ( 1 + E ) x. ( ( sum^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
700 399 699 eqbrtrd
 |-  ( ph -> ( ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
701 205 280 282 315 700 letrd
 |-  ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
702 189 701 eqbrtrd
 |-  ( ph -> ( G x. ( Q - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
703 165 702 jca
 |-  ( ph -> ( Q e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( Q - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) ) )
704 oveq1
 |-  ( z = Q -> ( z - ( A ` Z ) ) = ( Q - ( A ` Z ) ) )
705 704 oveq2d
 |-  ( z = Q -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( Q - ( A ` Z ) ) ) )
706 fveq2
 |-  ( z = Q -> ( H ` z ) = ( H ` Q ) )
707 706 fveq1d
 |-  ( z = Q -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` Q ) ` ( D ` j ) ) )
708 707 oveq2d
 |-  ( z = Q -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
709 708 mpteq2dv
 |-  ( z = Q -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) )
710 709 fveq2d
 |-  ( z = Q -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
711 710 oveq2d
 |-  ( z = Q -> ( ( 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 ` Q ) ` ( D ` j ) ) ) ) ) ) )
712 705 711 breq12d
 |-  ( z = Q -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( Q - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) ) )
713 712 elrab
 |-  ( Q 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 ) ) ) ) ) ) } <-> ( Q e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( Q - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) ) )
714 703 713 sylibr
 |-  ( ph -> Q 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 ) ) ) ) ) ) } )
715 714 17 eleqtrrdi
 |-  ( ph -> Q e. U )
716 breq2
 |-  ( u = Q -> ( S < u <-> S < Q ) )
717 716 rspcev
 |-  ( ( Q e. U /\ S < Q ) -> E. u e. U S < u )
718 715 157 717 syl2anc
 |-  ( ph -> E. u e. U S < u )