Step |
Hyp |
Ref |
Expression |
1 |
|
vonioolem1.x |
|- ( ph -> X e. Fin ) |
2 |
|
vonioolem1.a |
|- ( ph -> A : X --> RR ) |
3 |
|
vonioolem1.b |
|- ( ph -> B : X --> RR ) |
4 |
|
vonioolem1.u |
|- ( ph -> X =/= (/) ) |
5 |
|
vonioolem1.t |
|- ( ( ph /\ k e. X ) -> ( A ` k ) < ( B ` k ) ) |
6 |
|
vonioolem1.c |
|- C = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) ) |
7 |
|
vonioolem1.d |
|- D = ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) |
8 |
|
vonioolem1.s |
|- S = ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) |
9 |
|
vonioolem1.r |
|- T = ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) |
10 |
|
vonioolem1.e |
|- E = inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) |
11 |
|
vonioolem1.n |
|- N = ( ( |_ ` ( 1 / E ) ) + 1 ) |
12 |
|
vonioolem1.z |
|- Z = ( ZZ>= ` N ) |
13 |
9
|
a1i |
|- ( ph -> T = ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) ) |
14 |
6
|
a1i |
|- ( ph -> C = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) ) ) |
15 |
1
|
mptexd |
|- ( ph -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) e. _V ) |
16 |
15
|
adantr |
|- ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) e. _V ) |
17 |
14 16
|
fvmpt2d |
|- ( ( ph /\ n e. NN ) -> ( C ` n ) = ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) ) |
18 |
|
ovexd |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) e. _V ) |
19 |
17 18
|
fvmpt2d |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( A ` k ) + ( 1 / n ) ) ) |
20 |
19
|
oveq2d |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) - ( ( C ` n ) ` k ) ) = ( ( B ` k ) - ( ( A ` k ) + ( 1 / n ) ) ) ) |
21 |
3
|
ffvelrnda |
|- ( ( ph /\ k e. X ) -> ( B ` k ) e. RR ) |
22 |
21
|
adantlr |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. RR ) |
23 |
22
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B ` k ) e. CC ) |
24 |
2
|
adantr |
|- ( ( ph /\ n e. NN ) -> A : X --> RR ) |
25 |
24
|
ffvelrnda |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. RR ) |
26 |
25
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A ` k ) e. CC ) |
27 |
|
nnrecre |
|- ( n e. NN -> ( 1 / n ) e. RR ) |
28 |
27
|
ad2antlr |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR ) |
29 |
28
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. CC ) |
30 |
23 26 29
|
subsub4d |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) = ( ( B ` k ) - ( ( A ` k ) + ( 1 / n ) ) ) ) |
31 |
20 30
|
eqtr4d |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( B ` k ) - ( ( C ` n ) ` k ) ) = ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) |
32 |
31
|
prodeq2dv |
|- ( ( ph /\ n e. NN ) -> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) = prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) |
33 |
32
|
mpteq2dva |
|- ( ph -> ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) ) |
34 |
13 33
|
eqtrd |
|- ( ph -> T = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) ) |
35 |
|
nfv |
|- F/ k ph |
36 |
|
rpssre |
|- RR+ C_ RR |
37 |
2
|
ffvelrnda |
|- ( ( ph /\ k e. X ) -> ( A ` k ) e. RR ) |
38 |
|
difrp |
|- ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) ) |
39 |
37 21 38
|
syl2anc |
|- ( ( ph /\ k e. X ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) ) |
40 |
5 39
|
mpbid |
|- ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) |
41 |
36 40
|
sselid |
|- ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. RR ) |
42 |
41
|
recnd |
|- ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. CC ) |
43 |
|
eqid |
|- ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) = ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) |
44 |
35 1 42 43
|
fprodsubrecnncnv |
|- ( ph -> ( n e. NN |-> prod_ k e. X ( ( ( B ` k ) - ( A ` k ) ) - ( 1 / n ) ) ) ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) ) |
45 |
34 44
|
eqbrtrd |
|- ( ph -> T ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) ) |
46 |
|
nnex |
|- NN e. _V |
47 |
46
|
mptex |
|- ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) e. _V |
48 |
47
|
a1i |
|- ( ph -> ( n e. NN |-> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) e. _V ) |
49 |
9 48
|
eqeltrid |
|- ( ph -> T e. _V ) |
50 |
46
|
mptex |
|- ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) e. _V |
51 |
50
|
a1i |
|- ( ph -> ( n e. NN |-> ( ( voln ` X ) ` ( D ` n ) ) ) e. _V ) |
52 |
8 51
|
eqeltrid |
|- ( ph -> S e. _V ) |
53 |
|
1rp |
|- 1 e. RR+ |
54 |
53
|
a1i |
|- ( ph -> 1 e. RR+ ) |
55 |
|
eqid |
|- ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) = ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) |
56 |
35 55 40
|
rnmptssd |
|- ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR+ ) |
57 |
|
ltso |
|- < Or RR |
58 |
57
|
a1i |
|- ( ph -> < Or RR ) |
59 |
55
|
rnmptfi |
|- ( X e. Fin -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin ) |
60 |
1 59
|
syl |
|- ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin ) |
61 |
35 40 55 4
|
rnmptn0 |
|- ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) =/= (/) ) |
62 |
36
|
a1i |
|- ( ph -> RR+ C_ RR ) |
63 |
56 62
|
sstrd |
|- ( ph -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR ) |
64 |
|
fiinfcl |
|- ( ( < Or RR /\ ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin /\ ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) =/= (/) /\ ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR ) ) -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) |
65 |
58 60 61 63 64
|
syl13anc |
|- ( ph -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) |
66 |
10 65
|
eqeltrid |
|- ( ph -> E e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) |
67 |
56 66
|
sseldd |
|- ( ph -> E e. RR+ ) |
68 |
54 67
|
rpdivcld |
|- ( ph -> ( 1 / E ) e. RR+ ) |
69 |
68
|
rpred |
|- ( ph -> ( 1 / E ) e. RR ) |
70 |
68
|
rpge0d |
|- ( ph -> 0 <_ ( 1 / E ) ) |
71 |
|
flge0nn0 |
|- ( ( ( 1 / E ) e. RR /\ 0 <_ ( 1 / E ) ) -> ( |_ ` ( 1 / E ) ) e. NN0 ) |
72 |
69 70 71
|
syl2anc |
|- ( ph -> ( |_ ` ( 1 / E ) ) e. NN0 ) |
73 |
|
nn0p1nn |
|- ( ( |_ ` ( 1 / E ) ) e. NN0 -> ( ( |_ ` ( 1 / E ) ) + 1 ) e. NN ) |
74 |
72 73
|
syl |
|- ( ph -> ( ( |_ ` ( 1 / E ) ) + 1 ) e. NN ) |
75 |
74
|
nnzd |
|- ( ph -> ( ( |_ ` ( 1 / E ) ) + 1 ) e. ZZ ) |
76 |
11 75
|
eqeltrid |
|- ( ph -> N e. ZZ ) |
77 |
11
|
recnnltrp |
|- ( E e. RR+ -> ( N e. NN /\ ( 1 / N ) < E ) ) |
78 |
67 77
|
syl |
|- ( ph -> ( N e. NN /\ ( 1 / N ) < E ) ) |
79 |
78
|
simpld |
|- ( ph -> N e. NN ) |
80 |
|
uznnssnn |
|- ( N e. NN -> ( ZZ>= ` N ) C_ NN ) |
81 |
79 80
|
syl |
|- ( ph -> ( ZZ>= ` N ) C_ NN ) |
82 |
12 81
|
eqsstrid |
|- ( ph -> Z C_ NN ) |
83 |
82
|
adantr |
|- ( ( ph /\ n e. Z ) -> Z C_ NN ) |
84 |
|
simpr |
|- ( ( ph /\ n e. Z ) -> n e. Z ) |
85 |
83 84
|
sseldd |
|- ( ( ph /\ n e. Z ) -> n e. NN ) |
86 |
7
|
a1i |
|- ( ph -> D = ( n e. NN |-> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) ) |
87 |
1
|
adantr |
|- ( ( ph /\ n e. NN ) -> X e. Fin ) |
88 |
|
eqid |
|- dom ( voln ` X ) = dom ( voln ` X ) |
89 |
25 28
|
readdcld |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) e. RR ) |
90 |
89
|
fmpttd |
|- ( ( ph /\ n e. NN ) -> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) : X --> RR ) |
91 |
17
|
feq1d |
|- ( ( ph /\ n e. NN ) -> ( ( C ` n ) : X --> RR <-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) : X --> RR ) ) |
92 |
90 91
|
mpbird |
|- ( ( ph /\ n e. NN ) -> ( C ` n ) : X --> RR ) |
93 |
3
|
adantr |
|- ( ( ph /\ n e. NN ) -> B : X --> RR ) |
94 |
87 88 92 93
|
hoimbl |
|- ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) e. dom ( voln ` X ) ) |
95 |
94
|
elexd |
|- ( ( ph /\ n e. NN ) -> X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) e. _V ) |
96 |
86 95
|
fvmpt2d |
|- ( ( ph /\ n e. NN ) -> ( D ` n ) = X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) |
97 |
85 96
|
syldan |
|- ( ( ph /\ n e. Z ) -> ( D ` n ) = X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) |
98 |
97
|
fveq2d |
|- ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` ( D ` n ) ) = ( ( voln ` X ) ` X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) ) |
99 |
1
|
adantr |
|- ( ( ph /\ n e. Z ) -> X e. Fin ) |
100 |
4
|
adantr |
|- ( ( ph /\ n e. Z ) -> X =/= (/) ) |
101 |
85 92
|
syldan |
|- ( ( ph /\ n e. Z ) -> ( C ` n ) : X --> RR ) |
102 |
3
|
adantr |
|- ( ( ph /\ n e. Z ) -> B : X --> RR ) |
103 |
|
eqid |
|- X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) = X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) |
104 |
99 100 101 102 103
|
vonn0hoi |
|- ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` X_ k e. X ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = prod_ k e. X ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) ) |
105 |
101
|
ffvelrnda |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( C ` n ) ` k ) e. RR ) |
106 |
85 22
|
syldanl |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( B ` k ) e. RR ) |
107 |
|
volico |
|- ( ( ( ( C ` n ) ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = if ( ( ( C ` n ) ` k ) < ( B ` k ) , ( ( B ` k ) - ( ( C ` n ) ` k ) ) , 0 ) ) |
108 |
105 106 107
|
syl2anc |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = if ( ( ( C ` n ) ` k ) < ( B ` k ) , ( ( B ` k ) - ( ( C ` n ) ` k ) ) , 0 ) ) |
109 |
85 19
|
syldanl |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( C ` n ) ` k ) = ( ( A ` k ) + ( 1 / n ) ) ) |
110 |
85 28
|
syldanl |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / n ) e. RR ) |
111 |
79
|
nnrecred |
|- ( ph -> ( 1 / N ) e. RR ) |
112 |
111
|
ad2antrr |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / N ) e. RR ) |
113 |
41
|
adantlr |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. RR ) |
114 |
12
|
eleq2i |
|- ( n e. Z <-> n e. ( ZZ>= ` N ) ) |
115 |
114
|
biimpi |
|- ( n e. Z -> n e. ( ZZ>= ` N ) ) |
116 |
|
eluzle |
|- ( n e. ( ZZ>= ` N ) -> N <_ n ) |
117 |
115 116
|
syl |
|- ( n e. Z -> N <_ n ) |
118 |
117
|
adantl |
|- ( ( ph /\ n e. Z ) -> N <_ n ) |
119 |
79
|
nnrpd |
|- ( ph -> N e. RR+ ) |
120 |
119
|
adantr |
|- ( ( ph /\ n e. Z ) -> N e. RR+ ) |
121 |
|
nnrp |
|- ( n e. NN -> n e. RR+ ) |
122 |
85 121
|
syl |
|- ( ( ph /\ n e. Z ) -> n e. RR+ ) |
123 |
120 122
|
lerecd |
|- ( ( ph /\ n e. Z ) -> ( N <_ n <-> ( 1 / n ) <_ ( 1 / N ) ) ) |
124 |
118 123
|
mpbid |
|- ( ( ph /\ n e. Z ) -> ( 1 / n ) <_ ( 1 / N ) ) |
125 |
124
|
adantr |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / n ) <_ ( 1 / N ) ) |
126 |
111
|
adantr |
|- ( ( ph /\ k e. X ) -> ( 1 / N ) e. RR ) |
127 |
36 67
|
sselid |
|- ( ph -> E e. RR ) |
128 |
127
|
adantr |
|- ( ( ph /\ k e. X ) -> E e. RR ) |
129 |
78
|
simprd |
|- ( ph -> ( 1 / N ) < E ) |
130 |
129
|
adantr |
|- ( ( ph /\ k e. X ) -> ( 1 / N ) < E ) |
131 |
63
|
adantr |
|- ( ( ph /\ k e. X ) -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR ) |
132 |
60
|
adantr |
|- ( ( ph /\ k e. X ) -> ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin ) |
133 |
|
id |
|- ( k e. X -> k e. X ) |
134 |
|
ovexd |
|- ( k e. X -> ( ( B ` k ) - ( A ` k ) ) e. _V ) |
135 |
55
|
elrnmpt1 |
|- ( ( k e. X /\ ( ( B ` k ) - ( A ` k ) ) e. _V ) -> ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) |
136 |
133 134 135
|
syl2anc |
|- ( k e. X -> ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) |
137 |
136
|
adantl |
|- ( ( ph /\ k e. X ) -> ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) |
138 |
|
infrefilb |
|- ( ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) C_ RR /\ ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) e. Fin /\ ( ( B ` k ) - ( A ` k ) ) e. ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) ) -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) <_ ( ( B ` k ) - ( A ` k ) ) ) |
139 |
131 132 137 138
|
syl3anc |
|- ( ( ph /\ k e. X ) -> inf ( ran ( k e. X |-> ( ( B ` k ) - ( A ` k ) ) ) , RR , < ) <_ ( ( B ` k ) - ( A ` k ) ) ) |
140 |
10 139
|
eqbrtrid |
|- ( ( ph /\ k e. X ) -> E <_ ( ( B ` k ) - ( A ` k ) ) ) |
141 |
126 128 41 130 140
|
ltletrd |
|- ( ( ph /\ k e. X ) -> ( 1 / N ) < ( ( B ` k ) - ( A ` k ) ) ) |
142 |
141
|
adantlr |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / N ) < ( ( B ` k ) - ( A ` k ) ) ) |
143 |
110 112 113 125 142
|
lelttrd |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( 1 / n ) < ( ( B ` k ) - ( A ` k ) ) ) |
144 |
85 25
|
syldanl |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( A ` k ) e. RR ) |
145 |
144 110 106
|
ltaddsub2d |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( ( A ` k ) + ( 1 / n ) ) < ( B ` k ) <-> ( 1 / n ) < ( ( B ` k ) - ( A ` k ) ) ) ) |
146 |
143 145
|
mpbird |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( A ` k ) + ( 1 / n ) ) < ( B ` k ) ) |
147 |
109 146
|
eqbrtrd |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( ( C ` n ) ` k ) < ( B ` k ) ) |
148 |
147
|
iftrued |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> if ( ( ( C ` n ) ` k ) < ( B ` k ) , ( ( B ` k ) - ( ( C ` n ) ` k ) ) , 0 ) = ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) |
149 |
108 148
|
eqtrd |
|- ( ( ( ph /\ n e. Z ) /\ k e. X ) -> ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) |
150 |
149
|
prodeq2dv |
|- ( ( ph /\ n e. Z ) -> prod_ k e. X ( vol ` ( ( ( C ` n ) ` k ) [,) ( B ` k ) ) ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) |
151 |
98 104 150
|
3eqtrd |
|- ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` ( D ` n ) ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) |
152 |
|
fvexd |
|- ( ( ph /\ n e. Z ) -> ( ( voln ` X ) ` ( D ` n ) ) e. _V ) |
153 |
8
|
fvmpt2 |
|- ( ( n e. NN /\ ( ( voln ` X ) ` ( D ` n ) ) e. _V ) -> ( S ` n ) = ( ( voln ` X ) ` ( D ` n ) ) ) |
154 |
85 152 153
|
syl2anc |
|- ( ( ph /\ n e. Z ) -> ( S ` n ) = ( ( voln ` X ) ` ( D ` n ) ) ) |
155 |
|
prodex |
|- prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) e. _V |
156 |
155
|
a1i |
|- ( ( ph /\ n e. Z ) -> prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) e. _V ) |
157 |
9
|
fvmpt2 |
|- ( ( n e. NN /\ prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) e. _V ) -> ( T ` n ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) |
158 |
85 156 157
|
syl2anc |
|- ( ( ph /\ n e. Z ) -> ( T ` n ) = prod_ k e. X ( ( B ` k ) - ( ( C ` n ) ` k ) ) ) |
159 |
151 154 158
|
3eqtr4rd |
|- ( ( ph /\ n e. Z ) -> ( T ` n ) = ( S ` n ) ) |
160 |
12 49 52 76 159
|
climeq |
|- ( ph -> ( T ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) <-> S ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) ) ) |
161 |
45 160
|
mpbid |
|- ( ph -> S ~~> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) ) |