Step |
Hyp |
Ref |
Expression |
1 |
|
reprval.a |
|- ( ph -> A C_ NN ) |
2 |
|
reprval.m |
|- ( ph -> M e. ZZ ) |
3 |
|
reprval.s |
|- ( ph -> S e. NN0 ) |
4 |
|
reprf.c |
|- ( ph -> C e. ( A ( repr ` S ) M ) ) |
5 |
|
reprle.x |
|- ( ph -> X e. ( 0 ..^ S ) ) |
6 |
|
fveq2 |
|- ( a = X -> ( C ` a ) = ( C ` X ) ) |
7 |
|
fzofi |
|- ( 0 ..^ S ) e. Fin |
8 |
7
|
a1i |
|- ( ph -> ( 0 ..^ S ) e. Fin ) |
9 |
1 2 3 4
|
reprsum |
|- ( ph -> sum_ a e. ( 0 ..^ S ) ( C ` a ) = M ) |
10 |
1
|
adantr |
|- ( ( ph /\ a e. ( 0 ..^ S ) ) -> A C_ NN ) |
11 |
1 2 3 4
|
reprf |
|- ( ph -> C : ( 0 ..^ S ) --> A ) |
12 |
11
|
ffvelrnda |
|- ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( C ` a ) e. A ) |
13 |
10 12
|
sseldd |
|- ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( C ` a ) e. NN ) |
14 |
13
|
nnrpd |
|- ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( C ` a ) e. RR+ ) |
15 |
6 8 9 14 5
|
fsumub |
|- ( ph -> ( C ` X ) <_ M ) |