Step |
Hyp |
Ref |
Expression |
1 |
|
ovoliun.t |
|- T = seq 1 ( + , G ) |
2 |
|
ovoliun.g |
|- G = ( n e. NN |-> ( vol* ` A ) ) |
3 |
|
ovoliun.a |
|- ( ( ph /\ n e. NN ) -> A C_ RR ) |
4 |
|
ovoliun.v |
|- ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR ) |
5 |
|
ovoliun2.t |
|- ( ph -> T e. dom ~~> ) |
6 |
1 2 3 4
|
ovoliun |
|- ( ph -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) |
7 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
8 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
9 |
|
fvex |
|- ( vol* ` [_ m / n ]_ A ) e. _V |
10 |
|
nfcv |
|- F/_ m ( vol* ` A ) |
11 |
|
nfcv |
|- F/_ n vol* |
12 |
|
nfcsb1v |
|- F/_ n [_ m / n ]_ A |
13 |
11 12
|
nffv |
|- F/_ n ( vol* ` [_ m / n ]_ A ) |
14 |
|
csbeq1a |
|- ( n = m -> A = [_ m / n ]_ A ) |
15 |
14
|
fveq2d |
|- ( n = m -> ( vol* ` A ) = ( vol* ` [_ m / n ]_ A ) ) |
16 |
10 13 15
|
cbvmpt |
|- ( n e. NN |-> ( vol* ` A ) ) = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) ) |
17 |
2 16
|
eqtri |
|- G = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) ) |
18 |
17
|
fvmpt2 |
|- ( ( m e. NN /\ ( vol* ` [_ m / n ]_ A ) e. _V ) -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) ) |
19 |
9 18
|
mpan2 |
|- ( m e. NN -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) ) |
20 |
19
|
adantl |
|- ( ( ph /\ m e. NN ) -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) ) |
21 |
4
|
ralrimiva |
|- ( ph -> A. n e. NN ( vol* ` A ) e. RR ) |
22 |
10
|
nfel1 |
|- F/ m ( vol* ` A ) e. RR |
23 |
13
|
nfel1 |
|- F/ n ( vol* ` [_ m / n ]_ A ) e. RR |
24 |
15
|
eleq1d |
|- ( n = m -> ( ( vol* ` A ) e. RR <-> ( vol* ` [_ m / n ]_ A ) e. RR ) ) |
25 |
22 23 24
|
cbvralw |
|- ( A. n e. NN ( vol* ` A ) e. RR <-> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR ) |
26 |
21 25
|
sylib |
|- ( ph -> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR ) |
27 |
26
|
r19.21bi |
|- ( ( ph /\ m e. NN ) -> ( vol* ` [_ m / n ]_ A ) e. RR ) |
28 |
20 27
|
eqeltrd |
|- ( ( ph /\ m e. NN ) -> ( G ` m ) e. RR ) |
29 |
7 8 28
|
serfre |
|- ( ph -> seq 1 ( + , G ) : NN --> RR ) |
30 |
1
|
feq1i |
|- ( T : NN --> RR <-> seq 1 ( + , G ) : NN --> RR ) |
31 |
29 30
|
sylibr |
|- ( ph -> T : NN --> RR ) |
32 |
31
|
frnd |
|- ( ph -> ran T C_ RR ) |
33 |
|
1nn |
|- 1 e. NN |
34 |
31
|
fdmd |
|- ( ph -> dom T = NN ) |
35 |
33 34
|
eleqtrrid |
|- ( ph -> 1 e. dom T ) |
36 |
35
|
ne0d |
|- ( ph -> dom T =/= (/) ) |
37 |
|
dm0rn0 |
|- ( dom T = (/) <-> ran T = (/) ) |
38 |
37
|
necon3bii |
|- ( dom T =/= (/) <-> ran T =/= (/) ) |
39 |
36 38
|
sylib |
|- ( ph -> ran T =/= (/) ) |
40 |
1 5
|
eqeltrrid |
|- ( ph -> seq 1 ( + , G ) e. dom ~~> ) |
41 |
7 8 20 27 40
|
isumrecl |
|- ( ph -> sum_ m e. NN ( vol* ` [_ m / n ]_ A ) e. RR ) |
42 |
|
elfznn |
|- ( m e. ( 1 ... k ) -> m e. NN ) |
43 |
42
|
adantl |
|- ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> m e. NN ) |
44 |
43 19
|
syl |
|- ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( G ` m ) = ( vol* ` [_ m / n ]_ A ) ) |
45 |
|
simpr |
|- ( ( ph /\ k e. NN ) -> k e. NN ) |
46 |
45 7
|
eleqtrdi |
|- ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) ) |
47 |
|
simpl |
|- ( ( ph /\ k e. NN ) -> ph ) |
48 |
47 42 27
|
syl2an |
|- ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( vol* ` [_ m / n ]_ A ) e. RR ) |
49 |
48
|
recnd |
|- ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( vol* ` [_ m / n ]_ A ) e. CC ) |
50 |
44 46 49
|
fsumser |
|- ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) = ( seq 1 ( + , G ) ` k ) ) |
51 |
1
|
fveq1i |
|- ( T ` k ) = ( seq 1 ( + , G ) ` k ) |
52 |
50 51
|
eqtr4di |
|- ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) = ( T ` k ) ) |
53 |
|
fzfid |
|- ( ph -> ( 1 ... k ) e. Fin ) |
54 |
|
fz1ssnn |
|- ( 1 ... k ) C_ NN |
55 |
54
|
a1i |
|- ( ph -> ( 1 ... k ) C_ NN ) |
56 |
3
|
ralrimiva |
|- ( ph -> A. n e. NN A C_ RR ) |
57 |
|
nfv |
|- F/ m A C_ RR |
58 |
|
nfcv |
|- F/_ n RR |
59 |
12 58
|
nfss |
|- F/ n [_ m / n ]_ A C_ RR |
60 |
14
|
sseq1d |
|- ( n = m -> ( A C_ RR <-> [_ m / n ]_ A C_ RR ) ) |
61 |
57 59 60
|
cbvralw |
|- ( A. n e. NN A C_ RR <-> A. m e. NN [_ m / n ]_ A C_ RR ) |
62 |
56 61
|
sylib |
|- ( ph -> A. m e. NN [_ m / n ]_ A C_ RR ) |
63 |
62
|
r19.21bi |
|- ( ( ph /\ m e. NN ) -> [_ m / n ]_ A C_ RR ) |
64 |
|
ovolge0 |
|- ( [_ m / n ]_ A C_ RR -> 0 <_ ( vol* ` [_ m / n ]_ A ) ) |
65 |
63 64
|
syl |
|- ( ( ph /\ m e. NN ) -> 0 <_ ( vol* ` [_ m / n ]_ A ) ) |
66 |
7 8 53 55 20 27 65 40
|
isumless |
|- ( ph -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) ) |
67 |
66
|
adantr |
|- ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( vol* ` [_ m / n ]_ A ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) ) |
68 |
52 67
|
eqbrtrrd |
|- ( ( ph /\ k e. NN ) -> ( T ` k ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) ) |
69 |
68
|
ralrimiva |
|- ( ph -> A. k e. NN ( T ` k ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) ) |
70 |
|
brralrspcev |
|- ( ( sum_ m e. NN ( vol* ` [_ m / n ]_ A ) e. RR /\ A. k e. NN ( T ` k ) <_ sum_ m e. NN ( vol* ` [_ m / n ]_ A ) ) -> E. x e. RR A. k e. NN ( T ` k ) <_ x ) |
71 |
41 69 70
|
syl2anc |
|- ( ph -> E. x e. RR A. k e. NN ( T ` k ) <_ x ) |
72 |
31
|
ffnd |
|- ( ph -> T Fn NN ) |
73 |
|
breq1 |
|- ( z = ( T ` k ) -> ( z <_ x <-> ( T ` k ) <_ x ) ) |
74 |
73
|
ralrn |
|- ( T Fn NN -> ( A. z e. ran T z <_ x <-> A. k e. NN ( T ` k ) <_ x ) ) |
75 |
72 74
|
syl |
|- ( ph -> ( A. z e. ran T z <_ x <-> A. k e. NN ( T ` k ) <_ x ) ) |
76 |
75
|
rexbidv |
|- ( ph -> ( E. x e. RR A. z e. ran T z <_ x <-> E. x e. RR A. k e. NN ( T ` k ) <_ x ) ) |
77 |
71 76
|
mpbird |
|- ( ph -> E. x e. RR A. z e. ran T z <_ x ) |
78 |
|
supxrre |
|- ( ( ran T C_ RR /\ ran T =/= (/) /\ E. x e. RR A. z e. ran T z <_ x ) -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) ) |
79 |
32 39 77 78
|
syl3anc |
|- ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) ) |
80 |
7 1 8 20 27 65 71
|
isumsup |
|- ( ph -> sum_ m e. NN ( vol* ` [_ m / n ]_ A ) = sup ( ran T , RR , < ) ) |
81 |
79 80
|
eqtr4d |
|- ( ph -> sup ( ran T , RR* , < ) = sum_ m e. NN ( vol* ` [_ m / n ]_ A ) ) |
82 |
10 13 15
|
cbvsumi |
|- sum_ n e. NN ( vol* ` A ) = sum_ m e. NN ( vol* ` [_ m / n ]_ A ) |
83 |
81 82
|
eqtr4di |
|- ( ph -> sup ( ran T , RR* , < ) = sum_ n e. NN ( vol* ` A ) ) |
84 |
6 83
|
breqtrd |
|- ( ph -> ( vol* ` U_ n e. NN A ) <_ sum_ n e. NN ( vol* ` A ) ) |