This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniioombllem4

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

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

Proof

Step Hyp Ref Expression
1 uniioombl.1 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
2 uniioombl.2 
 |-  ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
3 uniioombl.3 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
4 uniioombl.a 
 |-  A = U. ran ( (,) o. F )
5 uniioombl.e 
 |-  ( ph -> ( vol* ` E ) e. RR )
6 uniioombl.c 
 |-  ( ph -> C e. RR+ )
7 uniioombl.g 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
8 uniioombl.s 
 |-  ( ph -> E C_ U. ran ( (,) o. G ) )
9 uniioombl.t 
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
10 uniioombl.v 
 |-  ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
11 uniioombl.m 
 |-  ( ph -> M e. NN )
12 uniioombl.m2 
 |-  ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C )
13 uniioombl.k 
 |-  K = U. ( ( (,) o. G ) " ( 1 ... M ) )
14 uniioombl.n 
 |-  ( ph -> N e. NN )
15 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 ) )
16 uniioombl.l 
 |-  L = U. ( ( (,) o. F ) " ( 1 ... N ) )
17 inss1 
 |-  ( K i^i A ) C_ K
18 imassrn 
 |-  ( ( (,) o. G ) " ( 1 ... M ) ) C_ ran ( (,) o. G )
19 18 unissi 
 |-  U. ( ( (,) o. G ) " ( 1 ... M ) ) C_ U. ran ( (,) o. G )
20 13 19 eqsstri 
 |-  K C_ U. ran ( (,) o. G )
21 7 uniiccdif 
 |-  ( ph -> ( U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) /\ ( vol* ` ( U. ran ( [,] o. G ) \ U. ran ( (,) o. G ) ) ) = 0 ) )
22 21 simpld 
 |-  ( ph -> U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) )
23 ovolficcss 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. G ) C_ RR )
24 7 23 syl 
 |-  ( ph -> U. ran ( [,] o. G ) C_ RR )
25 22 24 sstrd 
 |-  ( ph -> U. ran ( (,) o. G ) C_ RR )
26 20 25 sstrid 
 |-  ( ph -> K C_ RR )
27 1 2 3 4 5 6 7 8 9 10 uniioombllem1 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR )
28 ssid 
 |-  U. ran ( (,) o. G ) C_ U. ran ( (,) o. G )
29 9 ovollb 
 |-  ( ( 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* , < ) )
30 7 28 29 sylancl 
 |-  ( ph -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) )
31 ovollecl 
 |-  ( ( 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 )
32 25 27 30 31 syl3anc 
 |-  ( ph -> ( vol* ` U. ran ( (,) o. G ) ) e. RR )
33 ovolsscl 
 |-  ( ( K C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol* ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol* ` K ) e. RR )
34 20 25 32 33 mp3an2i 
 |-  ( ph -> ( vol* ` K ) e. RR )
35 ovolsscl 
 |-  ( ( ( K i^i A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i A ) ) e. RR )
36 17 26 34 35 mp3an2i 
 |-  ( ph -> ( vol* ` ( K i^i A ) ) e. RR )
37 inss1 
 |-  ( K i^i L ) C_ K
38 ovolsscl 
 |-  ( ( ( K i^i L ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i L ) ) e. RR )
39 37 26 34 38 mp3an2i 
 |-  ( ph -> ( vol* ` ( K i^i L ) ) e. RR )
40 ssun2 
 |-  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 ) ) ) )
41 nnuz 
 |-  NN = ( ZZ>= ` 1 )
42 14 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
43 42 41 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
44 uzsplit 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
45 43 44 syl 
 |-  ( ph -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
46 41 45 eqtrid 
 |-  ( ph -> NN = ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
47 14 nncnd 
 |-  ( ph -> N e. CC )
48 ax-1cn 
 |-  1 e. CC
49 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
50 47 48 49 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
51 50 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N + 1 ) - 1 ) ) = ( 1 ... N ) )
52 51 uneq1d 
 |-  ( ph -> ( ( 1 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
53 46 52 eqtrd 
 |-  ( ph -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
54 53 iuneq1d 
 |-  ( ph -> U_ i e. NN ( (,) ` ( F ` i ) ) = U_ i e. ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) ( (,) ` ( F ` i ) ) )
55 iunxun 
 |-  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 ) ) )
56 54 55 eqtrdi 
 |-  ( ph -> U_ i e. NN ( (,) ` ( F ` i ) ) = ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
57 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
58 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
59 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
60 58 59 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
61 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
62 1 60 61 sylancl 
 |-  ( ph -> F : NN --> ( RR* X. RR* ) )
63 fco 
 |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR )
64 57 62 63 sylancr 
 |-  ( ph -> ( (,) o. F ) : NN --> ~P RR )
65 ffn 
 |-  ( ( (,) o. F ) : NN --> ~P RR -> ( (,) o. F ) Fn NN )
66 fniunfv 
 |-  ( ( (,) o. F ) Fn NN -> U_ i e. NN ( ( (,) o. F ) ` i ) = U. ran ( (,) o. F ) )
67 64 65 66 3syl 
 |-  ( ph -> U_ i e. NN ( ( (,) o. F ) ` i ) = U. ran ( (,) o. F ) )
68 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ i e. NN ) -> ( ( (,) o. F ) ` i ) = ( (,) ` ( F ` i ) ) )
69 1 68 sylan 
 |-  ( ( ph /\ i e. NN ) -> ( ( (,) o. F ) ` i ) = ( (,) ` ( F ` i ) ) )
70 69 iuneq2dv 
 |-  ( ph -> U_ i e. NN ( ( (,) o. F ) ` i ) = U_ i e. NN ( (,) ` ( F ` i ) ) )
71 67 70 eqtr3d 
 |-  ( ph -> U. ran ( (,) o. F ) = U_ i e. NN ( (,) ` ( F ` i ) ) )
72 4 71 eqtrid 
 |-  ( ph -> A = U_ i e. NN ( (,) ` ( F ` i ) ) )
73 ffun 
 |-  ( ( (,) o. F ) : NN --> ~P RR -> Fun ( (,) o. F ) )
74 funiunfv 
 |-  ( Fun ( (,) o. F ) -> U_ i e. ( 1 ... N ) ( ( (,) o. F ) ` i ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
75 64 73 74 3syl 
 |-  ( ph -> U_ i e. ( 1 ... N ) ( ( (,) o. F ) ` i ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
76 elfznn 
 |-  ( i e. ( 1 ... N ) -> i e. NN )
77 1 76 68 syl2an 
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` i ) = ( (,) ` ( F ` i ) ) )
78 77 iuneq2dv 
 |-  ( ph -> U_ i e. ( 1 ... N ) ( ( (,) o. F ) ` i ) = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
79 75 78 eqtr3d 
 |-  ( ph -> U. ( ( (,) o. F ) " ( 1 ... N ) ) = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
80 16 79 eqtrid 
 |-  ( ph -> L = U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
81 80 uneq1d 
 |-  ( 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 ) ) ) )
82 56 72 81 3eqtr4d 
 |-  ( ph -> A = ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
83 82 ineq2d 
 |-  ( ph -> ( K i^i A ) = ( K i^i ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) )
84 indi 
 |-  ( 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 ) ) ) )
85 83 84 eqtrdi 
 |-  ( ph -> ( K i^i A ) = ( ( K i^i L ) u. ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) ) )
86 fss 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> G : NN --> ( RR* X. RR* ) )
87 7 60 86 sylancl 
 |-  ( ph -> G : NN --> ( RR* X. RR* ) )
88 fco 
 |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ G : NN --> ( RR* X. RR* ) ) -> ( (,) o. G ) : NN --> ~P RR )
89 57 87 88 sylancr 
 |-  ( ph -> ( (,) o. G ) : NN --> ~P RR )
90 ffun 
 |-  ( ( (,) o. G ) : NN --> ~P RR -> Fun ( (,) o. G ) )
91 funiunfv 
 |-  ( Fun ( (,) o. G ) -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) )
92 89 90 91 3syl 
 |-  ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) )
93 elfznn 
 |-  ( j e. ( 1 ... M ) -> j e. NN )
94 fvco3 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) )
95 7 93 94 syl2an 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) )
96 95 iuneq2dv 
 |-  ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
97 92 96 eqtr3d 
 |-  ( ph -> U. ( ( (,) o. G ) " ( 1 ... M ) ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
98 13 97 eqtrid 
 |-  ( ph -> K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) )
99 98 ineq2d 
 |-  ( 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 ) ) ) )
100 incom 
 |-  ( K i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i K )
101 iunin2 
 |-  U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
102 incom 
 |-  ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) )
103 102 a1i 
 |-  ( i e. ( ZZ>= ` ( N + 1 ) ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) )
104 103 iuneq2i 
 |-  U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) )
105 incom 
 |-  ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
106 101 104 105 3eqtr4ri 
 |-  ( U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) )
107 106 a1i 
 |-  ( 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 ) ) ) )
108 107 iuneq2i 
 |-  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 ) ) )
109 iunin2 
 |-  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 ) ) )
110 108 109 eqtr3i 
 |-  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 ) ) )
111 99 100 110 3eqtr4g 
 |-  ( 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 ) ) ) )
112 111 uneq2d 
 |-  ( 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 ) ) ) ) )
113 85 112 eqtrd 
 |-  ( 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 ) ) ) ) )
114 40 113 sseqtrrid 
 |-  ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( K i^i A ) )
115 114 17 sstrdi 
 |-  ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
116 ovolsscl 
 |-  ( ( 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 )
117 115 26 34 116 syl3anc 
 |-  ( ph -> ( vol* ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
118 39 117 readdcld 
 |-  ( 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 )
119 6 rpred 
 |-  ( ph -> C e. RR )
120 39 119 readdcld 
 |-  ( ph -> ( ( vol* ` ( K i^i L ) ) + C ) e. RR )
121 113 fveq2d 
 |-  ( 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 ) ) ) ) ) )
122 37 26 sstrid 
 |-  ( ph -> ( K i^i L ) C_ RR )
123 115 26 sstrd 
 |-  ( ph -> U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR )
124 ovolun 
 |-  ( ( ( ( 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 ) ) ) ) ) )
125 122 39 123 117 124 syl22anc 
 |-  ( 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 ) ) ) ) ) )
126 121 125 eqbrtrd 
 |-  ( 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 ) ) ) ) ) )
127 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
128 iunss 
 |-  ( 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 )
129 115 128 sylib 
 |-  ( ph -> A. j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
130 129 r19.21bi 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ K )
131 26 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> K C_ RR )
132 34 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` K ) e. RR )
133 ovolsscl 
 |-  ( ( 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 )
134 130 131 132 133 syl3anc 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
135 127 134 fsumrecl 
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( vol* ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
136 130 131 sstrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ RR )
137 136 134 jca 
 |-  ( ( 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 ) )
138 137 ralrimiva 
 |-  ( 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 ) )
139 ovolfiniun 
 |-  ( ( ( 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 ) ) ) ) )
140 127 138 139 syl2anc 
 |-  ( 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 ) ) ) ) )
141 119 11 nndivred 
 |-  ( ph -> ( C / M ) e. RR )
142 141 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( C / M ) e. RR )
143 80 ineq2d 
 |-  ( ph -> ( ( (,) ` ( G ` j ) ) i^i L ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) ) )
144 143 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) ) )
145 102 a1i 
 |-  ( i e. ( 1 ... N ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) )
146 145 iuneq2i 
 |-  U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( 1 ... N ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) )
147 iunin2 
 |-  U_ i e. ( 1 ... N ) ( ( (,) ` ( G ` j ) ) i^i ( (,) ` ( F ` i ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
148 146 147 eqtri 
 |-  U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) )
149 144 148 eqtr4di 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) = U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
150 fzfid 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1 ... N ) e. Fin )
151 ffvelcdm 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ i e. NN ) -> ( F ` i ) e. ( <_ i^i ( RR X. RR ) ) )
152 1 76 151 syl2an 
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. ( <_ i^i ( RR X. RR ) ) )
153 152 elin2d 
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. ( RR X. RR ) )
154 1st2nd2 
 |-  ( ( F ` i ) e. ( RR X. RR ) -> ( F ` i ) = <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. )
155 153 154 syl 
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( F ` i ) = <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. )
156 155 fveq2d 
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) = ( (,) ` <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. ) )
157 df-ov 
 |-  ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) = ( (,) ` <. ( 1st ` ( F ` i ) ) , ( 2nd ` ( F ` i ) ) >. )
158 156 157 eqtr4di 
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) = ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) )
159 ioombl 
 |-  ( ( 1st ` ( F ` i ) ) (,) ( 2nd ` ( F ` i ) ) ) e. dom vol
160 158 159 eqeltrdi 
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) e. dom vol )
161 160 adantlr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( (,) ` ( F ` i ) ) e. dom vol )
162 ffvelcdm 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
163 7 93 162 syl2an 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
164 163 elin2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( RR X. RR ) )
165 1st2nd2 
 |-  ( ( G ` j ) e. ( RR X. RR ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
166 164 165 syl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
167 166 fveq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) )
168 df-ov 
 |-  ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
169 167 168 eqtr4di 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) )
170 ioombl 
 |-  ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) e. dom vol
171 169 170 eqeltrdi 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) e. dom vol )
172 171 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( (,) ` ( G ` j ) ) e. dom vol )
173 inmbl 
 |-  ( ( ( (,) ` ( F ` i ) ) e. dom vol /\ ( (,) ` ( G ` j ) ) e. dom vol ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
174 161 172 173 syl2anc 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
175 174 ralrimiva 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> A. i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
176 finiunmbl 
 |-  ( ( ( 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 )
177 150 175 176 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol )
178 149 177 eqeltrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) e. dom vol )
179 inss2 
 |-  ( ( (,) ` ( G ` j ) ) i^i A ) C_ A
180 1 uniiccdif 
 |-  ( ph -> ( U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) /\ ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 ) )
181 180 simpld 
 |-  ( ph -> U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) )
182 ovolficcss 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )
183 1 182 syl 
 |-  ( ph -> U. ran ( [,] o. F ) C_ RR )
184 181 183 sstrd 
 |-  ( ph -> U. ran ( (,) o. F ) C_ RR )
185 4 184 eqsstrid 
 |-  ( ph -> A C_ RR )
186 185 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> A C_ RR )
187 179 186 sstrid 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i A ) C_ RR )
188 inss1 
 |-  ( ( (,) ` ( G ` j ) ) i^i A ) C_ ( (,) ` ( G ` j ) )
189 ioossre 
 |-  ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR
190 169 189 eqsstrdi 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
191 169 fveq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) )
192 ovolfcl 
 |-  ( ( 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 ) ) ) )
193 7 93 192 syl2an 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) )
194 ovolioo 
 |-  ( ( ( 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 ) ) ) )
195 193 194 syl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
196 191 195 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
197 193 simp2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( 2nd ` ( G ` j ) ) e. RR )
198 193 simp1d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1st ` ( G ` j ) ) e. RR )
199 197 198 resubcld 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR )
200 196 199 eqeltrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
201 ovolsscl 
 |-  ( ( ( ( (,) ` ( 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 )
202 188 190 200 201 mp3an2i 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) e. RR )
203 mblsplit 
 |-  ( ( ( ( (,) ` ( 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 ) ) ) ) )
204 178 187 202 203 syl3anc 
 |-  ( ( 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 ) ) ) ) )
205 imassrn 
 |-  ( ( (,) o. F ) " ( 1 ... N ) ) C_ ran ( (,) o. F )
206 205 unissi 
 |-  U. ( ( (,) o. F ) " ( 1 ... N ) ) C_ U. ran ( (,) o. F )
207 206 16 4 3sstr4i 
 |-  L C_ A
208 sslin 
 |-  ( L C_ A -> ( ( (,) ` ( G ` j ) ) i^i L ) C_ ( ( (,) ` ( G ` j ) ) i^i A ) )
209 207 208 mp1i 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i L ) C_ ( ( (,) ` ( G ` j ) ) i^i A ) )
210 sseqin2 
 |-  ( ( ( (,) ` ( 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 ) )
211 209 210 sylib 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) = ( ( (,) ` ( G ` j ) ) i^i L ) )
212 211 fveq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( ( (,) ` ( G ` j ) ) i^i A ) i^i ( ( (,) ` ( G ` j ) ) i^i L ) ) ) = ( vol* ` ( ( (,) ` ( G ` j ) ) i^i L ) ) )
213 indifdir 
 |-  ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( A i^i ( (,) ` ( G ` j ) ) ) \ ( L i^i ( (,) ` ( G ` j ) ) ) )
214 incom 
 |-  ( A i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i A )
215 incom 
 |-  ( L i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i L )
216 214 215 difeq12i 
 |-  ( ( A i^i ( (,) ` ( G ` j ) ) ) \ ( L i^i ( (,) ` ( G ` j ) ) ) ) = ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) )
217 213 216 eqtri 
 |-  ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( ( (,) ` ( G ` j ) ) i^i A ) \ ( ( (,) ` ( G ` j ) ) i^i L ) )
218 82 eqcomd 
 |-  ( ph -> ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = A )
219 80 ineq1d 
 |-  ( 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 ) ) ) )
220 2fveq3 
 |-  ( x = i -> ( (,) ` ( F ` x ) ) = ( (,) ` ( F ` i ) ) )
221 220 cbvdisjv 
 |-  ( Disj_ x e. NN ( (,) ` ( F ` x ) ) <-> Disj_ i e. NN ( (,) ` ( F ` i ) ) )
222 2 221 sylib 
 |-  ( ph -> Disj_ i e. NN ( (,) ` ( F ` i ) ) )
223 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
224 223 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
225 uzss 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` 1 ) )
226 43 225 syl 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` 1 ) )
227 226 41 sseqtrrdi 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ NN )
228 51 ineq1d 
 |-  ( ph -> ( ( 1 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
229 uzdisj 
 |-  ( ( 1 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
230 228 229 eqtr3di 
 |-  ( ph -> ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) )
231 disjiun 
 |-  ( ( 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 ) ) ) = (/) )
232 222 224 227 230 231 syl13anc 
 |-  ( ph -> ( U_ i e. ( 1 ... N ) ( (,) ` ( F ` i ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = (/) )
233 219 232 eqtrd 
 |-  ( ph -> ( L i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = (/) )
234 uneqdifeq 
 |-  ( ( 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 ) ) ) )
235 207 233 234 sylancr 
 |-  ( ph -> ( ( L u. U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) = A <-> ( A \ L ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
236 218 235 mpbid 
 |-  ( ph -> ( A \ L ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
237 236 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( A \ L ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
238 237 ineq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) i^i ( A \ L ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) ) )
239 incom 
 |-  ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i ( A \ L ) )
240 104 101 eqtri 
 |-  U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( G ` j ) ) i^i U_ i e. ( ZZ>= ` ( N + 1 ) ) ( (,) ` ( F ` i ) ) )
241 238 239 240 3eqtr4g 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( A \ L ) i^i ( (,) ` ( G ` j ) ) ) = U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
242 217 241 eqtr3id 
 |-  ( ( 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 ) ) ) )
243 242 fveq2d 
 |-  ( ( 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 ) ) ) ) )
244 212 243 oveq12d 
 |-  ( ( 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 ) ) ) ) ) )
245 204 244 eqtrd 
 |-  ( ( 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 ) ) ) ) ) )
246 202 142 resubcld 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) e. RR )
247 inss2 
 |-  ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) )
248 190 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
249 200 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
250 ovolsscl 
 |-  ( ( ( ( (,) ` ( 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 )
251 247 248 249 250 mp3an2i 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
252 150 251 fsumrecl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> sum_ i e. ( 1 ... N ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
253 15 r19.21bi 
 |-  ( ( 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 ) )
254 252 202 142 absdifltd 
 |-  ( ( 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 ) ) ) ) )
255 253 254 mpbid 
 |-  ( ( 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 ) ) ) )
256 255 simpld 
 |-  ( ( 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 ) ) ) ) )
257 246 252 256 ltled 
 |-  ( ( 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 ) ) ) ) )
258 149 fveq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i L ) ) = ( vol* ` U_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
259 mblvol 
 |-  ( ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. dom vol -> ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
260 174 259 syl 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
261 260 251 eqeltrd 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ i e. ( 1 ... N ) ) -> ( vol ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
262 174 261 jca 
 |-  ( ( ( 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 ) )
263 262 ralrimiva 
 |-  ( ( 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 ) )
264 inss1 
 |-  ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( F ` i ) )
265 264 rgenw 
 |-  A. i e. NN ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( F ` i ) )
266 222 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> Disj_ i e. NN ( (,) ` ( F ` i ) ) )
267 disjss2 
 |-  ( 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 ) ) ) ) )
268 265 266 267 mpsyl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> Disj_ i e. NN ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
269 disjss1 
 |-  ( ( 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 ) ) ) ) )
270 223 268 269 mpsyl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> Disj_ i e. ( 1 ... N ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
271 volfiniun 
 |-  ( ( ( 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 ) ) ) ) )
272 150 263 270 271 syl3anc 
 |-  ( ( 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 ) ) ) ) )
273 mblvol 
 |-  ( 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 ) ) ) ) )
274 177 273 syl 
 |-  ( ( 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 ) ) ) ) )
275 260 sumeq2dv 
 |-  ( ( 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 ) ) ) ) )
276 272 274 275 3eqtr3d 
 |-  ( ( 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 ) ) ) ) )
277 258 276 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i L ) ) = sum_ i e. ( 1 ... N ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
278 257 277 breqtrrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) - ( C / M ) ) <_ ( vol* ` ( ( (,) ` ( G ` j ) ) i^i L ) ) )
279 277 252 eqeltrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i L ) ) e. RR )
280 202 142 279 lesubaddd 
 |-  ( ( 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 ) ) ) )
281 278 280 mpbid 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) <_ ( ( vol* ` ( ( (,) ` ( G ` j ) ) i^i L ) ) + ( C / M ) ) )
282 245 281 eqbrtrrd 
 |-  ( ( 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 ) ) )
283 134 142 279 leadd2d 
 |-  ( ( 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 ) ) ) )
284 282 283 mpbird 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ ( C / M ) )
285 127 134 142 284 fsumle 
 |-  ( 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 ) )
286 141 recnd 
 |-  ( ph -> ( C / M ) e. CC )
287 fsumconst 
 |-  ( ( ( 1 ... M ) e. Fin /\ ( C / M ) e. CC ) -> sum_ j e. ( 1 ... M ) ( C / M ) = ( ( # ` ( 1 ... M ) ) x. ( C / M ) ) )
288 127 286 287 syl2anc 
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( C / M ) = ( ( # ` ( 1 ... M ) ) x. ( C / M ) ) )
289 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
290 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
291 11 289 290 3syl 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = M )
292 291 oveq1d 
 |-  ( ph -> ( ( # ` ( 1 ... M ) ) x. ( C / M ) ) = ( M x. ( C / M ) ) )
293 119 recnd 
 |-  ( ph -> C e. CC )
294 11 nncnd 
 |-  ( ph -> M e. CC )
295 11 nnne0d 
 |-  ( ph -> M =/= 0 )
296 293 294 295 divcan2d 
 |-  ( ph -> ( M x. ( C / M ) ) = C )
297 288 292 296 3eqtrd 
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( C / M ) = C )
298 285 297 breqtrd 
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( vol* ` U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ C )
299 117 135 119 140 298 letrd 
 |-  ( ph -> ( vol* ` U_ j e. ( 1 ... M ) U_ i e. ( ZZ>= ` ( N + 1 ) ) ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) <_ C )
300 117 119 39 299 leadd2dd 
 |-  ( 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 ) )
301 36 118 120 126 300 letrd 
 |-  ( ph -> ( vol* ` ( K i^i A ) ) <_ ( ( vol* ` ( K i^i L ) ) + C ) )