Theorem hoidmvlelem2 40810

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.)

Hypotheses

Ref	Expression
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 -> (Σ^ ` ( 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. (Σ^ ` ( 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

Ref	Expression
hoidmvlelem2	|- ( ph -> E. u e. U S < u )

Distinct variable groups:   x, k   A, a, b, k   z, A   B, a, b, k   y, B   z, B   C, a, b, j, k   C, i, j   z, C, j   D, a, b, j, k   D, c, j, k   D, i   y, D, j   z, D   z, E   F, a, b, k   z, G   H, a, b, k   z, H   J, a, b, k   K, a, b, k   z, L   i, M, j   i, O   P, a, b, k, x   Q, a, b, j, k, x   Q, c, x   u, Q   z, Q   S, a, b, j, k, x   S, c   S, i, x   u, S   z, S   u, U   x, V, y   W, a, b, j, k, x   W, c   z, W   Y, a, b, j, k, x   Y, c   y, Y   Z, c, j, k, x   i, Z   y, Z   z, Z   ph, a, b, j, k, x   ph, c   ph, i   ph, y

Allowed substitution hints:   ph( z, u)   A( x, y, u, i, j, c)   B( x, u, i, j, c)   C( x, y, u, c)   D( x, u)   P( y, z, u, i, j, c)   Q( y, i)   S( y)   U( x, y, z, i, j, k, a, b, c)   E( x, y, u, i, j, k, a, b, c)   F( x, y, z, u, i, j, c)   G( x, y, u, i, j, k, a, b, c)   H( x, y, u, i, j, c)   J( x, y, z, u, i, j, c)   K( x, y, z, u, i, j, c)   L( x, y, u, i, j, k, a, b, c)   M( x, y, z, u, k, a, b, c)   O( x, y, z, u, j, k, a, b, c)   V( z, u, i, j, k, a, b, c)   W( y, u, i)   X( x, y, z, u, i, j, k, a, b, c)   Y( z, u, i)   Z( u, a, b)

Proof of Theorem hoidmvlelem2

Dummy variable l is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hoidmvlelem2.a	. . . . . . 7 |- ( ph -> A : W --> RR )
2		hoidmvlelem2.z	. . . . . . . . . 10 |- ( ph -> Z e. ( X \ Y ) )
3		snidg 4206	. . . . . . . . . 10 |- ( Z e. ( X \ Y ) -> Z e. { Z } )
4	2, 3	syl 17	. . . . . . . . 9 |- ( ph -> Z e. { Z } )
5		elun2 3781	. . . . . . . . 9 |- ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
6	4, 5	syl 17	. . . . . . . 8 |- ( ph -> Z e. ( Y u. { Z } ) )
7		hoidmvlelem2.w	. . . . . . . 8 |- W = ( Y u. { Z } )
8	6, 7	syl6eleqr 2712	. . . . . . 7 |- ( ph -> Z e. W )
9	1, 8	ffvelrnd 6360	. . . . . 6 |- ( ph -> ( A ` Z ) e. RR )
10		hoidmvlelem2.b	. . . . . . 7 |- ( ph -> B : W --> RR )
11	10, 8	ffvelrnd 6360	. . . . . 6 |- ( ph -> ( B ` Z ) e. RR )
12		hoidmvlelem2.v	. . . . . . . 8 |- V = ( { ( B ` Z ) } u. O )
13	11	snssd 4340	. . . . . . . . 9 |- ( ph -> { ( B ` Z ) } C_ RR )
14		hoidmvlelem2.O	. . . . . . . . . 10 |- O = ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )
15		nfv 1843	. . . . . . . . . . 11 |- F/ i ph
16		eqid 2622	. . . . . . . . . . 11 |- ( 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 ) )
17		simpl 473	. . . . . . . . . . . 12 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ph )
18		fz1ssnn 12372	. . . . . . . . . . . . . 14 |- ( 1 ... M ) C_ NN
19		elrabi 3359	. . . . . . . . . . . . . 14 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> i e. ( 1 ... M ) )
20	18, 19	sseldi 3601	. . . . . . . . . . . . 13 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> i e. NN )
21	20	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> i e. NN )
22		eleq1 2689	. . . . . . . . . . . . . . 15 |- ( j = i -> ( j e. NN <-> i e. NN ) )
23	22	anbi2d 740	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ph /\ j e. NN ) <-> ( ph /\ i e. NN ) ) )
24		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( D ` j ) = ( D ` i ) )
25	24	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
26	25	eleq1d 2686	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( D ` j ) ` Z ) e. RR <-> ( ( D ` i ) ` Z ) e. RR ) )
27	23, 26	imbi12d 334	. . . . . . . . . . . . 13 |- ( j = i -> ( ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR ) <-> ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR ) ) )
28		hoidmvlelem2.d	. . . . . . . . . . . . . . . 16 |- ( ph -> D : NN --> ( RR ^m W ) )
29	28	ffvelrnda 6359	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
30		elmapi 7879	. . . . . . . . . . . . . . 15 |- ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
31	29, 30	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
32	8	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> Z e. W )
33	31, 32	ffvelrnd 6360	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR )
34	27, 33	chvarv 2263	. . . . . . . . . . . 12 |- ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR )
35	17, 21, 34	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( D ` i ) ` Z ) e. RR )
36	15, 16, 35	rnmptssd 39385	. . . . . . . . . 10 |- ( ph -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) C_ RR )
37	14, 36	syl5eqss 3649	. . . . . . . . 9 |- ( ph -> O C_ RR )
38	13, 37	unssd 3789	. . . . . . . 8 |- ( ph -> ( { ( B ` Z ) } u. O ) C_ RR )
39	12, 38	syl5eqss 3649	. . . . . . 7 |- ( ph -> V C_ RR )
40		hoidmvlelem2.q	. . . . . . . 8 |- Q = inf ( V , RR , < )
41		ltso 10118	. . . . . . . . . 10 |- < Or RR
42	41	a1i 11	. . . . . . . . 9 |- ( ph -> < Or RR )
43		snfi 8038	. . . . . . . . . . . 12 |- { ( B ` Z ) } e. Fin
44	43	a1i 11	. . . . . . . . . . 11 |- ( ph -> { ( B ` Z ) } e. Fin )
45		fzfi 12771	. . . . . . . . . . . . . . 15 |- ( 1 ... M ) e. Fin
46		rabfi 8185	. . . . . . . . . . . . . . 15 |- ( ( 1 ... M ) e. Fin -> { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin )
47	45, 46	ax-mp 5	. . . . . . . . . . . . . 14 |- { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin
48	47	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin )
49	16	rnmptfi 39351	. . . . . . . . . . . . 13 |- ( { 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 )
50	48, 49	syl 17	. . . . . . . . . . . 12 |- ( ph -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) e. Fin )
51	14, 50	syl5eqel 2705	. . . . . . . . . . 11 |- ( ph -> O e. Fin )
52		unfi 8227	. . . . . . . . . . 11 |- ( ( { ( B ` Z ) } e. Fin /\ O e. Fin ) -> ( { ( B ` Z ) } u. O ) e. Fin )
53	44, 51, 52	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( { ( B ` Z ) } u. O ) e. Fin )
54	12, 53	syl5eqel 2705	. . . . . . . . 9 |- ( ph -> V e. Fin )
55		fvex 6201	. . . . . . . . . . . . . 14 |- ( B ` Z ) e. _V
56	55	snid 4208	. . . . . . . . . . . . 13 |- ( B ` Z ) e. { ( B ` Z ) }
57		elun1 3780	. . . . . . . . . . . . 13 |- ( ( B ` Z ) e. { ( B ` Z ) } -> ( B ` Z ) e. ( { ( B ` Z ) } u. O ) )
58	56, 57	ax-mp 5	. . . . . . . . . . . 12 |- ( B ` Z ) e. ( { ( B ` Z ) } u. O )
59	12	eqcomi 2631	. . . . . . . . . . . 12 |- ( { ( B ` Z ) } u. O ) = V
60	58, 59	eleqtri 2699	. . . . . . . . . . 11 |- ( B ` Z ) e. V
61	60	a1i 11	. . . . . . . . . 10 |- ( ph -> ( B ` Z ) e. V )
62		ne0i 3921	. . . . . . . . . 10 |- ( ( B ` Z ) e. V -> V =/= (/) )
63	61, 62	syl 17	. . . . . . . . 9 |- ( ph -> V =/= (/) )
64		fiinfcl 8407	. . . . . . . . 9 |- ( ( < Or RR /\ ( V e. Fin /\ V =/= (/) /\ V C_ RR ) ) -> inf ( V , RR , < ) e. V )
65	42, 54, 63, 39, 64	syl13anc 1328	. . . . . . . 8 |- ( ph -> inf ( V , RR , < ) e. V )
66	40, 65	syl5eqel 2705	. . . . . . 7 |- ( ph -> Q e. V )
67	39, 66	sseldd 3604	. . . . . 6 |- ( ph -> Q e. RR )
68		hoidmvlelem2.u	. . . . . . . . . . . 12 |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
69		ssrab2 3687	. . . . . . . . . . . 12 |- { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } C_ ( ( A ` Z ) [,] ( B ` Z ) )
70	68, 69	eqsstri 3635	. . . . . . . . . . 11 |- U C_ ( ( A ` Z ) [,] ( B ` Z ) )
71	70	a1i 11	. . . . . . . . . 10 |- ( ph -> U C_ ( ( A ` Z ) [,] ( B ` Z ) ) )
72	9, 11	iccssred 39727	. . . . . . . . . 10 |- ( ph -> ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR )
73	71, 72	sstrd 3613	. . . . . . . . 9 |- ( ph -> U C_ RR )
74		hoidmvlelem2.su	. . . . . . . . 9 |- ( ph -> S e. U )
75	73, 74	sseldd 3604	. . . . . . . 8 |- ( ph -> S e. RR )
76	9	rexrd 10089	. . . . . . . . 9 |- ( ph -> ( A ` Z ) e. RR* )
77	11	rexrd 10089	. . . . . . . . 9 |- ( ph -> ( B ` Z ) e. RR* )
78	70, 74	sseldi 3601	. . . . . . . . 9 |- ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) )
79		iccgelb 12230	. . . . . . . . 9 |- ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ S e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> ( A ` Z ) <_ S )
80	76, 77, 78, 79	syl3anc 1326	. . . . . . . 8 |- ( ph -> ( A ` Z ) <_ S )
81		hoidmvlelem2.sb	. . . . . . . . . . . . . . 15 |- ( ph -> S < ( B ` Z ) )
82	81	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ x = ( B ` Z ) ) -> S < ( B ` Z ) )
83		id 22	. . . . . . . . . . . . . . . 16 |- ( x = ( B ` Z ) -> x = ( B ` Z ) )
84	83	eqcomd 2628	. . . . . . . . . . . . . . 15 |- ( x = ( B ` Z ) -> ( B ` Z ) = x )
85	84	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ x = ( B ` Z ) ) -> ( B ` Z ) = x )
86	82, 85	breqtrd 4679	. . . . . . . . . . . . 13 |- ( ( ph /\ x = ( B ` Z ) ) -> S < x )
87	86	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. V ) /\ x = ( B ` Z ) ) -> S < x )
88		simpll 790	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> ph )
89		id 22	. . . . . . . . . . . . . . . . 17 |- ( x e. V -> x e. V )
90	89, 12	syl6eleq 2711	. . . . . . . . . . . . . . . 16 |- ( x e. V -> x e. ( { ( B ` Z ) } u. O ) )
91	90	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( x e. V /\ -. x = ( B ` Z ) ) -> x e. ( { ( B ` Z ) } u. O ) )
92		elsni 4194	. . . . . . . . . . . . . . . . 17 |- ( x e. { ( B ` Z ) } -> x = ( B ` Z ) )
93	92	con3i 150	. . . . . . . . . . . . . . . 16 |- ( -. x = ( B ` Z ) -> -. x e. { ( B ` Z ) } )
94	93	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( x e. V /\ -. x = ( B ` Z ) ) -> -. x e. { ( B ` Z ) } )
95		elunnel1 3754	. . . . . . . . . . . . . . 15 |- ( ( x e. ( { ( B ` Z ) } u. O ) /\ -. x e. { ( B ` Z ) } ) -> x e. O )
96	91, 94, 95	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( x e. V /\ -. x = ( B ` Z ) ) -> x e. O )
97	96	adantll 750	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> x e. O )
98		id 22	. . . . . . . . . . . . . . . . 17 |- ( x e. O -> x e. O )
99	98, 14	syl6eleq 2711	. . . . . . . . . . . . . . . 16 |- ( x e. O -> x e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) )
100		vex 3203	. . . . . . . . . . . . . . . . 17 |- x e. _V
101	16	elrnmpt 5372	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( 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 ) )
103	99, 102	sylib 208	. . . . . . . . . . . . . . 15 |- ( x e. O -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
104	103	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. O ) -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
105		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = i -> ( C ` j ) = ( C ` i ) )
106	105	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = i -> ( ( C ` j ) ` Z ) = ( ( C ` i ) ` Z ) )
107	106	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = i -> ( ( ( C ` j ) ` Z ) e. RR <-> ( ( C ` i ) ` Z ) e. RR ) )
108	23, 107	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = i -> ( ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR ) <-> ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR ) ) )
109		hoidmvlelem2.c	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> C : NN --> ( RR ^m W ) )
110	109	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
111		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
112	110, 111	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
113	112, 32	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR )
114	108, 113	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR )
115	114	rexrd 10089	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR* )
116	17, 21, 115	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( C ` i ) ` Z ) e. RR* )
117	34	rexrd 10089	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR* )
118	17, 21, 117	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( D ` i ) ` Z ) e. RR* )
119	106, 25	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
120	119	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = i -> ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
121	120	elrab 3363	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) ) ) )
122	121	biimpi 206	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) ) )
123	122	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
124	123	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
125		icoltub 39732	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( C ` i ) ` Z ) e. RR* /\ ( ( D ` i ) ` Z ) e. RR* /\ S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) -> S < ( ( D ` i ) ` Z ) )
126	116, 118, 124, 125	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> S < ( ( D ` i ) ` Z ) )
127	126	3adant3 1081	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> S < ( ( D ` i ) ` Z ) )
128		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( ( D ` i ) ` Z ) -> x = ( ( D ` i ) ` Z ) )
129	128	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( ( D ` i ) ` Z ) -> ( ( D ` i ) ` Z ) = x )
130	129	3ad2ant3 1084	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> ( ( D ` i ) ` Z ) = x )
131	127, 130	breqtrd 4679	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> S < x )
132	131	3exp 1264	. . . . . . . . . . . . . . . 16 |- ( ph -> ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( x = ( ( D ` i ) ` Z ) -> S < x ) ) )
133	132	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. O ) -> ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( x = ( ( D ` i ) ` Z ) -> S < x ) ) )
134	133	rexlimdv 3030	. . . . . . . . . . . . . 14 |- ( ( 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 ) )
135	104, 134	mpd 15	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. O ) -> S < x )
136	88, 97, 135	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> S < x )
137	87, 136	pm2.61dan 832	. . . . . . . . . . 11 |- ( ( ph /\ x e. V ) -> S < x )
138	137	ralrimiva 2966	. . . . . . . . . 10 |- ( ph -> A. x e. V S < x )
139		breq2 4657	. . . . . . . . . . 11 |- ( x = inf ( V , RR , < ) -> ( S < x <-> S < inf ( V , RR , < ) ) )
140	139	rspcva 3307	. . . . . . . . . 10 |- ( (inf ( V , RR , < ) e. V /\ A. x e. V S < x ) -> S < inf ( V , RR , < ) )
141	65, 138, 140	syl2anc 693	. . . . . . . . 9 |- ( ph -> S < inf ( V , RR , < ) )
142	40	eqcomi 2631	. . . . . . . . . 10 |- inf ( V , RR , < ) = Q
143	142	a1i 11	. . . . . . . . 9 |- ( ph -> inf ( V , RR , < ) = Q )
144	141, 143	breqtrd 4679	. . . . . . . 8 |- ( ph -> S < Q )
145	9, 75, 67, 80, 144	lelttrd 10195	. . . . . . 7 |- ( ph -> ( A ` Z ) < Q )
146	9, 67, 145	ltled 10185	. . . . . 6 |- ( ph -> ( A ` Z ) <_ Q )
147		fiminre 10972	. . . . . . . . 9 |- ( ( V C_ RR /\ V e. Fin /\ V =/= (/) ) -> E. x e. V A. y e. V x <_ y )
148	39, 54, 63, 147	syl3anc 1326	. . . . . . . 8 |- ( ph -> E. x e. V A. y e. V x <_ y )
149		lbinfle 10978	. . . . . . . 8 |- ( ( V C_ RR /\ E. x e. V A. y e. V x <_ y /\ ( B ` Z ) e. V ) -> inf ( V , RR , < ) <_ ( B ` Z ) )
150	39, 148, 61, 149	syl3anc 1326	. . . . . . 7 |- ( ph -> inf ( V , RR , < ) <_ ( B ` Z ) )
151	40, 150	syl5eqbr 4688	. . . . . 6 |- ( ph -> Q <_ ( B ` Z ) )
152	9, 11, 67, 146, 151	eliccd 39726	. . . . 5 |- ( ph -> Q e. ( ( A ` Z ) [,] ( B ` Z ) ) )
153	67	recnd 10068	. . . . . . . . . 10 |- ( ph -> Q e. CC )
154	75	recnd 10068	. . . . . . . . . 10 |- ( ph -> S e. CC )
155	9	recnd 10068	. . . . . . . . . 10 |- ( ph -> ( A ` Z ) e. CC )
156	153, 154, 155	npncand 10416	. . . . . . . . 9 |- ( ph -> ( ( Q - S ) + ( S - ( A ` Z ) ) ) = ( Q - ( A ` Z ) ) )
157	156	eqcomd 2628	. . . . . . . 8 |- ( ph -> ( Q - ( A ` Z ) ) = ( ( Q - S ) + ( S - ( A ` Z ) ) ) )
158	157	oveq2d 6666	. . . . . . 7 |- ( ph -> ( G x. ( Q - ( A ` Z ) ) ) = ( G x. ( ( Q - S ) + ( S - ( A ` Z ) ) ) ) )
159		rge0ssre 12280	. . . . . . . . . 10 |- ( 0 [,) +oo ) C_ RR
160		hoidmvlelem2.g	. . . . . . . . . . 11 |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
161		hoidmvlelem2.l	. . . . . . . . . . . 12 |- 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 ) ) ) ) ) )
162		hoidmvlelem2.x	. . . . . . . . . . . . 13 |- ( ph -> X e. Fin )
163		hoidmvlelem2.y	. . . . . . . . . . . . 13 |- ( ph -> Y C_ X )
164	162, 163	ssfid 8183	. . . . . . . . . . . 12 |- ( ph -> Y e. Fin )
165		ssun1 3776	. . . . . . . . . . . . . . 15 |- Y C_ ( Y u. { Z } )
166	165, 7	sseqtr4i 3638	. . . . . . . . . . . . . 14 |- Y C_ W
167	166	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> Y C_ W )
168	1, 167	fssresd 6071	. . . . . . . . . . . 12 |- ( ph -> ( A |` Y ) : Y --> RR )
169	10, 167	fssresd 6071	. . . . . . . . . . . 12 |- ( ph -> ( B |` Y ) : Y --> RR )
170	161, 164, 168, 169	hoidmvcl 40796	. . . . . . . . . . 11 |- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. ( 0 [,) +oo ) )
171	160, 170	syl5eqel 2705	. . . . . . . . . 10 |- ( ph -> G e. ( 0 [,) +oo ) )
172	159, 171	sseldi 3601	. . . . . . . . 9 |- ( ph -> G e. RR )
173	172	recnd 10068	. . . . . . . 8 |- ( ph -> G e. CC )
174	153, 154	subcld 10392	. . . . . . . 8 |- ( ph -> ( Q - S ) e. CC )
175	154, 155	subcld 10392	. . . . . . . 8 |- ( ph -> ( S - ( A ` Z ) ) e. CC )
176	173, 174, 175	adddid 10064	. . . . . . 7 |- ( ph -> ( G x. ( ( Q - S ) + ( S - ( A ` Z ) ) ) ) = ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) )
177	173, 174	mulcld 10060	. . . . . . . 8 |- ( ph -> ( G x. ( Q - S ) ) e. CC )
178	173, 175	mulcld 10060	. . . . . . . 8 |- ( ph -> ( G x. ( S - ( A ` Z ) ) ) e. CC )
179	177, 178	addcomd 10238	. . . . . . 7 |- ( ph -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) = ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) )
180	158, 176, 179	3eqtrd 2660	. . . . . 6 |- ( ph -> ( G x. ( Q - ( A ` Z ) ) ) = ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) )
181	67, 75	jca 554	. . . . . . . . . . . . 13 |- ( ph -> ( Q e. RR /\ S e. RR ) )
182		resubcl 10345	. . . . . . . . . . . . 13 |- ( ( Q e. RR /\ S e. RR ) -> ( Q - S ) e. RR )
183	181, 182	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( Q - S ) e. RR )
184	172, 183	jca 554	. . . . . . . . . . 11 |- ( ph -> ( G e. RR /\ ( Q - S ) e. RR ) )
185		remulcl 10021	. . . . . . . . . . 11 |- ( ( G e. RR /\ ( Q - S ) e. RR ) -> ( G x. ( Q - S ) ) e. RR )
186	184, 185	syl 17	. . . . . . . . . 10 |- ( ph -> ( G x. ( Q - S ) ) e. RR )
187	75, 9	jca 554	. . . . . . . . . . . . 13 |- ( ph -> ( S e. RR /\ ( A ` Z ) e. RR ) )
188		resubcl 10345	. . . . . . . . . . . . 13 |- ( ( S e. RR /\ ( A ` Z ) e. RR ) -> ( S - ( A ` Z ) ) e. RR )
189	187, 188	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( S - ( A ` Z ) ) e. RR )
190	172, 189	jca 554	. . . . . . . . . . 11 |- ( ph -> ( G e. RR /\ ( S - ( A ` Z ) ) e. RR ) )
191		remulcl 10021	. . . . . . . . . . 11 |- ( ( G e. RR /\ ( S - ( A ` Z ) ) e. RR ) -> ( G x. ( S - ( A ` Z ) ) ) e. RR )
192	190, 191	syl 17	. . . . . . . . . 10 |- ( ph -> ( G x. ( S - ( A ` Z ) ) ) e. RR )
193	186, 192	jca 554	. . . . . . . . 9 |- ( ph -> ( ( G x. ( Q - S ) ) e. RR /\ ( G x. ( S - ( A ` Z ) ) ) e. RR ) )
194		readdcl 10019	. . . . . . . . 9 |- ( ( ( G x. ( Q - S ) ) e. RR /\ ( G x. ( S - ( A ` Z ) ) ) e. RR ) -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) e. RR )
195	193, 194	syl 17	. . . . . . . 8 |- ( ph -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) e. RR )
196	179, 195	eqeltrrd 2702	. . . . . . 7 |- ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) e. RR )
197		1red 10055	. . . . . . . . . 10 |- ( ph -> 1 e. RR )
198		hoidmvlelem2.e	. . . . . . . . . . 11 |- ( ph -> E e. RR+ )
199	198	rpred 11872	. . . . . . . . . 10 |- ( ph -> E e. RR )
200	197, 199	readdcld 10069	. . . . . . . . 9 |- ( ph -> ( 1 + E ) e. RR )
201	2	eldifbd 3587	. . . . . . . . . . 11 |- ( ph -> -. Z e. Y )
202	8, 201	eldifd 3585	. . . . . . . . . 10 |- ( ph -> Z e. ( W \ Y ) )
203		hoidmvlelem2.r	. . . . . . . . . 10 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
204		hoidmvlelem2.h	. . . . . . . . . 10 |- 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 ) ) ) ) )
205	161, 164, 202, 7, 109, 28, 203, 204, 75	sge0hsphoire 40803	. . . . . . . . 9 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
206	200, 205	remulcld 10070	. . . . . . . 8 |- ( ph -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
207		fzfid 12772	. . . . . . . . . 10 |- ( ph -> ( 1 ... M ) e. Fin )
208	183	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - S ) e. RR )
209		simpl 473	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ph )
210		elfznn 12370	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> j e. NN )
211	210	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> j e. NN )
212		id 22	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> j e. NN )
213		ovexd 6680	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V )
214		hoidmvlelem2.p	. . . . . . . . . . . . . . . . 17 |- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
215	214	fvmpt2 6291	. . . . . . . . . . . . . . . 16 |- ( ( j e. NN /\ ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
216	212, 213, 215	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
217	216	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
218	164	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> Y e. Fin )
219	166	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN ) -> Y C_ W )
220	112, 219	fssresd 6071	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) |` Y ) : Y --> RR )
221	220	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) |` Y ) : Y --> RR )
222		iftrue 4092	. . . . . . . . . . . . . . . . . . . 20 |- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
223	222	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) )
224	223	feq1d 6030	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
225	221, 224	mpbird 247	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
226		0red 10041	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. Y ) -> 0 e. RR )
227		hoidmvlelem2.f	. . . . . . . . . . . . . . . . . . . 20 |- F = ( y e. Y |-> 0 )
228	226, 227	fmptd 6385	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F : Y --> RR )
229	228	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F : Y --> RR )
230		iffalse 4095	. . . . . . . . . . . . . . . . . . . 20 |- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
231	230	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 )
232	231	feq1d 6030	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
233	229, 232	mpbird 247	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
234	225, 233	pm2.61dan 832	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
235		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> j e. NN )
236		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( C ` j ) e. _V
237	236	resex 5443	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( C ` j ) |` Y ) e. _V
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( C ` j ) |` Y ) e. _V )
239	162, 163	ssexd 4805	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> Y e. _V )
240		mptexg 6484	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Y e. _V -> ( y e. Y |-> 0 ) e. _V )
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( y e. Y |-> 0 ) e. _V )
242	227, 241	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> F e. _V )
243	238, 242	ifcld 4131	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
244	243	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
245		hoidmvlelem2.j	. . . . . . . . . . . . . . . . . . 19 |- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
246	245	fvmpt2 6291	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) )
247	235, 244, 246	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
248	247	feq1d 6030	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( J ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR ) )
249	234, 248	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR )
250	31, 219	fssresd 6071	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN ) -> ( ( D ` j ) |` Y ) : Y --> RR )
251	250	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( D ` j ) |` Y ) : Y --> RR )
252		iftrue 4092	. . . . . . . . . . . . . . . . . . . 20 |- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
253	252	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) )
254	253	feq1d 6030	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
255	251, 254	mpbird 247	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
256		iffalse 4095	. . . . . . . . . . . . . . . . . . . 20 |- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = F )
257	256	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 )
258	257	feq1d 6030	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
259	229, 258	mpbird 247	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
260	255, 259	pm2.61dan 832	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR )
261		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D ` j ) e. _V
262	261	resex 5443	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( D ` j ) |` Y ) e. _V
263	262	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( D ` j ) |` Y ) e. _V )
264	263, 242	ifcld 4131	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
265	264	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
266		hoidmvlelem2.k	. . . . . . . . . . . . . . . . . . 19 |- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
267	266	fvmpt2 6291	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) )
268	235, 265, 267	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
269	268	feq1d 6030	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( K ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR ) )
270	260, 269	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( K ` j ) : Y --> RR )
271	161, 218, 249, 270	hoidmvcl 40796	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. ( 0 [,) +oo ) )
272	217, 271	eqeltrd 2701	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) )
273	159, 272	sseldi 3601	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> ( P ` j ) e. RR )
274	209, 211, 273	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P ` j ) e. RR )
275	208, 274	remulcld 10070	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( Q - S ) x. ( P ` j ) ) e. RR )
276	207, 275	fsumrecl 14465	. . . . . . . . 9 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) e. RR )
277	200, 276	remulcld 10070	. . . . . . . 8 |- ( ph -> ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
278	206, 277	readdcld 10069	. . . . . . 7 |- ( ph -> ( ( ( 1 + E ) x. (Σ^ ` ( 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 )
279	161, 164, 202, 7, 109, 28, 203, 204, 67	sge0hsphoire 40803	. . . . . . . 8 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR )
280	200, 279	remulcld 10070	. . . . . . 7 |- ( ph -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) e. RR )
281	74, 68	syl6eleq 2711	. . . . . . . . . 10 |- ( ph -> S e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
282		oveq1 6657	. . . . . . . . . . . . 13 |- ( z = S -> ( z - ( A ` Z ) ) = ( S - ( A ` Z ) ) )
283	282	oveq2d 6666	. . . . . . . . . . . 12 |- ( z = S -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( S - ( A ` Z ) ) ) )
284		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( z = S -> ( H ` z ) = ( H ` S ) )
285	284	fveq1d 6193	. . . . . . . . . . . . . . . 16 |- ( z = S -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` S ) ` ( D ` j ) ) )
286	285	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( z = S -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
287	286	mpteq2dv 4745	. . . . . . . . . . . . . 14 |- ( z = S -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) )
288	287	fveq2d 6195	. . . . . . . . . . . . 13 |- ( z = S -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) )
289	288	oveq2d 6666	. . . . . . . . . . . 12 |- ( z = S -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
290	283, 289	breq12d 4666	. . . . . . . . . . 11 |- ( z = S -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
291	290	elrab 3363	. . . . . . . . . 10 |- ( S e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( 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. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
292	281, 291	sylib 208	. . . . . . . . 9 |- ( ph -> ( S e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
293	292	simprd 479	. . . . . . . 8 |- ( ph -> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
294	207, 274	fsumrecl 14465	. . . . . . . . . . 11 |- ( ph -> sum_ j e. ( 1 ... M ) ( P ` j ) e. RR )
295	200, 294	remulcld 10070	. . . . . . . . . 10 |- ( ph -> ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) e. RR )
296		0red 10041	. . . . . . . . . . 11 |- ( ph -> 0 e. RR )
297	75, 67	posdifd 10614	. . . . . . . . . . . 12 |- ( ph -> ( S < Q <-> 0 < ( Q - S ) ) )
298	144, 297	mpbid 222	. . . . . . . . . . 11 |- ( ph -> 0 < ( Q - S ) )
299	296, 183, 298	ltled 10185	. . . . . . . . . 10 |- ( ph -> 0 <_ ( Q - S ) )
300		hoidmvlelem2.le	. . . . . . . . . 10 |- ( ph -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) )
301	172, 295, 183, 299, 300	lemul1ad 10963	. . . . . . . . 9 |- ( ph -> ( G x. ( Q - S ) ) <_ ( ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) x. ( Q - S ) ) )
302	200	recnd 10068	. . . . . . . . . . 11 |- ( ph -> ( 1 + E ) e. CC )
303	294	recnd 10068	. . . . . . . . . . 11 |- ( ph -> sum_ j e. ( 1 ... M ) ( P ` j ) e. CC )
304	302, 303, 174	mulassd 10063	. . . . . . . . . 10 |- ( 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 ) ) ) )
305	274	recnd 10068	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P ` j ) e. CC )
306	207, 174, 305	fsummulc1 14517	. . . . . . . . . . . 12 |- ( ph -> ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( P ` j ) x. ( Q - S ) ) )
307	174	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - S ) e. CC )
308	305, 307	mulcomd 10061	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( P ` j ) x. ( Q - S ) ) = ( ( Q - S ) x. ( P ` j ) ) )
309	308	sumeq2dv 14433	. . . . . . . . . . . 12 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) )
310	306, 309	eqtrd 2656	. . . . . . . . . . 11 |- ( ph -> ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) )
311	310	oveq2d 6666	. . . . . . . . . 10 |- ( 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 ) ) ) )
312	304, 311	eqtrd 2656	. . . . . . . . 9 |- ( 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	301, 312	breqtrd 4679	. . . . . . . 8 |- ( ph -> ( G x. ( Q - S ) ) <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
314	192, 186, 206, 277, 293, 313	leadd12dd 39532	. . . . . . 7 |- ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) <_ ( ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
315		hoidmvlelem2.m	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. NN )
316		nnsplit 39574	. . . . . . . . . . . . . . . . 17 |- ( M e. NN -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
317	315, 316	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
318		uncom 3757	. . . . . . . . . . . . . . . . 17 |- ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) )
319	318	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) )
320	317, 319	eqtr2d 2657	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) = NN )
321	320	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( ph -> NN = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) )
322	321	mpteq1d 4738	. . . . . . . . . . . . 13 |- ( 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 6195	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
324		nfv 1843	. . . . . . . . . . . . 13 |- F/ j ph
325		fvexd 6203	. . . . . . . . . . . . 13 |- ( ph -> ( ZZ>= ` ( M + 1 ) ) e. _V )
326		ovexd 6680	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... M ) e. _V )
327		incom 3805	. . . . . . . . . . . . . . 15 |- ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = ( ( 1 ... M ) i^i ( ZZ>= ` ( M + 1 ) ) )
328		nnuzdisj 39571	. . . . . . . . . . . . . . 15 |- ( ( 1 ... M ) i^i ( ZZ>= ` ( M + 1 ) ) ) = (/)
329	327, 328	eqtri 2644	. . . . . . . . . . . . . 14 |- ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = (/)
330	329	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = (/) )
331		icossicc 12260	. . . . . . . . . . . . . 14 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
332		ssid 3624	. . . . . . . . . . . . . . 15 |- ( 0 [,) +oo ) C_ ( 0 [,) +oo )
333		simpl 473	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ph )
334	315	peano2nnd 11037	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( M + 1 ) e. NN )
335		uznnssnn 11735	. . . . . . . . . . . . . . . . . . 19 |- ( ( M + 1 ) e. NN -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
336	334, 335	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
337	336	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
338		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. ( ZZ>= ` ( M + 1 ) ) )
339	337, 338	sseldd 3604	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. NN )
340		snfi 8038	. . . . . . . . . . . . . . . . . . . . 21 |- { Z } e. Fin
341	340	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> { Z } e. Fin )
342		unfi 8227	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Y e. Fin /\ { Z } e. Fin ) -> ( Y u. { Z } ) e. Fin )
343	164, 341, 342	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( Y u. { Z } ) e. Fin )
344	7, 343	syl5eqel 2705	. . . . . . . . . . . . . . . . . 18 |- ( ph -> W e. Fin )
345	344	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> W e. Fin )
346		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = l -> ( j e. Y <-> l e. Y ) )
347		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = l -> ( c ` j ) = ( c ` l ) )
348	347	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = l -> ( ( c ` j ) <_ x <-> ( c ` l ) <_ x ) )
349	348, 347	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = l -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` l ) <_ x , ( c ` l ) , x ) )
350	346, 347, 349	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 4750	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 4741	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 4741	. . . . . . . . . . . . . . . . . . 19 |- ( 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	204, 353	eqtri 2644	. . . . . . . . . . . . . . . . . 18 |- 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	75	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> S e. RR )
356	354, 355, 345, 31	hsphoif 40790	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( ( H ` S ) ` ( D ` j ) ) : W --> RR )
357	161, 345, 112, 356	hoidmvcl 40796	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
358	333, 339, 357	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
359	332, 358	sseldi 3601	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
360	331, 359	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
361	209, 211, 357	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
362	331, 361	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
363	324, 325, 326, 330, 360, 362	sge0splitmpt 40628	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
364		nnex 11026	. . . . . . . . . . . . . . 15 |- NN e. _V
365	364	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> NN e. _V )
366	331, 357	sseldi 3601	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
367	324, 365, 366, 205, 336	sge0ssrempt 40622	. . . . . . . . . . . . 13 |- ( ph -> (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
368	18	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... M ) C_ NN )
369	324, 365, 366, 205, 368	sge0ssrempt 40622	. . . . . . . . . . . . 13 |- ( ph -> (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
370		rexadd 12063	. . . . . . . . . . . . 13 |- ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR /\ (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR ) -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
371	367, 369, 370	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
372	323, 363, 371	3eqtrd 2660	. . . . . . . . . . 11 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
373	372	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
374	373	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( ( 1 + E ) x. (Σ^ ` ( 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. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( 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, 205	eqeltrrd 2702	. . . . . . . . . . . 12 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
376	375	recnd 10068	. . . . . . . . . . 11 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. CC )
377	276	recnd 10068	. . . . . . . . . . 11 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) e. CC )
378	302, 376, 377	adddid 10064	. . . . . . . . . 10 |- ( ph -> ( ( 1 + E ) x. ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( 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. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( 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 2628	. . . . . . . . 9 |- ( ph -> ( ( ( 1 + E ) x. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( 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. ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( 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 10068	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. CC )
381	369	recnd 10068	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. CC )
382	380, 381, 377	addassd 10062	. . . . . . . . . . 11 |- ( ph -> ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
383	207, 361	sge0fsummpt 40607	. . . . . . . . . . . . . 14 |- ( ph -> (Σ^ ` ( 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 6665	. . . . . . . . . . . . 13 |- ( ph -> ( (Σ^ ` ( 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 9993	. . . . . . . . . . . . . . . . . 18 |- RR C_ CC
386	159, 385	sstri 3612	. . . . . . . . . . . . . . . . 17 |- ( 0 [,) +oo ) C_ CC
387	386, 357	sseldi 3601	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. CC )
388	209, 211, 387	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. CC )
389	183	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> ( Q - S ) e. RR )
390	389, 273	remulcld 10070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( ( Q - S ) x. ( P ` j ) ) e. RR )
391	390	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( Q - S ) x. ( P ` j ) ) e. CC )
392	211, 391	syldan 487	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( Q - S ) x. ( P ` j ) ) e. CC )
393	207, 388, 392	fsumadd 14470	. . . . . . . . . . . . . 14 |- ( 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 2628	. . . . . . . . . . . . 13 |- ( 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 2656	. . . . . . . . . . . 12 |- ( ph -> ( (Σ^ ` ( 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 6666	. . . . . . . . . . 11 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( (Σ^ ` ( 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 2656	. . . . . . . . . 10 |- ( ph -> ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = ( (Σ^ ` ( 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 6666	. . . . . . . . 9 |- ( ph -> ( ( 1 + E ) x. ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( 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. ( (Σ^ ` ( 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 2660	. . . . . . . 8 |- ( ph -> ( ( ( 1 + E ) x. (Σ^ ` ( 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. ( (Σ^ ` ( 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	159, 357	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. RR )
401	400, 390	readdcld 10069	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
402	209, 211, 401	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
403	207, 402	fsumrecl 14465	. . . . . . . . . 10 |- ( 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 10069	. . . . . . . . 9 |- ( ph -> ( (Σ^ ` ( 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 10551	. . . . . . . . . . 11 |- 0 <_ 1
406	405	a1i 11	. . . . . . . . . 10 |- ( ph -> 0 <_ 1 )
407	198	rpge0d 11876	. . . . . . . . . 10 |- ( ph -> 0 <_ E )
408	197, 199, 406, 407	addge0d 10603	. . . . . . . . 9 |- ( ph -> 0 <_ ( 1 + E ) )
409	67	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> Q e. RR )
410	354, 409, 345, 31	hsphoif 40790	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( ( H ` Q ) ` ( D ` j ) ) : W --> RR )
411	161, 345, 112, 410	hoidmvcl 40796	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
412	331, 411	sseldi 3601	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
413	324, 365, 412, 279, 336	sge0ssrempt 40622	. . . . . . . . . . 11 |- ( ph -> (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR )
414	159, 411	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. RR )
415	209, 211, 414	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. RR )
416	207, 415	fsumrecl 14465	. . . . . . . . . . 11 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. RR )
417	333, 339, 412	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
418	202	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> Z e. ( W \ Y ) )
419	75, 67, 144	ltled 10185	. . . . . . . . . . . . . . 15 |- ( ph -> S <_ Q )
420	419	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> S <_ Q )
421	161, 345, 418, 7, 355, 409, 420, 354, 112, 31	hsphoidmvle2 40799	. . . . . . . . . . . . 13 |- ( ( 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 693	. . . . . . . . . . . 12 |- ( ( 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 40627	. . . . . . . . . . 11 |- ( ph -> (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) <_ (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
424	209	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) = 0 ) -> ph )
425	211	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) = 0 ) -> j e. NN )
426		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) = 0 ) -> ( P ` j ) = 0 )
427		oveq2 6658	. . . . . . . . . . . . . . . . . . 19 |- ( ( P ` j ) = 0 -> ( ( Q - S ) x. ( P ` j ) ) = ( ( Q - S ) x. 0 ) )
428	427	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( Q - S ) x. ( P ` j ) ) = ( ( Q - S ) x. 0 ) )
429	174	mul01d 10235	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( Q - S ) x. 0 ) = 0 )
430	429	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( Q - S ) x. 0 ) = 0 )
431	428, 430	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) = 0 ) -> ( ( Q - S ) x. ( P ` j ) ) = 0 )
432	431	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 10236	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + 0 ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
434	433	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 2656	. . . . . . . . . . . . . . 15 |- ( ( ( 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 481	. . . . . . . . . . . . . . 15 |- ( ( ( 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 4675	. . . . . . . . . . . . . 14 |- ( ( ( 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 1325	. . . . . . . . . . . . 13 |- ( ( ( 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 473	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( P ` j ) = 0 ) -> ( ph /\ j e. ( 1 ... M ) ) )
440		neqne 2802	. . . . . . . . . . . . . . 15 |- ( -. ( P ` j ) = 0 -> ( P ` j ) =/= 0 )
441	440	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( P ` j ) = 0 ) -> ( P ` j ) =/= 0 )
442	402	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
443	209	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ph )
444	211	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> j e. NN )
445		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( P ` j ) =/= 0 )
446	2	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN ) -> Z e. ( X \ Y ) )
447	201	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN ) -> -. Z e. Y )
448		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 |- 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	161, 218, 446, 447, 7, 112, 356, 448	hoiprodp1 40802	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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	217	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
452	218	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> Y e. Fin )
453	217	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
454		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( Y = (/) -> ( L ` Y ) = ( L ` (/) ) )
455	454	oveqd 6667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( Y = (/) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` j ) ( L ` (/) ) ( K ` j ) ) )
456	455	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` j ) ( L ` (/) ) ( K ` j ) ) )
457	249	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( J ` j ) : Y --> RR )
458		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( Y = (/) -> Y = (/) )
459	458	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( Y = (/) -> (/) = Y )
460	459	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> (/) = Y )
461	460	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( J ` j ) : (/) --> RR <-> ( J ` j ) : Y --> RR ) )
462	457, 461	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( J ` j ) : (/) --> RR )
463	270	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( K ` j ) : Y --> RR )
464	460	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( K ` j ) : (/) --> RR <-> ( K ` j ) : Y --> RR ) )
465	463, 464	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( K ` j ) : (/) --> RR )
466	161, 462, 465	hoidmv0val 40797	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( ( J ` j ) ( L ` (/) ) ( K ` j ) ) = 0 )
467	453, 456, 466	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. NN ) /\ Y = (/) ) -> ( P ` j ) = 0 )
468	467	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ Y = (/) ) -> ( P ` j ) = 0 )
469		neneq 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( P ` j ) =/= 0 -> -. ( P ` j ) = 0 )
470	469	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ Y = (/) ) -> -. ( P ` j ) = 0 )
471	468, 470	pm2.65da 600	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> -. Y = (/) )
472	471	neqned 2801	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> Y =/= (/) )
473	249	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( J ` j ) : Y --> RR )
474	270	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( K ` j ) : Y --> RR )
475	161, 452, 472, 473, 474	hoidmvn0val 40798	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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	247	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
477	217	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
478	247	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( 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, 231	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( J ` j ) = F )
480	268	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( 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, 257	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( K ` j ) = F )
482	479, 481	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( F ( L ` Y ) F ) )
483	161, 164, 228	hoidmvval0b 40804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> ( F ( L ` Y ) F ) = 0 )
484	483	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( F ( L ` Y ) F ) = 0 )
485	477, 482, 484	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( P ` j ) = 0 )
486	485	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( P ` j ) = 0 )
487	469	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> -. ( P ` j ) = 0 )
488	486, 487	condan 835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
489	488	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( J ` j ) = ( ( C ` j ) |` Y ) )
491	490	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( J ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
492	491	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( J ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
493		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( k e. Y -> ( ( ( C ` j ) |` Y ) ` k ) = ( ( C ` j ) ` k ) )
494	493	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( ( C ` j ) |` Y ) ` k ) = ( ( C ` j ) ` k ) )
495	492, 494	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( J ` j ) ` k ) = ( ( C ` j ) ` k ) )
496	268	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
497	488, 252	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( K ` j ) = ( ( D ` j ) |` Y ) )
499	498	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( K ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
500	499	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( K ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
501		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( k e. Y -> ( ( ( D ` j ) |` Y ) ` k ) = ( ( D ` j ) ` k ) )
502	501	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( ( D ` j ) |` Y ) ` k ) = ( ( D ` j ) ` k ) )
503	500, 502	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ k e. Y ) -> ( ( K ` j ) ` k ) = ( ( D ` j ) ` k ) )
504	495, 503	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 6195	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 14653	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> S e. RR )
509	345	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> W e. Fin )
510	31	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( D ` j ) : W --> RR )
511		elun1 3780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( k e. Y -> k e. ( Y u. { Z } ) )
512	511, 7	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( k e. Y -> k e. W )
513	512	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> k e. W )
514	354, 508, 509, 510, 513	hsphoival 40793	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( 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 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( 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 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( H ` S ) ` ( D ` j ) ) ` k ) = ( ( D ` j ) ` k ) )
518	517	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( C ` j ) ` k ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
519	518	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 14653	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 2628	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 2661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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, 31, 32	hsphoival 40793	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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	201	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 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 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. NN ) -> ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) = if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) )
528	527	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 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	113	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR* )
531	530	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) e. RR* )
532	33	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR* )
533	532	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. RR* )
534		icoltub 39732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( 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 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> S < ( ( D ` j ) ` Z ) )
536	355	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> S e. RR )
537	33	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. RR )
538	536, 537	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( S < ( ( D ` j ) ` Z ) <-> -. ( ( D ` j ) ` Z ) <_ S ) )
539	535, 538	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> -. ( ( D ` j ) ` Z ) <_ S )
540	539	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> if ( ( ( D ` j ) ` Z ) <_ S , ( ( D ` j ) ` Z ) , S ) = S )
541	540	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) S ) )
543	542	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) S ) ) )
544		volico 40200	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( C ` j ) ` Z ) e. RR /\ S e. RR ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) S ) ) = if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) )
545	113, 536, 544	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 857	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) S ) ) = if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) )
547		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( C ` j ) ` Z ) < S -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = ( S - ( ( C ` j ) ` Z ) ) )
548	547	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 4095	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. ( ( C ` j ) ` Z ) < S -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = 0 )
550	549	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> if ( ( ( C ` j ) ` Z ) < S , ( S - ( ( C ` j ) ` Z ) ) , 0 ) = 0 )
551		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ph /\ j e. NN ) )
552		icogelb 12225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) <_ S )
554	553	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( C ` j ) ` Z ) <_ S )
555		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> -. ( ( C ` j ) ` Z ) < S )
556	554, 555	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( ( C ` j ) ` Z ) <_ S /\ -. ( ( C ` j ) ` Z ) < S ) )
557	551, 113	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( C ` j ) ` Z ) e. RR )
558	551, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> S e. RR )
559	557, 558	eqleltd 10181	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> ( ( C ` j ) ` Z ) = S )
561		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( C ` j ) ` Z ) = S -> ( ( C ` j ) ` Z ) = S )
562	561	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( C ` j ) ` Z ) = S -> S = ( ( C ` j ) ` Z ) )
563	562	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( C ` j ) ` Z ) = S -> ( S - ( ( C ` j ) ` Z ) ) = ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) )
564	563	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. NN ) /\ ( ( C ` j ) ` Z ) = S ) -> ( S - ( ( C ` j ) ` Z ) ) = ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) )
565	385, 113	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. CC )
566	565	subidd 10380	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) = 0 )
567	566	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. NN ) /\ ( ( C ` j ) ` Z ) = S ) -> ( ( ( C ` j ) ` Z ) - ( ( C ` j ) ` Z ) ) = 0 )
568	564, 567	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. NN ) /\ ( ( C ` j ) ` Z ) = S ) -> 0 = ( S - ( ( C ` j ) ` Z ) ) )
569	551, 560, 568	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( C ` j ) ` Z ) < S ) -> 0 = ( S - ( ( C ` j ) ` Z ) ) )
570	550, 569	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 832	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 2660	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. NN ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` S ) ` ( D ` j ) ) ` Z ) ) ) = ( S - ( ( C ` j ) ` Z ) ) )
573	523, 572	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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, 272	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN ) -> ( P ` j ) e. CC )
575	355, 113	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. NN ) -> ( S - ( ( C ` j ) ` Z ) ) e. RR )
576	575	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN ) -> ( S - ( ( C ` j ) ` Z ) ) e. CC )
577	574, 576	mulcomd 10061	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. NN ) -> ( ( P ` j ) x. ( S - ( ( C ` j ) ` Z ) ) ) = ( ( S - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
578	577	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 2660	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 6665	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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	174	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. NN ) -> ( Q - S ) e. CC )
582	576, 581, 574	adddird 10065	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 2628	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 10238	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. NN ) -> ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) = ( ( Q - S ) + ( S - ( ( C ` j ) ` Z ) ) ) )
586	153	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN ) -> Q e. CC )
587	154	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. NN ) -> S e. CC )
588	586, 587, 565	npncand 10416	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. NN ) -> ( ( Q - S ) + ( S - ( ( C ` j ) ` Z ) ) ) = ( Q - ( ( C ` j ) ` Z ) ) )
589	585, 588	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN ) -> ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) = ( Q - ( ( C ` j ) ` Z ) ) )
590	589	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN ) -> ( ( ( S - ( ( C ` j ) ` Z ) ) + ( Q - S ) ) x. ( P ` j ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
591	590	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 2660	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 1325	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 2622	. . . . . . . . . . . . . . . . . . . 20 |- 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	161, 218, 32, 447, 7, 112, 410, 594	hoiprodp1 40802	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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	209, 211, 595	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 2628	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> Q e. RR )
600	354, 599, 509, 510, 513	hsphoival 40793	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 4092	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 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 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) = ( ( D ` j ) ` k ) )
604	603	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ j e. NN ) /\ k e. Y ) -> ( ( ( C ` j ) ` k ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
605	604	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 14653	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 2666	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 1325	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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, 31, 32	hsphoival 40793	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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	211, 610	syldan 487	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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	201	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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	211, 33	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) ` Z ) e. RR )
616	615	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) e. RR )
617		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) = Q )
618	616, 617	eqled 10140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) <_ Q )
619	618	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( ( D ` j ) ` Z ) = Q ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = Q )
621	620	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ ( ( D ` j ) ` Z ) = Q ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = Q )
622	67	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ j e. ( 1 ... M ) ) -> Q e. RR )
623	622	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q e. RR )
624	623	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q e. RR )
625	615	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) e. RR )
626	625	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) e. RR )
627	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> Q = inf ( V , RR , < ) )
628	443, 39	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> V C_ RR )
629	148	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> E. x e. V A. y e. V x <_ y )
630		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> j e. ( 1 ... M ) )
631	210, 488	sylanl2 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
632	630, 631	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( j e. ( 1 ... M ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
633		rabid 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 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 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> j e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } )
635		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) = ( ( D ` j ) ` Z ) )
636		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( i = j -> ( D ` i ) = ( D ` j ) )
637	636	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( i = j -> ( ( D ` i ) ` Z ) = ( ( D ` j ) ` Z ) )
638	637	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( i = j -> ( ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) <-> ( ( D ` j ) ` Z ) = ( ( D ` j ) ` Z ) ) )
639	638	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( 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 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( 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 6203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. _V )
642	16, 640, 641	elrnmptd 39366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( 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, 14	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. O )
644		elun2 3781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( D ` j ) ` Z ) e. O -> ( ( D ` j ) ` Z ) e. ( { ( B ` Z ) } u. O ) )
645	643, 644	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. ( { ( B ` Z ) } u. O ) )
646	59	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( { ( B ` Z ) } u. O ) = V )
647	645, 646	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( D ` j ) ` Z ) e. V )
648		lbinfle 10978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> inf ( V , RR , < ) <_ ( ( D ` j ) ` Z ) )
650	627, 649	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> Q <_ ( ( D ` j ) ` Z ) )
651	650	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q <_ ( ( D ` j ) ` Z ) )
652		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. ( ( D ` j ) ` Z ) = Q -> ( ( D ` j ) ` Z ) =/= Q )
653	652	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( ( D ` j ) ` Z ) =/= Q )
654	624, 626, 651, 653	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> Q < ( ( D ` j ) ` Z ) )
655	624, 626	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> ( Q < ( ( D ` j ) ` Z ) <-> -. ( ( D ` j ) ` Z ) <_ Q ) )
656	654, 655	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) /\ -. ( ( D ` j ) ` Z ) = Q ) -> -. ( ( D ` j ) ` Z ) <_ Q )
657	656	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 832	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> if ( ( ( D ` j ) ` Z ) <_ Q , ( ( D ` j ) ` Z ) , Q ) = Q )
659	612, 614, 658	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) = Q )
660	659	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) Q ) )
661	660	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( ( H ` Q ) ` ( D ` j ) ) ` Z ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) Q ) ) )
662	209, 211, 113	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ` Z ) e. RR )
663	662	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) e. RR )
664	443, 67	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> Q e. RR )
665		volico 40200	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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, 75	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> S e. RR )
668	443, 444, 445, 553	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) <_ S )
669	443, 144	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> S < Q )
670	663, 667, 664, 668, 669	lelttrd 10195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ ( P ` j ) =/= 0 ) -> ( ( C ` j ) ` Z ) < Q )
671	670	iftrued 4094	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 2660	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 6668	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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	209, 153	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( 1 ... M ) ) -> Q e. CC )
675	385, 662	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ` Z ) e. CC )
676	674, 675	subcld 10392	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - ( ( C ` j ) ` Z ) ) e. CC )
677	305, 676	mulcomd 10061	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( P ` j ) x. ( Q - ( ( C ` j ) ` Z ) ) ) = ( ( Q - ( ( C ` j ) ` Z ) ) x. ( P ` j ) ) )
678	677	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 2660	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 2659	. . . . . . . . . . . . . . 15 |- ( ( ( 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 10140	. . . . . . . . . . . . . 14 |- ( ( ( 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 693	. . . . . . . . . . . . 13 |- ( ( ( 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 832	. . . . . . . . . . . 12 |- ( ( 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	207, 402, 415, 683	fsumle 14531	. . . . . . . . . . 11 |- ( 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 39532	. . . . . . . . . 10 |- ( ph -> ( (Σ^ ` ( 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 ) ) ) ) <_ ( (Σ^ ` ( 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 4738	. . . . . . . . . . . . 13 |- ( 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 6195	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
688	211, 412	syldan 487	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
689	324, 325, 326, 330, 417, 688	sge0splitmpt 40628	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
690	687, 689	eqtrd 2656	. . . . . . . . . . 11 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
691	209, 211, 411	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
692	207, 691	sge0fsummpt 40607	. . . . . . . . . . . . 13 |- ( ph -> (Σ^ ` ( 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 2701	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR )
694		rexadd 12063	. . . . . . . . . . . 12 |- ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR /\ (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR ) -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
695	413, 693, 694	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
696	692	oveq2d 6666	. . . . . . . . . . 11 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) = ( (Σ^ ` ( 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 2661	. . . . . . . . . 10 |- ( ph -> ( (Σ^ ` ( 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 ) ) ) ) = (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
698	685, 697	breqtrd 4679	. . . . . . . . 9 |- ( ph -> ( (Σ^ ` ( 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 ) ) ) ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
699	404, 279, 200, 408, 698	lemul2ad 10964	. . . . . . . 8 |- ( ph -> ( ( 1 + E ) x. ( (Σ^ ` ( 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. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
700	399, 699	eqbrtrd 4675	. . . . . . 7 |- ( ph -> ( ( ( 1 + E ) x. (Σ^ ` ( 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. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
701	196, 278, 280, 314, 700	letrd 10194	. . . . . 6 |- ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
702	180, 701	eqbrtrd 4675	. . . . 5 |- ( ph -> ( G x. ( Q - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
703	152, 702	jca 554	. . . 4 |- ( ph -> ( Q e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( Q - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) ) )
704		oveq1 6657	. . . . . . 7 |- ( z = Q -> ( z - ( A ` Z ) ) = ( Q - ( A ` Z ) ) )
705	704	oveq2d 6666	. . . . . 6 |- ( z = Q -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( Q - ( A ` Z ) ) ) )
706		fveq2 6191	. . . . . . . . . . 11 |- ( z = Q -> ( H ` z ) = ( H ` Q ) )
707	706	fveq1d 6193	. . . . . . . . . 10 |- ( z = Q -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` Q ) ` ( D ` j ) ) )
708	707	oveq2d 6666	. . . . . . . . 9 |- ( z = Q -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) )
709	708	mpteq2dv 4745	. . . . . . . 8 |- ( 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 6195	. . . . . . 7 |- ( z = Q -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) )
711	710	oveq2d 6666	. . . . . 6 |- ( z = Q -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) )
712	705, 711	breq12d 4666	. . . . 5 |- ( z = Q -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( Q - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) ) )
713	712	elrab 3363	. . . 4 |- ( Q e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( 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. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) ) )
714	703, 713	sylibr 224	. . 3 |- ( ph -> Q e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
715	714, 68	syl6eleqr 2712	. 2 |- ( ph -> Q e. U )
716		breq2 4657	. . 3 |- ( u = Q -> ( S < u <-> S < Q ) )
717	716	rspcev 3309	. 2 |- ( ( Q e. U /\ S < Q ) -> E. u e. U S < u )
718	715, 144, 717	syl2anc 693	1 |- ( ph -> E. u e. U S < u )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   Or wor 5034   ran crn 5115   |` cres 5116   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   ^m cmap 7857   Fincfn 7955  infcinf 8347   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   ZZ>=cuz 11687   RR+crp 11832   +ecxad 11944   [,)cico 12177   [,]cicc 12178   ...cfz 12326   sum_csu 14416   prod_cprod 14635   volcvol 23232  Σ^{^}csumge0 40579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-prod 14636  df-rest 16083  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750  df-cmp 21190  df-ovol 23233  df-vol 23234  df-sumge0 40580

This theorem is referenced by:  hoidmvlelem3  40811