MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniioombllem6 Structured version   Unicode version
Theorem uniioombllem6 21725
Description: Lemma for uniioombl 21726. (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 ) )
Assertion
Ref Expression
uniioombllem6 |- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
Distinct variable groups:   x, F   x, G   x, A   x, C   ph, x   x, T
Allowed substitution hints:   S( x)   E( x)
Proof of Theorem uniioombllem6
Dummy variables a i j k n y z m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11106 . . . 4 |- NN = ( ZZ>= ` 1 )
2 1zzd 10884 . . . 4 |- ( ph -> 1 e. ZZ )
3 uniioombl.c . . . 4 |- ( ph -> C e. RR+ )
4 eqidd 2461 . . . 4 |- ( ( ph /\ m e. NN ) -> ( T ` m ) = ( T ` m ) )
5 uniioombl.t . . . . . 6 |- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
6 eqidd 2461 . . . . . 6 |- ( ( ph /\ a e. NN ) -> ( ( ( abs o. - ) o. G ) ` a ) = ( ( ( abs o. - ) o. G ) ` a ) )
7 uniioombl.g . . . . . . . . . 10 |- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
8 eqid 2460 . . . . . . . . . . 11 |- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
98ovolfsf 21611 . . . . . . . . . 10 |- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
107, 9syl 16 . . . . . . . . 9 |- ( ph -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
1110ffvelrnda 6012 . . . . . . . 8 |- ( ( ph /\ a e. NN ) -> ( ( ( abs o. - ) o. G ) ` a ) e. ( 0 [,) +oo ) )
12 elrege0 11616 . . . . . . . 8 |- ( ( ( ( abs o. - ) o. G ) ` a ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. G ) ` a ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` a ) ) )
1311, 12sylib 196 . . . . . . 7 |- ( ( ph /\ a e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` a ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` a ) ) )
1413simpld 459 . . . . . 6 |- ( ( ph /\ a e. NN ) -> ( ( ( abs o. - ) o. G ) ` a ) e. RR )
1513simprd 463 . . . . . 6 |- ( ( ph /\ a e. NN ) -> 0 <_ ( ( ( abs o. - ) o. G ) ` a ) )
16 uniioombl.1 . . . . . . . 8 |- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
17 uniioombl.2 . . . . . . . 8 |- ( ph -> Disj x e. NN ( (,) ` ( F ` x ) ) )
18 uniioombl.3 . . . . . . . 8 |- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
19 uniioombl.a . . . . . . . 8 |- A = U. ran ( (,) o. F )
20 uniioombl.e . . . . . . . 8 |- ( ph -> ( vol* ` E ) e. RR )
21 uniioombl.s . . . . . . . 8 |- ( ph -> E C_ U. ran ( (,) o. G ) )
22 uniioombl.v . . . . . . . 8 |- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
2316, 17, 18, 19, 20, 3, 7, 21, 5, 22uniioombllem1 21718 . . . . . . 7 |- ( ph -> sup ( ran T , RR* , < ) e. RR )
248, 5ovolsf 21612 . . . . . . . . . . . . 13 |- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) )
257, 24syl 16 . . . . . . . . . . . 12 |- ( ph -> T : NN --> ( 0 [,) +oo ) )
26 frn 5728 . . . . . . . . . . . 12 |- ( T : NN --> ( 0 [,) +oo ) -> ran T C_ ( 0 [,) +oo ) )
2725, 26syl 16 . . . . . . . . . . 11 |- ( ph -> ran T C_ ( 0 [,) +oo ) )
28 icossxr 11598 . . . . . . . . . . 11 |- ( 0 [,) +oo ) C_ RR*
2927, 28syl6ss 3509 . . . . . . . . . 10 |- ( ph -> ran T C_ RR* )
30 supxrub 11505 . . . . . . . . . 10 |- ( ( ran T C_ RR* /\ x e. ran T ) -> x <_ sup ( ran T , RR* , < ) )
3129, 30sylan 471 . . . . . . . . 9 |- ( ( ph /\ x e. ran T ) -> x <_ sup ( ran T , RR* , < ) )
3231ralrimiva 2871 . . . . . . . 8 |- ( ph -> A. x e. ran T x <_ sup ( ran T , RR* , < ) )
33 ffn 5722 . . . . . . . . . 10 |- ( T : NN --> ( 0 [,) +oo ) -> T Fn NN )
3425, 33syl 16 . . . . . . . . 9 |- ( ph -> T Fn NN )
35 breq1 4443 . . . . . . . . . 10 |- ( x = ( T ` m ) -> ( x <_ sup ( ran T , RR* , < ) <-> ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
3635ralrn 6015 . . . . . . . . 9 |- ( T Fn NN -> ( A. x e. ran T x <_ sup ( ran T , RR* , < ) <-> A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
3734, 36syl 16 . . . . . . . 8 |- ( ph -> ( A. x e. ran T x <_ sup ( ran T , RR* , < ) <-> A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
3832, 37mpbid 210 . . . . . . 7 |- ( ph -> A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) )
39 breq2 4444 . . . . . . . . 9 |- ( x = sup ( ran T , RR* , < ) -> ( ( T ` m ) <_ x <-> ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
4039ralbidv 2896 . . . . . . . 8 |- ( x = sup ( ran T , RR* , < ) -> ( A. m e. NN ( T ` m ) <_ x <-> A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
4140rspcev 3207 . . . . . . 7 |- ( ( sup ( ran T , RR* , < ) e. RR /\ A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) ) -> E. x e. RR A. m e. NN ( T ` m ) <_ x )
4223, 38, 41syl2anc 661 . . . . . 6 |- ( ph -> E. x e. RR A. m e. NN ( T ` m ) <_ x )
431, 5, 2, 6, 14, 15, 42isumsup2 13610 . . . . 5 |- ( ph -> T ~~> sup ( ran T , RR , < ) )
44 0re 9585 . . . . . . . 8 |- 0 e. RR
45 pnfxr 11310 . . . . . . . 8 |- +oo e. RR*
46 icossre 11594 . . . . . . . 8 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
4744, 45, 46mp2an 672 . . . . . . 7 |- ( 0 [,) +oo ) C_ RR
4827, 47syl6ss 3509 . . . . . 6 |- ( ph -> ran T C_ RR )
49 1nn 10536 . . . . . . . . 9 |- 1 e. NN
50 fdm 5726 . . . . . . . . . 10 |- ( T : NN --> ( 0 [,) +oo ) -> dom T = NN )
5125, 50syl 16 . . . . . . . . 9 |- ( ph -> dom T = NN )
5249, 51syl5eleqr 2555 . . . . . . . 8 |- ( ph -> 1 e. dom T )
53 ne0i 3784 . . . . . . . 8 |- ( 1 e. dom T -> dom T =/= (/) )
5452, 53syl 16 . . . . . . 7 |- ( ph -> dom T =/= (/) )
55 dm0rn0 5210 . . . . . . . 8 |- ( dom T = (/) <-> ran T = (/) )
5655necon3bii 2728 . . . . . . 7 |- ( dom T =/= (/) <-> ran T =/= (/) )
5754, 56sylib 196 . . . . . 6 |- ( ph -> ran T =/= (/) )
58 breq2 4444 . . . . . . . . 9 |- ( y = sup ( ran T , RR* , < ) -> ( x <_ y <-> x <_ sup ( ran T , RR* , < ) ) )
5958ralbidv 2896 . . . . . . . 8 |- ( y = sup ( ran T , RR* , < ) -> ( A. x e. ran T x <_ y <-> A. x e. ran T x <_ sup ( ran T , RR* , < ) ) )
6059rspcev 3207 . . . . . . 7 |- ( ( sup ( ran T , RR* , < ) e. RR /\ A. x e. ran T x <_ sup ( ran T , RR* , < ) ) -> E. y e. RR A. x e. ran T x <_ y )
6123, 32, 60syl2anc 661 . . . . . 6 |- ( ph -> E. y e. RR A. x e. ran T x <_ y )
62 supxrre 11508 . . . . . 6 |- ( ( ran T C_ RR /\ ran T =/= (/) /\ E. y e. RR A. x e. ran T x <_ y ) -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
6348, 57, 61, 62syl3anc 1223 . . . . 5 |- ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
6443, 63breqtrrd 4466 . . . 4 |- ( ph -> T ~~> sup ( ran T , RR* , < ) )
651, 2, 3, 4, 64climi2 13283 . . 3 |- ( ph -> E. j e. NN A. m e. ( ZZ>= ` j ) ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
661r19.2uz 13133 . . 3 |- ( E. j e. NN A. m e. ( ZZ>= ` j ) ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C -> E. m e. NN ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
6765, 66syl 16 . 2 |- ( ph -> E. m e. NN ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
68 1zzd 10884 . . . . . . . . 9 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> 1 e. ZZ )
693ad2antrr 725 . . . . . . . . . 10 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> C e. RR+ )
70 simplrl 759 . . . . . . . . . . 11 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> m e. NN )
7170nnrpd 11244 . . . . . . . . . 10 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> m e. RR+ )
7269, 71rpdivcld 11262 . . . . . . . . 9 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( C / m ) e. RR+ )
73 fvex 5867 . . . . . . . . . . . . . . . 16 |- ( (,) ` ( F ` z ) ) e. _V
7473inex1 4581 . . . . . . . . . . . . . . 15 |- ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V
7574rgenw 2818 . . . . . . . . . . . . . 14 |- A. z e. NN ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V
76 eqid 2460 . . . . . . . . . . . . . . 15 |- ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) )
7776fnmpt 5698 . . . . . . . . . . . . . 14 |- ( A. z e. NN ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V -> ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) Fn NN )
7875, 77mp1i 12 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) Fn NN )
79 elfznn 11703 . . . . . . . . . . . . 13 |- ( i e. ( 1 ... n ) -> i e. NN )
80 fvco2 5933 . . . . . . . . . . . . 13 |- ( ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) Fn NN /\ i e. NN ) -> ( ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ` i ) = ( vol* ` ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) ) )
8178, 79, 80syl2an 477 . . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ` i ) = ( vol* ` ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) ) )
8279adantl 466 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> i e. NN )
83 fveq2 5857 . . . . . . . . . . . . . . . . 17 |- ( z = i -> ( F ` z ) = ( F ` i ) )
8483fveq2d 5861 . . . . . . . . . . . . . . . 16 |- ( z = i -> ( (,) ` ( F ` z ) ) = ( (,) ` ( F ` i ) ) )
8584ineq1d 3692 . . . . . . . . . . . . . . 15 |- ( z = i -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
86 fvex 5867 . . . . . . . . . . . . . . . 16 |- ( (,) ` ( F ` i ) ) e. _V
8786inex1 4581 . . . . . . . . . . . . . . 15 |- ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V
8885, 76, 87fvmpt 5941 . . . . . . . . . . . . . 14 |- ( i e. NN -> ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) = ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
8982, 88syl 16 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) = ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
9089fveq2d 5861 . . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) ) = ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
9181, 90eqtrd 2501 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ` i ) = ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
92 simpr 461 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> n e. NN )
9392, 1syl6eleq 2558 . . . . . . . . . . 11 |- ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
94 inss2 3712 . . . . . . . . . . . . . 14 |- ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) )
9594a1i 11 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) ) )
96 inss2 3712 . . . . . . . . . . . . . . . . . . 19 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
977adantr 465 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
98 elfznn 11703 . . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( 1 ... m ) -> j e. NN )
99 ffvelrn 6010 . . . . . . . . . . . . . . . . . . . 20 |- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
10097, 98, 99syl2an 477 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
10196, 100sseldi 3495 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( G ` j ) e. ( RR X. RR ) )
102 1st2nd2 6811 . . . . . . . . . . . . . . . . . 18 |- ( ( G ` j ) e. ( RR X. RR ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
103101, 102syl 16 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
104103fveq2d 5861 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) )
105 df-ov 6278 . . . . . . . . . . . . . . . 16 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
106104, 105syl6eqr 2519 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) )
107 ioossre 11575 . . . . . . . . . . . . . . 15 |- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR
108106, 107syl6eqss 3547 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
109108ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
110106fveq2d 5861 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) )
111 ovolfcl 21606 . . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
11297, 98, 111syl2an 477 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) )
113 ovolioo 21706 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) )
114112, 113syl 16 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
115110, 114eqtrd 2501 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
116112simp2d 1004 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( 2nd ` ( G ` j ) ) e. RR )
117112simp1d 1003 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( 1st ` ( G ` j ) ) e. RR )
118116, 117resubcld 9976 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR )
119115, 118eqeltrd 2548 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
120119ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
121 ovolsscl 21625 . . . . . . . . . . . . 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 )
12295, 109, 120, 121syl3anc 1223 . . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
123122recnd 9611 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. CC )
12491, 93, 123fsumser 13501 . . . . . . . . . 10 |- ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ` n ) )
125124eqcomd 2468 . . . . . . . . 9 |- ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> ( seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ` n ) = sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
126 fveq2 5857 . . . . . . . . . . . . . . 15 |- ( z = k -> ( F ` z ) = ( F ` k ) )
127126fveq2d 5861 . . . . . . . . . . . . . 14 |- ( z = k -> ( (,) ` ( F ` z ) ) = ( (,) ` ( F ` k ) ) )
128127ineq1d 3692 . . . . . . . . . . . . 13 |- ( z = k -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` k ) ) i^i ( (,) ` ( G ` j ) ) ) )
129128cbvmptv 4531 . . . . . . . . . . . 12 |- ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( k e. NN |-> ( ( (,) ` ( F ` k ) ) i^i ( (,) ` ( G ` j ) ) ) )
130 eqeq1 2464 . . . . . . . . . . . . . 14 |- ( z = x -> ( z = (/) <-> x = (/) ) )
131 supeq1 7894 . . . . . . . . . . . . . . 15 |- ( z = x -> sup ( z , RR* , `' < ) = sup ( x , RR* , `' < ) )
132 supeq1 7894 . . . . . . . . . . . . . . 15 |- ( z = x -> sup ( z , RR* , < ) = sup ( x , RR* , < ) )
133131, 132opeq12d 4214 . . . . . . . . . . . . . 14 |- ( z = x -> <. sup ( z , RR* , `' < ) , sup ( z , RR* , < ) >. = <. sup ( x , RR* , `' < ) , sup ( x , RR* , < ) >. )
134130, 133ifbieq2d 3957 . . . . . . . . . . . . 13 |- ( z = x -> if ( z = (/) , <. 0 , 0 >. , <. sup ( z , RR* , `' < ) , sup ( z , RR* , < ) >. ) = if ( x = (/) , <. 0 , 0 >. , <. sup ( x , RR* , `' < ) , sup ( x , RR* , < ) >. ) )
135134cbvmptv 4531 . . . . . . . . . . . 12 |- ( z e. ran (,) |-> if ( z = (/) , <. 0 , 0 >. , <. sup ( z , RR* , `' < ) , sup ( z , RR* , < ) >. ) ) = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. sup ( x , RR* , `' < ) , sup ( x , RR* , < ) >. ) )
13616, 17, 18, 19, 20, 3, 7, 21, 5, 22, 129, 135uniioombllem2 21720 . . . . . . . . . . 11 |- ( ( ph /\ j e. NN ) -> seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ~~> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) )
13798, 136sylan2 474 . . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... m ) ) -> seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ~~> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) )
138137adantlr 714 . . . . . . . . 9 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ~~> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) )
1391, 68, 72, 125, 138climi2 13283 . . . . . . . 8 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> E. a e. NN A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
140 1z 10883 . . . . . . . . 9 |- 1 e. ZZ
1411rexuz3 13130 . . . . . . . . 9 |- ( 1 e. ZZ -> ( E. a e. NN A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) )
142140, 141ax-mp 5 . . . . . . . 8 |- ( E. a e. NN A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
143139, 142sylib 196 . . . . . . 7 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
144143ralrimiva 2871 . . . . . 6 |- ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> A. j e. ( 1 ... m ) E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
145 fzfi 12038 . . . . . . 7 |- ( 1 ... m ) e. Fin
146 rexfiuz 13129 . . . . . . 7 |- ( ( 1 ... m ) e. Fin -> ( E. a e. ZZ A. n e. ( ZZ>= ` a ) 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 ) <-> A. j e. ( 1 ... m ) E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) )
147145, 146ax-mp 5 . . . . . 6 |- ( E. a e. ZZ A. n e. ( ZZ>= ` a ) 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 ) <-> A. j e. ( 1 ... m ) E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
148144, 147sylibr 212 . . . . 5 |- ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> E. a e. ZZ A. n e. ( ZZ>= ` a ) 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 ) )
1491rexuz3 13130 . . . . . 6 |- ( 1 e. ZZ -> ( E. a e. NN A. n e. ( ZZ>= ` a ) 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 ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) 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 ) ) )
150140, 149ax-mp 5 . . . . 5 |- ( E. a e. NN A. n e. ( ZZ>= ` a ) 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 ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) 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 ) )
151148, 150sylibr 212 . . . 4 |- ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> E. a e. NN A. n e. ( ZZ>= ` a ) 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 ) )
1521r19.2uz 13133 . . . 4 |- ( E. a e. NN A. n e. ( ZZ>= ` a ) 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 ) -> E. n e. NN 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 ) )
153151, 152syl 16 . . 3 |- ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> E. n e. NN 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 ) )
15416adantr 465 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
15517adantr 465 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> Disj x e. NN ( (,) ` ( F ` x ) ) )
15620adantr 465 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> ( vol* ` E ) e. RR )
1573adantr 465 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> C e. RR+ )
1587adantr 465 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
15921adantr 465 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> E C_ U. ran ( (,) o. G ) )
16022adantr 465 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
161 simprll 761 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> m e. NN )
162 simprlr 762 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
163 eqid 2460 . . . . 5 |- U. ( ( (,) o. G ) " ( 1 ... m ) ) = U. ( ( (,) o. G ) " ( 1 ... m ) )
164 simprrl 763 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> n e. NN )
165 simprrr 764 . . . . . 6 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> 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 ) )
166 fveq2 5857 . . . . . . . . . . . . . . 15 |- ( i = z -> ( F ` i ) = ( F ` z ) )
167166fveq2d 5861 . . . . . . . . . . . . . 14 |- ( i = z -> ( (,) ` ( F ` i ) ) = ( (,) ` ( F ` z ) ) )
168167ineq1d 3692 . . . . . . . . . . . . 13 |- ( i = z -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) )
169168fveq2d 5861 . . . . . . . . . . . 12 |- ( i = z -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
170169cbvsumv 13467 . . . . . . . . . . 11 |- sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) )
171 fveq2 5857 . . . . . . . . . . . . . . 15 |- ( j = k -> ( G ` j ) = ( G ` k ) )
172171fveq2d 5861 . . . . . . . . . . . . . 14 |- ( j = k -> ( (,) ` ( G ` j ) ) = ( (,) ` ( G ` k ) ) )
173172ineq2d 3693 . . . . . . . . . . . . 13 |- ( j = k -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) )
174173fveq2d 5861 . . . . . . . . . . . 12 |- ( j = k -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) )
175174sumeq2sdv 13475 . . . . . . . . . . 11 |- ( j = k -> sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) )
176170, 175syl5eq 2513 . . . . . . . . . 10 |- ( j = k -> sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) )
177172ineq1d 3692 . . . . . . . . . . 11 |- ( j = k -> ( ( (,) ` ( G ` j ) ) i^i A ) = ( ( (,) ` ( G ` k ) ) i^i A ) )
178177fveq2d 5861 . . . . . . . . . 10 |- ( j = k -> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) = ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) )
179176, 178oveq12d 6293 . . . . . . . . 9 |- ( j = k -> ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) = ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) )
180179fveq2d 5861 . . . . . . . 8 |- ( j = k -> ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) = ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) )
181180breq1d 4450 . . . . . . 7 |- ( j = k -> ( ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) < ( C / m ) ) )
182181cbvralv 3081 . . . . . 6 |- ( 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 ) <-> A. k e. ( 1 ... m ) ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) < ( C / m ) )
183165, 182sylib 196 . . . . 5 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> A. k e. ( 1 ... m ) ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) < ( C / m ) )
184 eqid 2460 . . . . 5 |- U. ( ( (,) o. F ) " ( 1 ... n ) ) = U. ( ( (,) o. F ) " ( 1 ... n ) )
185154, 155, 18, 19, 156, 157, 158, 159, 5, 160, 161, 162, 163, 164, 183, 184uniioombllem5 21724 . . . 4 |- ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ 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 ) ) ) ) -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
186185anassrs 648 . . 3 |- ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ ( n e. NN /\ 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 ) ) ) -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
187153, 186rexlimddv 2952 . 2 |- ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
18867, 187rexlimddv 2952 1 |- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 968   = wceq 1374   e. wcel 1762   =/= wne 2655   A.wral 2807   E.wrex 2808   _Vcvv 3106   \ cdif 3466   i^i cin 3468   C_ wss 3469   (/)c0 3778   ifcif 3932   <.cop 4026   U.cuni 4238  Disj wdisj 4410   class class class wbr 4440   |-> cmpt 4498   X. cxp 4990   `'ccnv 4991   dom cdm 4992   ran crn 4993   "cima 4995   o. ccom 4996   Fn wfn 5574   -->wf 5575   ` cfv 5579  (class class class)co 6275   1stc1st 6772   2ndc2nd 6773   Fincfn 7506   supcsup 7889   RRcr 9480   0cc0 9481   1c1 9482   + caddc 9484   x. cmul 9486   +oocpnf 9614   RR*cxr 9616   < clt 9617   <_ cle 9618   - cmin 9794   / cdiv 10195   NNcn 10525   4c4 10576   ZZcz 10853   ZZ>=cuz 11071   RR+crp 11209   (,)cioo 11518   [,)cico 11520   ...cfz 11661   seqcseq 12063   abscabs 13017   ~~> cli 13256   sum_csu 13457   vol*covol 21602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-inf2 8047  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-int 4276  df-iun 4320  df-disj 4411  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-se 4832  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-isom 5588  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-of 6515  df-om 6672  df-1st 6774  df-2nd 6775  df-recs 7032  df-rdg 7066  df-1o 7120  df-2o 7121  df-oadd 7124  df-er 7301  df-map 7412  df-pm 7413  df-en 7507  df-dom 7508  df-sdom 7509  df-fin 7510  df-fi 7860  df-sup 7890  df-oi 7924  df-card 8309  df-acn 8312  df-cda 8537  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-div 10196  df-nn 10526  df-2 10583  df-3 10584  df-4 10585  df-n0 10785  df-z 10854  df-uz 11072  df-q 11172  df-rp 11210  df-xneg 11307  df-xadd 11308  df-xmul 11309  df-ioo 11522  df-ico 11524  df-icc 11525  df-fz 11662  df-fzo 11782  df-fl 11886  df-seq 12064  df-exp 12123  df-hash 12361  df-cj 12882  df-re 12883  df-im 12884  df-sqr 13018  df-abs 13019  df-clim 13260  df-rlim 13261  df-sum 13458  df-rest 14667  df-topgen 14688  df-psmet 18175  df-xmet 18176  df-met 18177  df-bl 18178  df-mopn 18179  df-top 19159  df-bases 19161  df-topon 19162  df-cmp 19646  df-ovol 21604  df-vol 21605
This theorem is referenced by:  uniioombl  21726
  Copyright terms: Public domain W3C validator