This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda 
 |-  ( ( 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 )