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 )