Theorem hoidmvlelem2

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

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

Proof

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