Theorem uniioombllem4 19439

Description: Lemma for uniioombl 19442. (Contributed by Mario Carneiro, 26-Mar-2015.)

Hypotheses

Ref	Expression
uniioombl.1	|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2	|- ( ph -> Disj x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3	|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
uniioombl.a	|- A = U. ran ( (,) o. F )
uniioombl.e	|- ( ph -> ( vol * ` E ) e. RR )
uniioombl.c	|- ( ph -> C e. RR+ )
uniioombl.g	|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.s	|- ( ph -> E C_ U. ran ( (,) o. G ) )
uniioombl.t	|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
uniioombl.v	|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol * ` E ) + C ) )
uniioombl.m	|- ( ph -> M e. NN )
uniioombl.m2	|- ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C )
uniioombl.k	|- K = U. ( ( (,) o. G ) " ( 1 ... M ) )
uniioombl.n	|- ( ph -> N e. NN )
uniioombl.n2	|- ( ph -> A. j e. ( 1 ... M ) ( abs ` ( sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / M ) )
uniioombl.l	|- L = U. ( ( (,) o. F ) " ( 1 ... N ) )

Assertion

Ref	Expression
uniioombllem4	|- ( ph -> ( vol * ` ( K i^i A ) ) <_ ( ( vol * ` ( K i^i L ) ) + C ) )

Distinct variable groups:   i, j, x, F   i, G, j, x   j, K, x   A, j, x   C, i, j, x   i, M, j, x   i, N, j   ph, i, j, x   T, i, j, x

Allowed substitution hints:   A( i)   S( x, i, j)   E( x, i, j)   K( i)   L( x, i, j)   N( x)

Proof of Theorem uniioombllem4

Step	Hyp	Ref	Expression
1		inss1 3529	. . . 4 |- ( K i^i A ) C_ K
2	1	a1i 11	. . 3 |- ( ph -> ( K i^i A ) C_ K )
3		uniioombl.k	. . . . . 6 |- K = U. ( ( (,) o. G ) " ( 1 ... M ) )
4		imassrn 5183	. . . . . . 7 |- ( ( (,) o. G ) " ( 1 ... M ) ) C_ ran ( (,) o. G )
5	4	unissi 4006	. . . . . 6 |- U. ( ( (,) o. G ) " ( 1 ... M ) ) C_ U. ran ( (,) o. G )
6	3, 5	eqsstri 3346	. . . . 5 |- K C_ U. ran ( (,) o. G )
7	6	a1i 11	. . . 4 |- ( ph -> K C_ U. ran ( (,) o. G ) )
8		uniioombl.g	. . . . . . 7 |- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
9	8	uniiccdif 19431	. . . . . 6 |- ( ph -> ( U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) /\ ( vol * ` ( U. ran ( [,] o. G ) \ U. ran ( (,) o. G ) ) ) = 0 ) )
10	9	simpld 446	. . . . 5 |- ( ph -> U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) )
11		ovolficcss 19327	. . . . . 6 |- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. G ) C_ RR )
12	8, 11	syl 16	. . . . 5 |- ( ph -> U. ran ( [,] o. G ) C_ RR )
13	10, 12	sstrd 3326	. . . 4 |- ( ph -> U. ran ( (,) o. G ) C_ RR )
14	7, 13	sstrd 3326	. . 3 |- ( ph -> K C_ RR )
15		uniioombl.1	. . . . . 6 |- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
16		uniioombl.2	. . . . . 6 |- ( ph -> Disj x e. NN ( (,) ` ( F ` x ) ) )
17		uniioombl.3	. . . . . 6 |- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
18		uniioombl.a	. . . . . 6 |- A = U. ran ( (,) o. F )
19		uniioombl.e	. . . . . 6 |- ( ph -> ( vol * ` E ) e. RR )
20		uniioombl.c	. . . . . 6 |- ( ph -> C e. RR+ )
21		uniioombl.s	. . . . . 6 |- ( ph -> E C_ U. ran ( (,) o. G ) )
22		uniioombl.t	. . . . . 6 |- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
23		uniioombl.v	. . . . . 6 |- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol * ` E ) + C ) )
24	15, 16, 17, 18, 19, 20, 8, 21, 22, 23	uniioombllem1 19434	. . . . 5 |- ( ph -> sup ( ran T , RR* , < ) e. RR )
25		ssid 3335	. . . . . 6 |- U. ran ( (,) o. G ) C_ U. ran ( (,) o. G )
26	22	ovollb 19336	. . . . . 6 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. G ) C_ U. ran ( (,) o. G ) ) -> ( vol * ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) )
27	8, 25, 26	sylancl 644	. . . . 5 |- ( ph -> ( vol * ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) )
28		ovollecl 19340	. . . . 5 |- ( ( U. ran ( (,) o. G ) C_ RR /\ sup ( ran T , RR* , < ) e. RR /\ ( vol * ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) -> ( vol * ` U. ran ( (,) o. G ) ) e. RR )
29	13, 24, 27, 28	syl3anc 1184	. . . 4 |- ( ph -> ( vol * ` U. ran ( (,) o. G ) ) e. RR )
30		ovolsscl 19343	. . . 4 |- ( ( K C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol * ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol * ` K ) e. RR )
31	7, 13, 29, 30	syl3anc 1184	. . 3 |- ( ph -> ( vol * ` K ) e. RR )
32		ovolsscl 19343	. . 3 |- ( ( ( K i^i A ) C_ K /\ K C_ RR /\ ( vol * ` K ) e. RR ) -> ( vol * ` ( K i^i A ) ) e. RR )
33	2, 14, 31, 32	syl3anc 1184	. 2 |- ( ph -> ( vol * ` ( K i^i A ) ) e. RR )
34		inss1 3529	. . . . 5 |- ( K i^i L ) C_ K
35	34	a1i 11	. . . 4 |- ( ph -> ( K i^i L ) C_ K )
36		ovolsscl 19343	. . . 4 |- ( ( ( K i^i L ) C_ K /\ K C_ RR /\ ( vol * ` K ) e. RR ) -> ( vol * ` ( K i^i L ) ) e. RR )
37	35, 14, 31, 36	syl3anc 1184	. . 3 |- ( ph -> ( vol * ` ( K i^i L ) ) e. RR )
38		ssun2 3479	. . . . . 6 |- U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( ( K i^i L ) u. U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
39		nnuz 10485	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` 1 )
40		uniioombl.n	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. NN )
41	40	peano2nnd 9981	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
42	41, 39	syl6eleq 2502	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
43		uzsplit 11081	. . . . . . . . . . . . . . 15 |- ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
44	42, 43	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
45	39, 44	syl5eq 2456	. . . . . . . . . . . . 13 |- ( ph -> NN = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
46	40	nncnd 9980	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. CC )
47		ax-1cn 9012	. . . . . . . . . . . . . . . 16 |- 1 e. CC
48		pncan 9275	. . . . . . . . . . . . . . . 16 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
49	46, 47, 48	sylancl 644	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
50	49	oveq2d 6064	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... ( ( N + 1 ) - 1 ) ) = ( 1 ... N ) )
51	50	uneq1d 3468	. . . . . . . . . . . . 13 |- ( ph -> ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
52	45, 51	eqtrd 2444	. . . . . . . . . . . 12 |- ( ph -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
53	52	iuneq1d 4084	. . . . . . . . . . 11 |- ( ph -> U_ i e. NN ( (,) ` ( F ` i ) ) = U_ i e. ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) ( (,) ` ( F ` i ) ) )
54		iunxun 4140	. . . . . . . . . . 11 |- U_ i e. ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) ( (,) ` ( F ` i ) ) = ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
55	53, 54	syl6eq 2460	. . . . . . . . . 10 |- ( ph -> U_ i e. NN ( (,) ` ( F ` i ) ) = ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
56		ioof 10966	. . . . . . . . . . . . . 14 |- (,) : ( RR* X. RR* ) --> ~P RR
57		inss2 3530	. . . . . . . . . . . . . . . 16 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
58		ressxr 9093	. . . . . . . . . . . . . . . . 17 |- RR C_ RR*
59		xpss12 4948	. . . . . . . . . . . . . . . . 17 |- ( ( RR C_ RR* /\ RR C_ RR* ) -> ( RR X. RR ) C_ ( RR* X. RR* ) )
60	58, 58, 59	mp2an 654	. . . . . . . . . . . . . . . 16 |- ( RR X. RR ) C_ ( RR* X. RR* )
61	57, 60	sstri 3325	. . . . . . . . . . . . . . 15 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
62		fss 5566	. . . . . . . . . . . . . . 15 |- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
63	15, 61, 62	sylancl 644	. . . . . . . . . . . . . 14 |- ( ph -> F : NN --> ( RR* X. RR* ) )
64		fco 5567	. . . . . . . . . . . . . 14 |- ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR )
65	56, 63, 64	sylancr 645	. . . . . . . . . . . . 13 |- ( ph -> ( (,) o. F ) : NN --> ~P RR )
66		ffn 5558	. . . . . . . . . . . . 13 |- ( ( (,) o. F ) : NN --> ~P RR -> ( (,) o. F ) Fn NN )
67		fniunfv 5961	. . . . . . . . . . . . 13 |- ( ( (,) o. F ) Fn NN -> U_ i e. NN ( ( (,) o. F ) ` i ) = U. ran ( (,) o. F ) )
68	65, 66, 67	3syl 19	. . . . . . . . . . . 12 |- ( ph -> U_ i e. NN ( ( (,) o. F ) ` i ) = U. ran ( (,) o. F ) )
69		fvco3 5767	. . . . . . . . . . . . . 14 |- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ i e. NN ) -> ( ( (,) o. F ) ` i ) = ( (,) ` ( F ` i ) ) )
70	15, 69	sylan 458	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. NN ) -> ( ( (,) o. F ) ` i ) = ( (,) ` ( F ` i ) ) )
71	70	iuneq2dv 4082	. . . . . . . . . . . 12 |- ( ph -> U_ i e. NN ( ( (,) o. F ) ` i ) = U_ i e. NN ( (,) ` ( F ` i ) ) )
72	68, 71	eqtr3d 2446	. . . . . . . . . . 11 |- ( ph -> U. ran ( (,) o. F ) = U_ i e. NN ( (,) ` ( F ` i ) ) )
73	18, 72	syl5eq 2456	. . . . . . . . . 10 |- ( ph -> A = U_ i e. NN ( (,) ` ( F ` i ) ) )
74		uniioombl.l	. . . . . . . . . . . 12 |- L = U. ( ( (,) o. F ) " ( 1 ... N ) )
75		ffun 5560	. . . . . . . . . . . . . 14 |- ( ( (,) o. F ) : NN --> ~P RR -> Fun ( (,) o. F ) )
76		funiunfv 5962	. . . . . . . . . . . . . 14 |- ( Fun ( (,) o. F ) -> U_ i e. ( 1 ... N ) ( ( (,) o. F ) ` i ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
77	65, 75, 76	3syl 19	. . . . . . . . . . . . 13 |- ( ph -> U_ i e. ( 1 ... N ) ( ( (,) o. F ) ` i ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
78		elfznn 11044	. . . . . . . . . . . . . . 15 |- ( i e. ( 1 ... N ) -> i e. NN )
79	15, 78, 69	syl2an 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` i ) = ( (,) ` ( F ` i ) ) )
80	79	iuneq2dv 4082	. . . . . . . . . . . . 13 |- ( ph -> U_ i e. ( 1 ... N ) ( ( (,) o. F ) ` i ) = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
81	77, 80	eqtr3d 2446	. . . . . . . . . . . 12 |- ( ph -> U. ( ( (,) o. F ) " ( 1 ... N ) ) = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
82	74, 81	syl5eq 2456	. . . . . . . . . . 11 |- ( ph -> L = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
83	82	uneq1d 3468	. . . . . . . . . 10 |- ( ph -> ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
84	55, 73, 83	3eqtr4d 2454	. . . . . . . . 9 |- ( ph -> A = ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
85	84	ineq2d 3510	. . . . . . . 8 |- ( ph -> ( K i^i A ) = ( K i^i ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) )
86		indi 3555	. . . . . . . 8 |- ( K i^i ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) = ( ( K i^i L ) u. ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
87	85, 86	syl6eq 2460	. . . . . . 7 |- ( ph -> ( K i^i A ) = ( ( K i^i L ) u. ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) )
88		fss 5566	. . . . . . . . . . . . . . 15 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> G : NN --> ( RR* X. RR* ) )
89	8, 61, 88	sylancl 644	. . . . . . . . . . . . . 14 |- ( ph -> G : NN --> ( RR* X. RR* ) )
90		fco 5567	. . . . . . . . . . . . . 14 |- ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ G : NN --> ( RR* X. RR* ) ) -> ( (,) o. G ) : NN --> ~P RR )
91	56, 89, 90	sylancr 645	. . . . . . . . . . . . 13 |- ( ph -> ( (,) o. G ) : NN --> ~P RR )
92		ffun 5560	. . . . . . . . . . . . 13 |- ( ( (,) o. G ) : NN --> ~P RR -> Fun ( (,) o. G ) )
93		funiunfv 5962	. . . . . . . . . . . . 13 |- ( Fun ( (,) o. G ) -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) )
94	91, 92, 93	3syl 19	. . . . . . . . . . . 12 |- ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) )
95		elfznn 11044	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> j e. NN )
96		fvco3 5767	. . . . . . . . . . . . . 14 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) )
97	8, 95, 96	syl2an 464	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) )
98	97	iuneq2dv 4082	. . . . . . . . . . . 12 |- ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
99	94, 98	eqtr3d 2446	. . . . . . . . . . 11 |- ( ph -> U. ( ( (,) o. G ) " ( 1 ... M ) ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
100	3, 99	syl5eq 2456	. . . . . . . . . 10 |- ( ph -> K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
101	100	ineq2d 3510	. . . . . . . . 9 |- ( ph -> ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i K ) = ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) )
102		incom 3501	. . . . . . . . 9 |- ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i K )
103		iunin2 4123	. . . . . . . . . . . . 13 |- U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
104		incom 3501	. . . . . . . . . . . . . . 15 |- ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) )
105	104	a1i 11	. . . . . . . . . . . . . 14 |- ( i e. ( ZZ>= ` ( N + 1 ) ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) )
106	105	iuneq2i 4079	. . . . . . . . . . . . 13 |- U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) )
107		incom 3501	. . . . . . . . . . . . 13 |- ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
108	103, 106, 107	3eqtr4ri 2443	. . . . . . . . . . . 12 |- ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) )
109	108	a1i 11	. . . . . . . . . . 11 |- ( j e. ( 1 ... M ) -> ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
110	109	iuneq2i 4079	. . . . . . . . . 10 |- U_ j e. ( 1 ... M ) ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) )
111		iunin2 4123	. . . . . . . . . 10 |- U_ j e. ( 1 ... M ) ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
112	110, 111	eqtr3i 2434	. . . . . . . . 9 |- U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
113	101, 102, 112	3eqtr4g 2469	. . . . . . . 8 |- ( ph -> ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
114	113	uneq2d 3469	. . . . . . 7 |- ( ph -> ( ( K i^i L ) u. ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) = ( ( K i^i L ) u. U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
115	87, 114	eqtrd 2444	. . . . . 6 |- ( ph -> ( K i^i A ) = ( ( K i^i L ) u. U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
116	38, 115	syl5sseqr 3365	. . . . 5 |- ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( K i^i A ) )
117	116, 1	syl6ss 3328	. . . 4 |- ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
118		ovolsscl 19343	. . . 4 |- ( ( U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K /\ K C_ RR /\ ( vol * ` K ) e. RR ) -> ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
119	117, 14, 31, 118	syl3anc 1184	. . 3 |- ( ph -> ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
120	37, 119	readdcld 9079	. 2 |- ( ph -> ( ( vol * ` ( K i^i L ) ) + ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) e. RR )
121	20	rpred 10612	. . 3 |- ( ph -> C e. RR )
122	37, 121	readdcld 9079	. 2 |- ( ph -> ( ( vol * ` ( K i^i L ) ) + C ) e. RR )
123	115	fveq2d 5699	. . 3 |- ( ph -> ( vol * ` ( K i^i A ) ) = ( vol * ` ( ( K i^i L ) u. U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) )
124	35, 14	sstrd 3326	. . . 4 |- ( ph -> ( K i^i L ) C_ RR )
125	117, 14	sstrd 3326	. . . 4 |- ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR )
126		ovolun 19356	. . . 4 |- ( ( ( ( K i^i L ) C_ RR /\ ( vol * ` ( K i^i L ) ) e. RR ) /\ ( U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR /\ ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR ) ) -> ( vol * ` ( ( K i^i L ) u. U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) <_ ( ( vol * ` ( K i^i L ) ) + ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) )
127	124, 37, 125, 119, 126	syl22anc 1185	. . 3 |- ( ph -> ( vol * ` ( ( K i^i L ) u. U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) <_ ( ( vol * ` ( K i^i L ) ) + ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) )
128	123, 127	eqbrtrd 4200	. 2 |- ( ph -> ( vol * ` ( K i^i A ) ) <_ ( ( vol * ` ( K i^i L ) ) + ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) )
129		fzfid 11275	. . . . 5 |- ( ph -> ( 1 ... M ) e. Fin )
130		iunss 4100	. . . . . . . 8 |- ( U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K <-> A. j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
131	117, 130	sylib 189	. . . . . . 7 |- ( ph -> A. j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
132	131	r19.21bi 2772	. . . . . 6 |- ( ( ph /\ j e. ( 1 ... M ) ) -> U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
133	14	adantr 452	. . . . . 6 |- ( ( ph /\ j e. ( 1 ... M ) ) -> K C_ RR )
134	31	adantr 452	. . . . . 6 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` K ) e. RR )
135		ovolsscl 19343	. . . . . 6 |- ( ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K /\ K C_ RR /\ ( vol * ` K ) e. RR ) -> ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
136	132, 133, 134, 135	syl3anc 1184	. . . . 5 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
137	129, 136	fsumrecl 12491	. . . 4 |- ( ph -> sum_ j e. ( 1 ... M ) ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
138	132, 133	sstrd 3326	. . . . . . 7 |- ( ( ph /\ j e. ( 1 ... M ) ) -> U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR )
139	138, 136	jca 519	. . . . . 6 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR /\ ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR ) )
140	139	ralrimiva 2757	. . . . 5 |- ( ph -> A. j e. ( 1 ... M ) ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR /\ ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR ) )
141		ovolfiniun 19358	. . . . 5 |- ( ( ( 1 ... M ) e. Fin /\ A. j e. ( 1 ... M ) ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR /\ ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR ) ) -> ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ sum_ j e. ( 1 ... M ) ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
142	129, 140, 141	syl2anc 643	. . . 4 |- ( ph -> ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ sum_ j e. ( 1 ... M ) ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
143		uniioombl.m	. . . . . . . 8 |- ( ph -> M e. NN )
144	121, 143	nndivred 10012	. . . . . . 7 |- ( ph -> ( C / M ) e. RR )
145	144	adantr 452	. . . . . 6 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( C / M ) e. RR )
146	82	ineq2d 3510	. . . . . . . . . . . . 13 |- ( ph -> ( ( (,) ` ( G ` j ) ) i^i L ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) ) )
147	146	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) ) )
148	104	a1i 11	. . . . . . . . . . . . . 14 |- ( i e. ( 1 ... N ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) )
149	148	iuneq2i 4079	. . . . . . . . . . . . 13 |- U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( 1 ... N ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) )
150		iunin2 4123	. . . . . . . . . . . . 13 |- U_ i e. ( 1 ... N ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
151	149, 150	eqtri 2432	. . . . . . . . . . . 12 |- U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
152	147, 151	syl6eqr 2462	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) = U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
153		fzfid 11275	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1 ... N ) e. Fin )
154		ffvelrn 5835	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ i e. NN ) -> ( F ` i ) e. ( <_ i^i ( RR X. RR ) ) )
155	15, 78, 154	syl2an 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. ( <_ i^i ( RR X. RR ) ) )
156	57, 155	sseldi 3314	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. ( RR X. RR ) )
157		1st2nd2 6353	. . . . . . . . . . . . . . . . . . 19 |- ( ( F ` i ) e. ( RR X. RR ) -> ( F ` i ) = <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. )
158	156, 157	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( F ` i ) = <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. )
159	158	fveq2d 5699	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) = ( (,) ` <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. ) )
160		df-ov 6051	. . . . . . . . . . . . . . . . 17 |- ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) = ( (,) ` <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. )
161	159, 160	syl6eqr 2462	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) = ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) )
162		ioombl 19420	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) e. dom vol
163	161, 162	syl6eqel 2500	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) e. dom vol )
164	163	adantlr 696	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) e. dom vol )
165		ffvelrn 5835	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
166	8, 95, 165	syl2an 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
167	57, 166	sseldi 3314	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( RR X. RR ) )
168		1st2nd2 6353	. . . . . . . . . . . . . . . . . . 19 |- ( ( G ` j ) e. ( RR X. RR ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
169	167, 168	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
170	169	fveq2d 5699	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) )
171		df-ov 6051	. . . . . . . . . . . . . . . . 17 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
172	170, 171	syl6eqr 2462	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) )
173		ioombl 19420	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) e. dom vol
174	172, 173	syl6eqel 2500	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) e. dom vol )
175	174	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( (,) ` ( G ` j ) ) e. dom vol )
176		inmbl 19397	. . . . . . . . . . . . . 14 |- ( ( ( (,) ` ( F ` i ) ) e. dom vol /\ ( (,) ` ( G ` j ) ) e. dom vol ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
177	164, 175, 176	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
178	177	ralrimiva 2757	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> A. i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
179		finiunmbl 19399	. . . . . . . . . . . 12 |- ( ( ( 1 ... N ) e. Fin /\ A. i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol ) -> U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
180	153, 178, 179	syl2anc 643	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
181	152, 180	eqeltrd 2486	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) e. dom vol )
182		inss2 3530	. . . . . . . . . . 11 |- ( ( (,) ` ( G ` j ) ) i^i A ) C_ A
183	15	uniiccdif 19431	. . . . . . . . . . . . . . 15 |- ( ph -> ( U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) /\ ( vol * ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 ) )
184	183	simpld 446	. . . . . . . . . . . . . 14 |- ( ph -> U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) )
185		ovolficcss 19327	. . . . . . . . . . . . . . 15 |- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )
186	15, 185	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> U. ran ( [,] o. F ) C_ RR )
187	184, 186	sstrd 3326	. . . . . . . . . . . . 13 |- ( ph -> U. ran ( (,) o. F ) C_ RR )
188	18, 187	syl5eqss 3360	. . . . . . . . . . . 12 |- ( ph -> A C_ RR )
189	188	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> A C_ RR )
190	182, 189	syl5ss 3327	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i A ) C_ RR )
191		inss1 3529	. . . . . . . . . . . 12 |- ( ( (,) ` ( G ` j ) ) i^i A ) C_ ( (,) ` ( G ` j ) )
192	191	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i A ) C_ ( (,) ` ( G ` j ) ) )
193		ioossre 10936	. . . . . . . . . . . 12 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR
194	172, 193	syl6eqss 3366	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
195	172	fveq2d 5699	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( (,) ` ( G ` j ) ) ) = ( vol * ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) )
196		ovolfcl 19324	. . . . . . . . . . . . . . 15 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) )
197	8, 95, 196	syl2an 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) )
198		ovolioo 19423	. . . . . . . . . . . . . 14 |- ( ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) -> ( vol * ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
199	197, 198	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
200	195, 199	eqtrd 2444	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( (,) ` ( G ` j ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
201	197	simp2d 970	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 2nd ` ( G ` j ) ) e. RR )
202	197	simp1d 969	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1st ` ( G ` j ) ) e. RR )
203	201, 202	resubcld 9429	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR )
204	200, 203	eqeltrd 2486	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( (,) ` ( G ` j ) ) ) e. RR )
205		ovolsscl 19343	. . . . . . . . . . 11 |- ( ( ( ( (,) ` ( G ` j ) ) i^i A ) C_ ( (,) ` ( G ` j ) ) /\ ( (,) ` ( G ` j ) ) C_ RR /\ ( vol * ` ( (,) ` ( G ` j ) ) ) e. RR ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) e. RR )
206	192, 194, 204, 205	syl3anc 1184	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) e. RR )
207		mblsplit 19389	. . . . . . . . . 10 |- ( ( ( ( (,) ` ( G ` j ) ) i^i L ) e. dom vol /\ ( ( (,) ` ( G ` j ) ) i^i A ) C_ RR /\ ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) e. RR ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) = ( ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) ) + ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) ) ) ) )
208	181, 190, 206, 207	syl3anc 1184	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) = ( ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) ) + ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) ) ) ) )
209		imassrn 5183	. . . . . . . . . . . . . . 15 |- ( ( (,) o. F ) " ( 1 ... N ) ) C_ ran ( (,) o. F )
210	209	unissi 4006	. . . . . . . . . . . . . 14 |- U. ( ( (,) o. F ) " ( 1 ... N ) ) C_ U. ran ( (,) o. F )
211	210, 74, 18	3sstr4i 3355	. . . . . . . . . . . . 13 |- L C_ A
212		sslin 3535	. . . . . . . . . . . . 13 |- ( L C_ A -> ( ( (,) ` ( G ` j ) ) i^i L ) C_ ( ( (,) ` ( G ` j ) ) i^i A ) )
213	211, 212	mp1i 12	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) C_ ( ( (,) ` ( G ` j ) ) i^i A ) )
214		dfss1 3513	. . . . . . . . . . . 12 |- ( ( ( (,) ` ( G ` j ) ) i^i L ) C_ ( ( (,) ` ( G ` j ) ) i^i A ) <-> ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) = ( ( (,) ` ( G ` j ) ) i^i L ) )
215	213, 214	sylib 189	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) = ( ( (,) ` ( G ` j ) ) i^i L ) )
216	215	fveq2d 5699	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) ) = ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) )
217		indifdir 3565	. . . . . . . . . . . . 13 |- ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( A i^i ( (,) ` ( G ` j ) ) ) \ ( L i^i ( (,) ` ( G ` j ) ) ) )
218		incom 3501	. . . . . . . . . . . . . 14 |- ( A i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i A )
219		incom 3501	. . . . . . . . . . . . . 14 |- ( L i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i L )
220	218, 219	difeq12i 3431	. . . . . . . . . . . . 13 |- ( ( A i^i ( (,) ` ( G ` j ) ) ) \ ( L i^i ( (,) ` ( G ` j ) ) ) ) = ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) )
221	217, 220	eqtri 2432	. . . . . . . . . . . 12 |- ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) )
222	84	eqcomd 2417	. . . . . . . . . . . . . . . 16 |- ( ph -> ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = A )
223	82	ineq1d 3509	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( L i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
224		fveq2 5695	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = i -> ( F ` x ) = ( F ` i ) )
225	224	fveq2d 5699	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = i -> ( (,) ` ( F ` x ) ) = ( (,) ` ( F ` i ) ) )
226	225	cbvdisjv 4161	. . . . . . . . . . . . . . . . . . . 20 |- (Disj x e. NN ( (,) ` ( F ` x ) ) <-> Disj i e. NN ( (,) ` ( F ` i ) ) )
227	16, 226	sylib 189	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> Disj i e. NN ( (,) ` ( F ` i ) ) )
228	78	ssriv 3320	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 ... N ) C_ NN
229	228	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 ... N ) C_ NN )
230		uzss 10470	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` 1 ) )
231	42, 230	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` 1 ) )
232	231, 39	syl6sseqr 3363	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ NN )
233		uzdisj 11082	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
234	50	ineq1d 3509	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 1 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
235	233, 234	syl5reqr 2459	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) )
236		disjiun 4170	. . . . . . . . . . . . . . . . . . 19 |- ( (Disj i e. NN ( (,) ` ( F ` i ) ) /\ ( ( 1 ... N ) C_ NN /\ ( ZZ>= ` ( N + 1 ) ) C_ NN /\ ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) ) -> ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = (/) )
237	227, 229, 232, 235, 236	syl13anc 1186	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = (/) )
238	223, 237	eqtrd 2444	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = (/) )
239		uneqdifeq 3684	. . . . . . . . . . . . . . . . 17 |- ( ( L C_ A /\ ( L i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = (/) ) -> ( ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = A <-> ( A \ L ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
240	211, 238, 239	sylancr 645	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = A <-> ( A \ L ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
241	222, 240	mpbid 202	. . . . . . . . . . . . . . 15 |- ( ph -> ( A \ L ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
242	241	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( A \ L ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
243	242	ineq2d 3510	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i ( A \ L ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
244		incom 3501	. . . . . . . . . . . . 13 |- ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( A \ L ) )
245	106, 103	eqtri 2432	. . . . . . . . . . . . 13 |- U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
246	243, 244, 245	3eqtr4g 2469	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
247	221, 246	syl5eqr 2458	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
248	247	fveq2d 5699	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) ) ) = ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
249	216, 248	oveq12d 6066	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) ) + ( vol * ` ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) ) ) ) = ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) )
250	208, 249	eqtrd 2444	. . . . . . . 8 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) = ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) )
251	206, 145	resubcld 9429	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) e. RR )
252		inss2 3530	. . . . . . . . . . . . . 14 |- ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) )
253	252	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) ) )
254	194	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
255	204	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol * ` ( (,) ` ( G ` j ) ) ) e. RR )
256		ovolsscl 19343	. . . . . . . . . . . . 13 |- ( ( ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) ) /\ ( (,) ` ( G ` j ) ) C_ RR /\ ( vol * ` ( (,) ` ( G ` j ) ) ) e. RR ) -> ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
257	253, 254, 255, 256	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
258	153, 257	fsumrecl 12491	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
259		uniioombl.n2	. . . . . . . . . . . . . 14 |- ( ph -> A. j e. ( 1 ... M ) ( abs ` ( sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / M ) )
260	259	r19.21bi 2772	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( abs ` ( sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / M ) )
261	258, 206, 145	absdifltd 12199	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( abs ` ( sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / M ) <-> ( ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) < sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) /\ sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) < ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) + ( C / M ) ) ) ) )
262	260, 261	mpbid 202	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) < sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) /\ sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) < ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) + ( C / M ) ) ) )
263	262	simpld 446	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) < sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
264	251, 258, 263	ltled 9185	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) <_ sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
265	152	fveq2d 5699	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) = ( vol * ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
266		mblvol 19387	. . . . . . . . . . . . . . . . 17 |- ( ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol -> ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
267	177, 266	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
268	267, 257	eqeltrd 2486	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
269	177, 268	jca 519	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol /\ ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR ) )
270	269	ralrimiva 2757	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> A. i e. ( 1 ... N ) ( ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol /\ ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR ) )
271		inss1 3529	. . . . . . . . . . . . . . . 16 |- ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( F ` i ) )
272	271	rgenw 2741	. . . . . . . . . . . . . . 15 |- A. i e. NN ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( F ` i ) )
273	227	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> Disj i e. NN ( (,) ` ( F ` i ) ) )
274		disjss2 4153	. . . . . . . . . . . . . . 15 |- ( A. i e. NN ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( F ` i ) ) -> (Disj i e. NN ( (,) ` ( F ` i ) ) -> Disj i e. NN ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
275	272, 273, 274	mpsyl 61	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> Disj i e. NN ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
276		disjss1 4156	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) C_ NN -> (Disj i e. NN ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) -> Disj i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
277	228, 275, 276	mpsyl 61	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> Disj i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
278		volfiniun 19402	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) e. Fin /\ A. i e. ( 1 ... N ) ( ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol /\ ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR ) /\ Disj i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) -> ( vol ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ i e. ( 1 ... N ) ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
279	153, 270, 277, 278	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ i e. ( 1 ... N ) ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
280		mblvol 19387	. . . . . . . . . . . . 13 |- ( U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol -> ( vol ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol * ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
281	180, 280	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol * ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
282	267	sumeq2dv 12460	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> sum_ i e. ( 1 ... N ) ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
283	279, 281, 282	3eqtr3d 2452	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
284	265, 283	eqtrd 2444	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) = sum_ i e. ( 1 ... N ) ( vol * ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
285	264, 284	breqtrrd 4206	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) <_ ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) )
286	284, 258	eqeltrd 2486	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) e. RR )
287	206, 145, 286	lesubaddd 9587	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) <_ ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) <-> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) <_ ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( C / M ) ) ) )
288	285, 287	mpbid 202	. . . . . . . 8 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) <_ ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( C / M ) ) )
289	250, 288	eqbrtrrd 4202	. . . . . . 7 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) <_ ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( C / M ) ) )
290	136, 145, 286	leadd2d 9585	. . . . . . 7 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ ( C / M ) <-> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) <_ ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( C / M ) ) ) )
291	289, 290	mpbird 224	. . . . . 6 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ ( C / M ) )
292	129, 136, 145, 291	fsumle 12541	. . . . 5 |- ( ph -> sum_ j e. ( 1 ... M ) ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ sum_ j e. ( 1 ... M ) ( C / M ) )
293	144	recnd 9078	. . . . . . 7 |- ( ph -> ( C / M ) e. CC )
294		fsumconst 12536	. . . . . . 7 |- ( ( ( 1 ... M ) e. Fin /\ ( C / M ) e. CC ) -> sum_ j e. ( 1 ... M ) ( C / M ) = ( ( # ` ( 1 ... M ) ) x. ( C / M ) ) )
295	129, 293, 294	syl2anc 643	. . . . . 6 |- ( ph -> sum_ j e. ( 1 ... M ) ( C / M ) = ( ( # ` ( 1 ... M ) ) x. ( C / M ) ) )
296		nnnn0 10192	. . . . . . . 8 |- ( M e. NN -> M e. NN0 )
297		hashfz1 11593	. . . . . . . 8 |- ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
298	143, 296, 297	3syl 19	. . . . . . 7 |- ( ph -> ( # ` ( 1 ... M ) ) = M )
299	298	oveq1d 6063	. . . . . 6 |- ( ph -> ( ( # ` ( 1 ... M ) ) x. ( C / M ) ) = ( M x. ( C / M ) ) )
300	121	recnd 9078	. . . . . . 7 |- ( ph -> C e. CC )
301	143	nncnd 9980	. . . . . . 7 |- ( ph -> M e. CC )
302	143	nnne0d 10008	. . . . . . 7 |- ( ph -> M =/= 0 )
303	300, 301, 302	divcan2d 9756	. . . . . 6 |- ( ph -> ( M x. ( C / M ) ) = C )
304	295, 299, 303	3eqtrd 2448	. . . . 5 |- ( ph -> sum_ j e. ( 1 ... M ) ( C / M ) = C )
305	292, 304	breqtrd 4204	. . . 4 |- ( ph -> sum_ j e. ( 1 ... M ) ( vol * ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ C )
306	119, 137, 121, 142, 305	letrd 9191	. . 3 |- ( ph -> ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ C )
307	119, 121, 37, 306	leadd2dd 9605	. 2 |- ( ph -> ( ( vol * ` ( K i^i L ) ) + ( vol * ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) <_ ( ( vol * ` ( K i^i L ) ) + C ) )
308	33, 120, 122, 128, 307	letrd 9191	1 |- ( ph -> ( vol * ` ( K i^i A ) ) <_ ( ( vol * ` ( K i^i L ) ) + C ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2674   \ cdif 3285   u. cun 3286   i^i cin 3287   C_ wss 3288   (/)c0 3596   ~Pcpw 3767   <.cop 3785   U.cuni 3983   U_ciun 4061  Disj wdisj 4150   class class class wbr 4180   X. cxp 4843   dom cdm 4845   ran crn 4846   "cima 4848   o. ccom 4849   Fun wfun 5415   Fn wfn 5416   -->wf 5417   ` cfv 5421  (class class class)co 6048   1stc1st 6314   2ndc2nd 6315   Fincfn 7076   supcsup 7411   CCcc 8952   RRcr 8953   0cc0 8954   1c1 8955   + caddc 8957   x. cmul 8959   RR*cxr 9083   < clt 9084   <_ cle 9085   - cmin 9255   / cdiv 9641   NNcn 9964   NN0cn0 10185   ZZ>=cuz 10452   RR+crp 10576   (,)cioo 10880   [,]cicc 10883   ...cfz 11007   seq cseq 11286   #chash 11581   abscabs 12002   sum_csu 12442   vol *covol 19320   volcvol 19321

This theorem is referenced by:  uniioombllem5  19440

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-inf2 7560  ax-cnex 9010  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030  ax-pre-mulgt0 9031  ax-pre-sup 9032

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-disj 4151  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-of 6272  df-1st 6316  df-2nd 6317  df-riota 6516  df-recs 6600  df-rdg 6635  df-1o 6691  df-2o 6692  df-oadd 6695  df-er 6872  df-map 6987  df-pm 6988  df-en 7077  df-dom 7078  df-sdom 7079  df-fin 7080  df-fi 7382  df-sup 7412  df-oi 7443  df-card 7790  df-acn 7793  df-cda 8012  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090  df-sub 9257  df-neg 9258  df-div 9642  df-nn 9965  df-2 10022  df-3 10023  df-n0 10186  df-z 10247  df-uz 10453  df-q 10539  df-rp 10577  df-xneg 10674  df-xadd 10675  df-xmul 10676  df-ioo 10884  df-ico 10886  df-icc 10887  df-fz 11008  df-fzo 11099  df-fl 11165  df-seq 11287  df-exp 11346  df-hash 11582  df-cj 11867  df-re 11868  df-im 11869  df-sqr 12003  df-abs 12004  df-clim 12245  df-rlim 12246  df-sum 12443  df-rest 13613  df-topgen 13630  df-psmet 16657  df-xmet 16658  df-met 16659  df-bl 16660  df-mopn 16661  df-top 16926  df-bases 16928  df-topon 16929  df-cmp 17412  df-ovol 19322  df-vol 19323