Metamath Proof Explorer


Theorem reprle

Description: Upper bound to the terms in the representations of M as the sum of S nonnegative integers from set A . (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses reprval.a
|- ( ph -> A C_ NN )
reprval.m
|- ( ph -> M e. ZZ )
reprval.s
|- ( ph -> S e. NN0 )
reprf.c
|- ( ph -> C e. ( A ( repr ` S ) M ) )
reprle.x
|- ( ph -> X e. ( 0 ..^ S ) )
Assertion reprle
|- ( ph -> ( C ` X ) <_ M )

Proof

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 )