Theorem uniioombllem4 19478

Description: Lemma for uniioombl 19481. (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 3561	. . . 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 5216	. . . . . . 7 |- ( ( (,) o. G ) " ( 1 ... M ) ) C_ ran ( (,) o. G )
5	4	unissi 4038	. . . . . 6 |- U. ( ( (,) o. G ) " ( 1 ... M ) ) C_ U. ran ( (,) o. G )
6	3, 5	eqsstri 3378	. . . . 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 19470	. . . . . 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 19366	. . . . . 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 3358	. . . 4 |- ( ph -> U. ran ( (,) o. G ) C_ RR )
14	7, 13	sstrd 3358	. . 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 19473	. . . . 5 |- ( ph -> sup ( ran T , RR* , < ) e. RR )
25		ssid 3367	. . . . . 6 |- U. ran ( (,) o. G ) C_ U. ran ( (,) o. G )
26	22	ovollb 19375	. . . . . 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 19379	. . . . 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 19382	. . . 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 19382	. . 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 3561	. . . . 5 |- ( K i^i L ) C_ K
35	34	a1i 11	. . . 4 |- ( ph -> ( K i^i L ) C_ K )
36		ovolsscl 19382	. . . 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 3511	. . . . . 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 10521	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` 1 )
40		uniioombl.n	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. NN )
41	40	peano2nnd 10017	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
42	41, 39	syl6eleq 2526	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
43		uzsplit 11118	. . . . . . . . . . . . . . 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 2480	. . . . . . . . . . . . 13 |- ( ph -> NN = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
46	40	nncnd 10016	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. CC )
47		ax-1cn 9048	. . . . . . . . . . . . . . . 16 |- 1 e. CC
48		pncan 9311	. . . . . . . . . . . . . . . 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 6097	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... ( ( N + 1 ) - 1 ) ) = ( 1 ... N ) )
51	50	uneq1d 3500	. . . . . . . . . . . . 13 |- ( ph -> ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
52	45, 51	eqtrd 2468	. . . . . . . . . . . 12 |- ( ph -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
53	52	iuneq1d 4116	. . . . . . . . . . 11 |- ( ph -> U_ i e. NN ( (,) ` ( F ` i ) ) = U_ i e. ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) ( (,) ` ( F ` i ) ) )
54		iunxun 4172	. . . . . . . . . . 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 2484	. . . . . . . . . 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 11002	. . . . . . . . . . . . . 14 |- (,) : ( RR* X. RR* ) --> ~P RR
57		inss2 3562	. . . . . . . . . . . . . . . 16 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
58		ressxr 9129	. . . . . . . . . . . . . . . . 17 |- RR C_ RR*
59		xpss12 4981	. . . . . . . . . . . . . . . . 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 3357	. . . . . . . . . . . . . . 15 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
62		fss 5599	. . . . . . . . . . . . . . 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 5600	. . . . . . . . . . . . . 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 5591	. . . . . . . . . . . . 13 |- ( ( (,) o. F ) : NN --> ~P RR -> ( (,) o. F ) Fn NN )
67		fniunfv 5994	. . . . . . . . . . . . 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 5800	. . . . . . . . . . . . . 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 4114	. . . . . . . . . . . 12 |- ( ph -> U_ i e. NN ( ( (,) o. F ) ` i ) = U_ i e. NN ( (,) ` ( F ` i ) ) )
72	68, 71	eqtr3d 2470	. . . . . . . . . . 11 |- ( ph -> U. ran ( (,) o. F ) = U_ i e. NN ( (,) ` ( F ` i ) ) )
73	18, 72	syl5eq 2480	. . . . . . . . . 10 |- ( ph -> A = U_ i e. NN ( (,) ` ( F ` i ) ) )
74		uniioombl.l	. . . . . . . . . . . 12 |- L = U. ( ( (,) o. F ) " ( 1 ... N ) )
75		ffun 5593	. . . . . . . . . . . . . 14 |- ( ( (,) o. F ) : NN --> ~P RR -> Fun ( (,) o. F ) )
76		funiunfv 5995	. . . . . . . . . . . . . 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 11080	. . . . . . . . . . . . . . 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 4114	. . . . . . . . . . . . 13 |- ( ph -> U_ i e. ( 1 ... N ) ( ( (,) o. F ) ` i ) = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
81	77, 80	eqtr3d 2470	. . . . . . . . . . . 12 |- ( ph -> U. ( ( (,) o. F ) " ( 1 ... N ) ) = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
82	74, 81	syl5eq 2480	. . . . . . . . . . 11 |- ( ph -> L = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
83	82	uneq1d 3500	. . . . . . . . . 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 2478	. . . . . . . . 9 |- ( ph -> A = ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
85	84	ineq2d 3542	. . . . . . . 8 |- ( ph -> ( K i^i A ) = ( K i^i ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) )
86		indi 3587	. . . . . . . 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 2484	. . . . . . 7 |- ( ph -> ( K i^i A ) = ( ( K i^i L ) u. ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) )
88		fss 5599	. . . . . . . . . . . . . . 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 5600	. . . . . . . . . . . . . 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 5593	. . . . . . . . . . . . 13 |- ( ( (,) o. G ) : NN --> ~P RR -> Fun ( (,) o. G ) )
93		funiunfv 5995	. . . . . . . . . . . . 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 11080	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> j e. NN )
96		fvco3 5800	. . . . . . . . . . . . . 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 4114	. . . . . . . . . . . 12 |- ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
99	94, 98	eqtr3d 2470	. . . . . . . . . . 11 |- ( ph -> U. ( ( (,) o. G ) " ( 1 ... M ) ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
100	3, 99	syl5eq 2480	. . . . . . . . . 10 |- ( ph -> K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
101	100	ineq2d 3542	. . . . . . . . 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 3533	. . . . . . . . 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 4155	. . . . . . . . . . . . 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 3533	. . . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . 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 3533	. . . . . . . . . . . . 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 2467	. . . . . . . . . . . 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 4111	. . . . . . . . . 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 4155	. . . . . . . . . 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 2458	. . . . . . . . 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 2493	. . . . . . . 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 3501	. . . . . . 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 2468	. . . . . 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 3397	. . . . 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 3360	. . . 4 |- ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
118		ovolsscl 19382	. . . 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 9115	. 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 10648	. . 3 |- ( ph -> C e. RR )
122	37, 121	readdcld 9115	. 2 |- ( ph -> ( ( vol * ` ( K i^i L ) ) + C ) e. RR )
123	115	fveq2d 5732	. . 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 3358	. . . 4 |- ( ph -> ( K i^i L ) C_ RR )
125	117, 14	sstrd 3358	. . . 4 |- ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR )
126		ovolun 19395	. . . 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 4232	. 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 11312	. . . . 5 |- ( ph -> ( 1 ... M ) e. Fin )
130		iunss 4132	. . . . . . . 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 2804	. . . . . 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 19382	. . . . . 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 12528	. . . 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 3358	. . . . . . 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 2789	. . . . 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 19397	. . . . 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 10048	. . . . . . 7 |- ( ph -> ( C / M ) e. RR )
145	144	adantr 452	. . . . . 6 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( C / M ) e. RR )
146	82	ineq2d 3542	. . . . . . . . . . . . 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 4111	. . . . . . . . . . . . 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 4155	. . . . . . . . . . . . 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 2456	. . . . . . . . . . . 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 2486	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) = U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
153		fzfid 11312	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1 ... N ) e. Fin )
154		ffvelrn 5868	. . . . . . . . . . . . . . . . . . . . 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 3346	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. ( RR X. RR ) )
157		1st2nd2 6386	. . . . . . . . . . . . . . . . . . 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 5732	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) = ( (,) ` <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. ) )
160		df-ov 6084	. . . . . . . . . . . . . . . . 17 |- ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) = ( (,) ` <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. )
161	159, 160	syl6eqr 2486	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) = ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) )
162		ioombl 19459	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) e. dom vol
163	161, 162	syl6eqel 2524	. . . . . . . . . . . . . . 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 5868	. . . . . . . . . . . . . . . . . . . . 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 3346	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( RR X. RR ) )
168		1st2nd2 6386	. . . . . . . . . . . . . . . . . . 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 5732	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) )
171		df-ov 6084	. . . . . . . . . . . . . . . . 17 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
172	170, 171	syl6eqr 2486	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) )
173		ioombl 19459	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) e. dom vol
174	172, 173	syl6eqel 2524	. . . . . . . . . . . . . . 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 19436	. . . . . . . . . . . . . 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 2789	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> A. i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
179		finiunmbl 19438	. . . . . . . . . . . 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 2510	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) e. dom vol )
182		inss2 3562	. . . . . . . . . . 11 |- ( ( (,) ` ( G ` j ) ) i^i A ) C_ A
183	15	uniiccdif 19470	. . . . . . . . . . . . . . 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 19366	. . . . . . . . . . . . . . 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 3358	. . . . . . . . . . . . 13 |- ( ph -> U. ran ( (,) o. F ) C_ RR )
188	18, 187	syl5eqss 3392	. . . . . . . . . . . 12 |- ( ph -> A C_ RR )
189	188	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> A C_ RR )
190	182, 189	syl5ss 3359	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i A ) C_ RR )
191		inss1 3561	. . . . . . . . . . . 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 10972	. . . . . . . . . . . 12 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR
194	172, 193	syl6eqss 3398	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
195	172	fveq2d 5732	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( (,) ` ( G ` j ) ) ) = ( vol * ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) )
196		ovolfcl 19363	. . . . . . . . . . . . . . 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 19462	. . . . . . . . . . . . . 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 2468	. . . . . . . . . . . 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 9465	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR )
204	200, 203	eqeltrd 2510	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( (,) ` ( G ` j ) ) ) e. RR )
205		ovolsscl 19382	. . . . . . . . . . 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 19428	. . . . . . . . . 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 5216	. . . . . . . . . . . . . . 15 |- ( ( (,) o. F ) " ( 1 ... N ) ) C_ ran ( (,) o. F )
210	209	unissi 4038	. . . . . . . . . . . . . 14 |- U. ( ( (,) o. F ) " ( 1 ... N ) ) C_ U. ran ( (,) o. F )
211	210, 74, 18	3sstr4i 3387	. . . . . . . . . . . . 13 |- L C_ A
212		sslin 3567	. . . . . . . . . . . . 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 3545	. . . . . . . . . . . 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 5732	. . . . . . . . . 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 3597	. . . . . . . . . . . . 13 |- ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( A i^i ( (,) ` ( G ` j ) ) ) \ ( L i^i ( (,) ` ( G ` j ) ) ) )
218		incom 3533	. . . . . . . . . . . . . 14 |- ( A i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i A )
219		incom 3533	. . . . . . . . . . . . . 14 |- ( L i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i L )
220	218, 219	difeq12i 3463	. . . . . . . . . . . . 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 2456	. . . . . . . . . . . 12 |- ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) )
222	84	eqcomd 2441	. . . . . . . . . . . . . . . 16 |- ( ph -> ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = A )
223	82	ineq1d 3541	. . . . . . . . . . . . . . . . . 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 5728	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = i -> ( F ` x ) = ( F ` i ) )
225	224	fveq2d 5732	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = i -> ( (,) ` ( F ` x ) ) = ( (,) ` ( F ` i ) ) )
226	225	cbvdisjv 4193	. . . . . . . . . . . . . . . . . . . 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 3352	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 ... N ) C_ NN
229	228	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 ... N ) C_ NN )
230		uzss 10506	. . . . . . . . . . . . . . . . . . . . 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 3395	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ NN )
233		uzdisj 11119	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
234	50	ineq1d 3541	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 1 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
235	233, 234	syl5reqr 2483	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) )
236		disjiun 4202	. . . . . . . . . . . . . . . . . . 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 2468	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( L i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = (/) )
239		uneqdifeq 3716	. . . . . . . . . . . . . . . . 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 3542	. . . . . . . . . . . . 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 3533	. . . . . . . . . . . . 13 |- ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( A \ L ) )
245	106, 103	eqtri 2456	. . . . . . . . . . . . 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 2493	. . . . . . . . . . . 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 2482	. . . . . . . . . . 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 5732	. . . . . . . . . 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 6099	. . . . . . . . 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 2468	. . . . . . . 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 9465	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) e. RR )
252		inss2 3562	. . . . . . . . . . . . . 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 19382	. . . . . . . . . . . . 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 12528	. . . . . . . . . . 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 2804	. . . . . . . . . . . . 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 12236	. . . . . . . . . . . . 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 9221	. . . . . . . . . 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 5732	. . . . . . . . . . 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 19426	. . . . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . . 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 2789	. . . . . . . . . . . . 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 3561	. . . . . . . . . . . . . . . 16 |- ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( F ` i ) )
272	271	rgenw 2773	. . . . . . . . . . . . . . 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 4185	. . . . . . . . . . . . . . 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 4188	. . . . . . . . . . . . . 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 19441	. . . . . . . . . . . . 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 19426	. . . . . . . . . . . . 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 12497	. . . . . . . . . . . 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 2476	. . . . . . . . . . 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 2468	. . . . . . . . . 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 4238	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol * ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) <_ ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) )
286	284, 258	eqeltrd 2510	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol * ` ( ( (,) ` ( G ` j ) ) i^i L ) ) e. RR )
287	206, 145, 286	lesubaddd 9623	. . . . . . . . 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 4234	. . . . . . 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 9621	. . . . . . 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 12578	. . . . 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 9114	. . . . . . 7 |- ( ph -> ( C / M ) e. CC )
294		fsumconst 12573	. . . . . . 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 10228	. . . . . . . 8 |- ( M e. NN -> M e. NN0 )
297		hashfz1 11630	. . . . . . . 8 |- ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
298	143, 296, 297	3syl 19	. . . . . . 7 |- ( ph -> ( # ` ( 1 ... M ) ) = M )
299	298	oveq1d 6096	. . . . . 6 |- ( ph -> ( ( # ` ( 1 ... M ) ) x. ( C / M ) ) = ( M x. ( C / M ) ) )
300	121	recnd 9114	. . . . . . 7 |- ( ph -> C e. CC )
301	143	nncnd 10016	. . . . . . 7 |- ( ph -> M e. CC )
302	143	nnne0d 10044	. . . . . . 7 |- ( ph -> M =/= 0 )
303	300, 301, 302	divcan2d 9792	. . . . . 6 |- ( ph -> ( M x. ( C / M ) ) = C )
304	295, 299, 303	3eqtrd 2472	. . . . 5 |- ( ph -> sum_ j e. ( 1 ... M ) ( C / M ) = C )
305	292, 304	breqtrd 4236	. . . 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 9227	. . 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 9641	. 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 9227	1 |- ( ph -> ( vol * ` ( K i^i A ) ) <_ ( ( vol * ` ( K i^i L ) ) + C ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1652   e. wcel 1725   A.wral 2705   \ cdif 3317   u. cun 3318   i^i cin 3319   C_ wss 3320   (/)c0 3628   ~Pcpw 3799   <.cop 3817   U.cuni 4015   U_ciun 4093  Disj wdisj 4182   class class class wbr 4212   X. cxp 4876   dom cdm 4878   ran crn 4879   "cima 4881   o. ccom 4882   Fun wfun 5448   Fn wfn 5449   -->wf 5450   ` cfv 5454  (class class class)co 6081   1stc1st 6347   2ndc2nd 6348   Fincfn 7109   supcsup 7445   CCcc 8988   RRcr 8989   0cc0 8990   1c1 8991   + caddc 8993   x. cmul 8995   RR*cxr 9119   < clt 9120   <_ cle 9121   - cmin 9291   / cdiv 9677   NNcn 10000   NN0cn0 10221   ZZ>=cuz 10488   RR+crp 10612   (,)cioo 10916   [,]cicc 10919   ...cfz 11043   seq cseq 11323   #chash 11618   abscabs 12039   sum_csu 12479   vol *covol 19359   volcvol 19360

This theorem is referenced by:  uniioombllem5  19479

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-inf2 7596  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067  ax-pre-sup 9068

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-disj 4183  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-se 4542  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-isom 5463  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-of 6305  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-2o 6725  df-oadd 6728  df-er 6905  df-map 7020  df-pm 7021  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-fi 7416  df-sup 7446  df-oi 7479  df-card 7826  df-acn 7829  df-cda 8048  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-div 9678  df-nn 10001  df-2 10058  df-3 10059  df-n0 10222  df-z 10283  df-uz 10489  df-q 10575  df-rp 10613  df-xneg 10710  df-xadd 10711  df-xmul 10712  df-ioo 10920  df-ico 10922  df-icc 10923  df-fz 11044  df-fzo 11136  df-fl 11202  df-seq 11324  df-exp 11383  df-hash 11619  df-cj 11904  df-re 11905  df-im 11906  df-sqr 12040  df-abs 12041  df-clim 12282  df-rlim 12283  df-sum 12480  df-rest 13650  df-topgen 13667  df-psmet 16694  df-xmet 16695  df-met 16696  df-bl 16697  df-mopn 16698  df-top 16963  df-bases 16965  df-topon 16966  df-cmp 17450  df-ovol 19361  df-vol 19362