Step |
Hyp |
Ref |
Expression |
1 |
|
iuneq1 |
|- ( A = (/) -> U_ n e. A B = U_ n e. (/) B ) |
2 |
|
0iun |
|- U_ n e. (/) B = (/) |
3 |
1 2
|
eqtrdi |
|- ( A = (/) -> U_ n e. A B = (/) ) |
4 |
3
|
fveq2d |
|- ( A = (/) -> ( vol* ` U_ n e. A B ) = ( vol* ` (/) ) ) |
5 |
|
ovol0 |
|- ( vol* ` (/) ) = 0 |
6 |
4 5
|
eqtrdi |
|- ( A = (/) -> ( vol* ` U_ n e. A B ) = 0 ) |
7 |
6
|
a1i |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( A = (/) -> ( vol* ` U_ n e. A B ) = 0 ) ) |
8 |
|
reldom |
|- Rel ~<_ |
9 |
8
|
brrelex1i |
|- ( A ~<_ NN -> A e. _V ) |
10 |
9
|
adantr |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> A e. _V ) |
11 |
|
0sdomg |
|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) ) |
12 |
10 11
|
syl |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( (/) ~< A <-> A =/= (/) ) ) |
13 |
|
fodomr |
|- ( ( (/) ~< A /\ A ~<_ NN ) -> E. f f : NN -onto-> A ) |
14 |
13
|
expcom |
|- ( A ~<_ NN -> ( (/) ~< A -> E. f f : NN -onto-> A ) ) |
15 |
14
|
adantr |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( (/) ~< A -> E. f f : NN -onto-> A ) ) |
16 |
|
eliun |
|- ( x e. U_ n e. A B <-> E. n e. A x e. B ) |
17 |
|
nfv |
|- F/ n f : NN -onto-> A |
18 |
|
nfcv |
|- F/_ n NN |
19 |
|
nfcsb1v |
|- F/_ n [_ ( f ` k ) / n ]_ B |
20 |
18 19
|
nfiun |
|- F/_ n U_ k e. NN [_ ( f ` k ) / n ]_ B |
21 |
20
|
nfcri |
|- F/ n x e. U_ k e. NN [_ ( f ` k ) / n ]_ B |
22 |
|
foelrn |
|- ( ( f : NN -onto-> A /\ n e. A ) -> E. k e. NN n = ( f ` k ) ) |
23 |
22
|
ex |
|- ( f : NN -onto-> A -> ( n e. A -> E. k e. NN n = ( f ` k ) ) ) |
24 |
|
csbeq1a |
|- ( n = ( f ` k ) -> B = [_ ( f ` k ) / n ]_ B ) |
25 |
24
|
adantl |
|- ( ( f : NN -onto-> A /\ n = ( f ` k ) ) -> B = [_ ( f ` k ) / n ]_ B ) |
26 |
25
|
eleq2d |
|- ( ( f : NN -onto-> A /\ n = ( f ` k ) ) -> ( x e. B <-> x e. [_ ( f ` k ) / n ]_ B ) ) |
27 |
26
|
biimpd |
|- ( ( f : NN -onto-> A /\ n = ( f ` k ) ) -> ( x e. B -> x e. [_ ( f ` k ) / n ]_ B ) ) |
28 |
27
|
impancom |
|- ( ( f : NN -onto-> A /\ x e. B ) -> ( n = ( f ` k ) -> x e. [_ ( f ` k ) / n ]_ B ) ) |
29 |
28
|
reximdv |
|- ( ( f : NN -onto-> A /\ x e. B ) -> ( E. k e. NN n = ( f ` k ) -> E. k e. NN x e. [_ ( f ` k ) / n ]_ B ) ) |
30 |
|
eliun |
|- ( x e. U_ k e. NN [_ ( f ` k ) / n ]_ B <-> E. k e. NN x e. [_ ( f ` k ) / n ]_ B ) |
31 |
29 30
|
syl6ibr |
|- ( ( f : NN -onto-> A /\ x e. B ) -> ( E. k e. NN n = ( f ` k ) -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) |
32 |
31
|
ex |
|- ( f : NN -onto-> A -> ( x e. B -> ( E. k e. NN n = ( f ` k ) -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) ) |
33 |
32
|
com23 |
|- ( f : NN -onto-> A -> ( E. k e. NN n = ( f ` k ) -> ( x e. B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) ) |
34 |
23 33
|
syld |
|- ( f : NN -onto-> A -> ( n e. A -> ( x e. B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) ) |
35 |
17 21 34
|
rexlimd |
|- ( f : NN -onto-> A -> ( E. n e. A x e. B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) |
36 |
16 35
|
syl5bi |
|- ( f : NN -onto-> A -> ( x e. U_ n e. A B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) |
37 |
36
|
ssrdv |
|- ( f : NN -onto-> A -> U_ n e. A B C_ U_ k e. NN [_ ( f ` k ) / n ]_ B ) |
38 |
37
|
adantl |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> U_ n e. A B C_ U_ k e. NN [_ ( f ` k ) / n ]_ B ) |
39 |
|
fof |
|- ( f : NN -onto-> A -> f : NN --> A ) |
40 |
39
|
adantl |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> f : NN --> A ) |
41 |
40
|
ffvelrnda |
|- ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( f ` k ) e. A ) |
42 |
|
simpllr |
|- ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) |
43 |
|
nfcv |
|- F/_ n RR |
44 |
19 43
|
nfss |
|- F/ n [_ ( f ` k ) / n ]_ B C_ RR |
45 |
|
nfcv |
|- F/_ n vol* |
46 |
45 19
|
nffv |
|- F/_ n ( vol* ` [_ ( f ` k ) / n ]_ B ) |
47 |
46
|
nfeq1 |
|- F/ n ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 |
48 |
44 47
|
nfan |
|- F/ n ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) |
49 |
24
|
sseq1d |
|- ( n = ( f ` k ) -> ( B C_ RR <-> [_ ( f ` k ) / n ]_ B C_ RR ) ) |
50 |
24
|
fveqeq2d |
|- ( n = ( f ` k ) -> ( ( vol* ` B ) = 0 <-> ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) ) |
51 |
49 50
|
anbi12d |
|- ( n = ( f ` k ) -> ( ( B C_ RR /\ ( vol* ` B ) = 0 ) <-> ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) ) ) |
52 |
48 51
|
rspc |
|- ( ( f ` k ) e. A -> ( A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) -> ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) ) ) |
53 |
41 42 52
|
sylc |
|- ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) ) |
54 |
53
|
simpld |
|- ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> [_ ( f ` k ) / n ]_ B C_ RR ) |
55 |
54
|
ralrimiva |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> A. k e. NN [_ ( f ` k ) / n ]_ B C_ RR ) |
56 |
|
iunss |
|- ( U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR <-> A. k e. NN [_ ( f ` k ) / n ]_ B C_ RR ) |
57 |
55 56
|
sylibr |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR ) |
58 |
|
eqid |
|- seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) ) = seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) ) |
59 |
|
eqid |
|- ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) = ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) |
60 |
53
|
simprd |
|- ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) |
61 |
|
0re |
|- 0 e. RR |
62 |
60 61
|
eqeltrdi |
|- ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( vol* ` [_ ( f ` k ) / n ]_ B ) e. RR ) |
63 |
60
|
mpteq2dva |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) = ( k e. NN |-> 0 ) ) |
64 |
|
fconstmpt |
|- ( NN X. { 0 } ) = ( k e. NN |-> 0 ) |
65 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
66 |
65
|
xpeq1i |
|- ( NN X. { 0 } ) = ( ( ZZ>= ` 1 ) X. { 0 } ) |
67 |
64 66
|
eqtr3i |
|- ( k e. NN |-> 0 ) = ( ( ZZ>= ` 1 ) X. { 0 } ) |
68 |
63 67
|
eqtrdi |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) = ( ( ZZ>= ` 1 ) X. { 0 } ) ) |
69 |
68
|
seqeq3d |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) ) = seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ) |
70 |
|
1z |
|- 1 e. ZZ |
71 |
|
serclim0 |
|- ( 1 e. ZZ -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 ) |
72 |
|
seqex |
|- seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) e. _V |
73 |
|
c0ex |
|- 0 e. _V |
74 |
72 73
|
breldm |
|- ( seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) e. dom ~~> ) |
75 |
70 71 74
|
mp2b |
|- seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) e. dom ~~> |
76 |
69 75
|
eqeltrdi |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) ) e. dom ~~> ) |
77 |
58 59 54 62 76
|
ovoliun2 |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ sum_ k e. NN ( vol* ` [_ ( f ` k ) / n ]_ B ) ) |
78 |
60
|
sumeq2dv |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> sum_ k e. NN ( vol* ` [_ ( f ` k ) / n ]_ B ) = sum_ k e. NN 0 ) |
79 |
65
|
eqimssi |
|- NN C_ ( ZZ>= ` 1 ) |
80 |
79
|
orci |
|- ( NN C_ ( ZZ>= ` 1 ) \/ NN e. Fin ) |
81 |
|
sumz |
|- ( ( NN C_ ( ZZ>= ` 1 ) \/ NN e. Fin ) -> sum_ k e. NN 0 = 0 ) |
82 |
80 81
|
ax-mp |
|- sum_ k e. NN 0 = 0 |
83 |
78 82
|
eqtrdi |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> sum_ k e. NN ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) |
84 |
77 83
|
breqtrd |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ 0 ) |
85 |
|
ovolge0 |
|- ( U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR -> 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) |
86 |
57 85
|
syl |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) |
87 |
|
ovolcl |
|- ( U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) e. RR* ) |
88 |
57 87
|
syl |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) e. RR* ) |
89 |
|
0xr |
|- 0 e. RR* |
90 |
|
xrletri3 |
|- ( ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) e. RR* /\ 0 e. RR* ) -> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 <-> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ 0 /\ 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) ) ) |
91 |
88 89 90
|
sylancl |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 <-> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ 0 /\ 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) ) ) |
92 |
84 86 91
|
mpbir2and |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 ) |
93 |
|
ovolssnul |
|- ( ( U_ n e. A B C_ U_ k e. NN [_ ( f ` k ) / n ]_ B /\ U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 ) -> ( vol* ` U_ n e. A B ) = 0 ) |
94 |
38 57 92 93
|
syl3anc |
|- ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ n e. A B ) = 0 ) |
95 |
94
|
ex |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( f : NN -onto-> A -> ( vol* ` U_ n e. A B ) = 0 ) ) |
96 |
95
|
exlimdv |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( E. f f : NN -onto-> A -> ( vol* ` U_ n e. A B ) = 0 ) ) |
97 |
15 96
|
syld |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( (/) ~< A -> ( vol* ` U_ n e. A B ) = 0 ) ) |
98 |
12 97
|
sylbird |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( A =/= (/) -> ( vol* ` U_ n e. A B ) = 0 ) ) |
99 |
7 98
|
pm2.61dne |
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( vol* ` U_ n e. A B ) = 0 ) |