Metamath Proof Explorer

Theorem uniioombllem5

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 25-Aug-2014)

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 uniioombllem5 
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. 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 
 |-  ( E i^i A ) C_ E
18 7 uniiccdif 
 |-  ( ph -> ( U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) /\ ( vol* ` ( U. ran ( [,] o. G ) \ U. ran ( (,) o. G ) ) ) = 0 ) )
19 18 simpld 
 |-  ( ph -> U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) )
20 ovolficcss 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. G ) C_ RR )
21 7 20 syl 
 |-  ( ph -> U. ran ( [,] o. G ) C_ RR )
22 19 21 sstrd 
 |-  ( ph -> U. ran ( (,) o. G ) C_ RR )
23 8 22 sstrd 
 |-  ( ph -> E C_ RR )
24 ovolsscl 
 |-  ( ( ( E i^i A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i A ) ) e. RR )
25 17 23 5 24 mp3an2i 
 |-  ( ph -> ( vol* ` ( E i^i A ) ) e. RR )
26 difssd 
 |-  ( ph -> ( E \ A ) C_ E )
27 ovolsscl 
 |-  ( ( ( E \ A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ A ) ) e. RR )
28 26 23 5 27 syl3anc 
 |-  ( ph -> ( vol* ` ( E \ A ) ) e. RR )
29 25 28 readdcld 
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) e. RR )
30 inss1 
 |-  ( K i^i A ) C_ K
31 imassrn 
 |-  ( ( (,) o. G ) " ( 1 ... M ) ) C_ ran ( (,) o. G )
32 31 unissi 
 |-  U. ( ( (,) o. G ) " ( 1 ... M ) ) C_ U. ran ( (,) o. G )
33 13 32 eqsstri 
 |-  K C_ U. ran ( (,) o. G )
34 33 22 sstrid 
 |-  ( ph -> K C_ RR )
35 1 2 3 4 5 6 7 8 9 10 uniioombllem1 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR )
36 ssid 
 |-  U. ran ( (,) o. G ) C_ U. ran ( (,) o. G )
37 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* , < ) )
38 7 36 37 sylancl 
 |-  ( ph -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) )
39 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 )
40 22 35 38 39 syl3anc 
 |-  ( ph -> ( vol* ` U. ran ( (,) o. G ) ) e. RR )
41 ovolsscl 
 |-  ( ( K C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol* ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol* ` K ) e. RR )
42 33 22 40 41 mp3an2i 
 |-  ( ph -> ( vol* ` K ) e. RR )
43 ovolsscl 
 |-  ( ( ( K i^i A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i A ) ) e. RR )
44 30 34 42 43 mp3an2i 
 |-  ( ph -> ( vol* ` ( K i^i A ) ) e. RR )
45 difssd 
 |-  ( ph -> ( K \ A ) C_ K )
46 ovolsscl 
 |-  ( ( ( K \ A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K \ A ) ) e. RR )
47 45 34 42 46 syl3anc 
 |-  ( ph -> ( vol* ` ( K \ A ) ) e. RR )
48 44 47 readdcld 
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) e. RR )
49 6 rpred 
 |-  ( ph -> C e. RR )
50 49 49 readdcld 
 |-  ( ph -> ( C + C ) e. RR )
51 48 50 readdcld 
 |-  ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) e. RR )
52 4re 
 |-  4 e. RR
53 remulcl 
 |-  ( ( 4 e. RR /\ C e. RR ) -> ( 4 x. C ) e. RR )
54 52 49 53 sylancr 
 |-  ( ph -> ( 4 x. C ) e. RR )
55 5 54 readdcld 
 |-  ( ph -> ( ( vol* ` E ) + ( 4 x. C ) ) e. RR )
56 1 2 3 4 5 6 7 8 9 10 11 12 13 uniioombllem3 
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) < ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) )
57 29 51 56 ltled 
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) )
58 5 50 readdcld 
 |-  ( ph -> ( ( vol* ` E ) + ( C + C ) ) e. RR )
59 42 49 readdcld 
 |-  ( ph -> ( ( vol* ` K ) + C ) e. RR )
60 inss1 
 |-  ( K i^i L ) C_ K
61 ovolsscl 
 |-  ( ( ( K i^i L ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i L ) ) e. RR )
62 60 34 42 61 mp3an2i 
 |-  ( ph -> ( vol* ` ( K i^i L ) ) e. RR )
63 62 49 readdcld 
 |-  ( ph -> ( ( vol* ` ( K i^i L ) ) + C ) e. RR )
64 difssd 
 |-  ( ph -> ( K \ L ) C_ K )
65 ovolsscl 
 |-  ( ( ( K \ L ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K \ L ) ) e. RR )
66 64 34 42 65 syl3anc 
 |-  ( ph -> ( vol* ` ( K \ L ) ) e. RR )
67 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 uniioombllem4 
 |-  ( ph -> ( vol* ` ( K i^i A ) ) <_ ( ( vol* ` ( K i^i L ) ) + C ) )
68 imassrn 
 |-  ( ( (,) o. F ) " ( 1 ... N ) ) C_ ran ( (,) o. F )
69 68 unissi 
 |-  U. ( ( (,) o. F ) " ( 1 ... N ) ) C_ U. ran ( (,) o. F )
70 69 16 4 3sstr4i 
 |-  L C_ A
71 sscon 
 |-  ( L C_ A -> ( K \ A ) C_ ( K \ L ) )
72 70 71 mp1i 
 |-  ( ph -> ( K \ A ) C_ ( K \ L ) )
73 64 34 sstrd 
 |-  ( ph -> ( K \ L ) C_ RR )
74 ovolss 
 |-  ( ( ( K \ A ) C_ ( K \ L ) /\ ( K \ L ) C_ RR ) -> ( vol* ` ( K \ A ) ) <_ ( vol* ` ( K \ L ) ) )
75 72 73 74 syl2anc 
 |-  ( ph -> ( vol* ` ( K \ A ) ) <_ ( vol* ` ( K \ L ) ) )
76 44 47 63 66 67 75 le2addd 
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) )
77 62 recnd 
 |-  ( ph -> ( vol* ` ( K i^i L ) ) e. CC )
78 49 recnd 
 |-  ( ph -> C e. CC )
79 66 recnd 
 |-  ( ph -> ( vol* ` ( K \ L ) ) e. CC )
80 77 78 79 add32d 
 |-  ( ph -> ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) = ( ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) + C ) )
81 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
82 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
83 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
84 82 83 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
85 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
86 1 84 85 sylancl 
 |-  ( ph -> F : NN --> ( RR* X. RR* ) )
87 fco 
 |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR )
88 81 86 87 sylancr 
 |-  ( ph -> ( (,) o. F ) : NN --> ~P RR )
89 ffun 
 |-  ( ( (,) o. F ) : NN --> ~P RR -> Fun ( (,) o. F ) )
90 funiunfv 
 |-  ( Fun ( (,) o. F ) -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
91 88 89 90 3syl 
 |-  ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = U. ( ( (,) o. F ) " ( 1 ... N ) ) )
92 91 16 eqtr4di 
 |-  ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) = L )
93 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
94 elfznn 
 |-  ( n e. ( 1 ... N ) -> n e. NN )
95 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( (,) o. F ) ` n ) = ( (,) ` ( F ` n ) ) )
96 1 94 95 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) = ( (,) ` ( F ` n ) ) )
97 ffvelcdm 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) )
98 1 94 97 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) )
99 98 elin2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) e. ( RR X. RR ) )
100 1st2nd2 
 |-  ( ( F ` n ) e. ( RR X. RR ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
101 99 100 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
102 101 fveq2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( (,) ` ( F ` n ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
103 df-ov 
 |-  ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
104 102 103 eqtr4di 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( (,) ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) )
105 96 104 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) )
106 ioombl 
 |-  ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) e. dom vol
107 105 106 eqeltrdi 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( (,) o. F ) ` n ) e. dom vol )
108 107 ralrimiva 
 |-  ( ph -> A. n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol )
109 finiunmbl 
 |-  ( ( ( 1 ... N ) e. Fin /\ A. n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol ) -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol )
110 93 108 109 syl2anc 
 |-  ( ph -> U_ n e. ( 1 ... N ) ( ( (,) o. F ) ` n ) e. dom vol )
111 92 110 eqeltrrd 
 |-  ( ph -> L e. dom vol )
112 mblsplit 
 |-  ( ( L e. dom vol /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` K ) = ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) )
113 111 34 42 112 syl3anc 
 |-  ( ph -> ( vol* ` K ) = ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) )
114 113 oveq1d 
 |-  ( ph -> ( ( vol* ` K ) + C ) = ( ( ( vol* ` ( K i^i L ) ) + ( vol* ` ( K \ L ) ) ) + C ) )
115 80 114 eqtr4d 
 |-  ( ph -> ( ( ( vol* ` ( K i^i L ) ) + C ) + ( vol* ` ( K \ L ) ) ) = ( ( vol* ` K ) + C ) )
116 76 115 breqtrd 
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( vol* ` K ) + C ) )
117 5 49 readdcld 
 |-  ( ph -> ( ( vol* ` E ) + C ) e. RR )
118 9 ovollb 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ K C_ U. ran ( (,) o. G ) ) -> ( vol* ` K ) <_ sup ( ran T , RR* , < ) )
119 7 33 118 sylancl 
 |-  ( ph -> ( vol* ` K ) <_ sup ( ran T , RR* , < ) )
120 42 35 117 119 10 letrd 
 |-  ( ph -> ( vol* ` K ) <_ ( ( vol* ` E ) + C ) )
121 42 117 49 120 leadd1dd 
 |-  ( ph -> ( ( vol* ` K ) + C ) <_ ( ( ( vol* ` E ) + C ) + C ) )
122 5 recnd 
 |-  ( ph -> ( vol* ` E ) e. CC )
123 122 78 78 addassd 
 |-  ( ph -> ( ( ( vol* ` E ) + C ) + C ) = ( ( vol* ` E ) + ( C + C ) ) )
124 121 123 breqtrd 
 |-  ( ph -> ( ( vol* ` K ) + C ) <_ ( ( vol* ` E ) + ( C + C ) ) )
125 48 59 58 116 124 letrd 
 |-  ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) <_ ( ( vol* ` E ) + ( C + C ) ) )
126 48 58 50 125 leadd1dd 
 |-  ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) <_ ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) )
127 50 recnd 
 |-  ( ph -> ( C + C ) e. CC )
128 122 127 127 addassd 
 |-  ( ph -> ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) = ( ( vol* ` E ) + ( ( C + C ) + ( C + C ) ) ) )
129 2t2e4 
 |-  ( 2 x. 2 ) = 4
130 129 oveq1i 
 |-  ( ( 2 x. 2 ) x. C ) = ( 4 x. C )
131 2cnd 
 |-  ( ph -> 2 e. CC )
132 131 131 78 mulassd 
 |-  ( ph -> ( ( 2 x. 2 ) x. C ) = ( 2 x. ( 2 x. C ) ) )
133 78 2timesd 
 |-  ( ph -> ( 2 x. C ) = ( C + C ) )
134 133 oveq2d 
 |-  ( ph -> ( 2 x. ( 2 x. C ) ) = ( 2 x. ( C + C ) ) )
135 127 2timesd 
 |-  ( ph -> ( 2 x. ( C + C ) ) = ( ( C + C ) + ( C + C ) ) )
136 132 134 135 3eqtrd 
 |-  ( ph -> ( ( 2 x. 2 ) x. C ) = ( ( C + C ) + ( C + C ) ) )
137 130 136 eqtr3id 
 |-  ( ph -> ( 4 x. C ) = ( ( C + C ) + ( C + C ) ) )
138 137 oveq2d 
 |-  ( ph -> ( ( vol* ` E ) + ( 4 x. C ) ) = ( ( vol* ` E ) + ( ( C + C ) + ( C + C ) ) ) )
139 128 138 eqtr4d 
 |-  ( ph -> ( ( ( vol* ` E ) + ( C + C ) ) + ( C + C ) ) = ( ( vol* ` E ) + ( 4 x. C ) ) )
140 126 139 breqtrd 
 |-  ( ph -> ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
141 29 51 55 57 140 letrd 
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )