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	$$⊢\phi \to A\subseteq \mathbb{N}$$
	reprval.m	$$⊢\phi \to M\in \mathbb{Z}$$
	reprval.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	reprf.c	$$⊢\phi \to C\in \left(A\mathrm{repr}\left(S\right)M\right)$$
	reprle.x	$$⊢\phi \to X\in \left(0..^S\right)$$
Assertion	reprle	$$⊢\phi \to C\left(X\right)\le M$$

Proof

Step	Hyp	Ref	Expression
1		reprval.a	$$⊢\phi \to A\subseteq \mathbb{N}$$
2		reprval.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		reprval.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
4		reprf.c	$$⊢\phi \to C\in \left(A\mathrm{repr}\left(S\right)M\right)$$
5		reprle.x	$$⊢\phi \to X\in \left(0..^S\right)$$
6		fveq2	$$⊢a=X\to C\left(a\right)=C\left(X\right)$$
7		fzofi	$$⊢\left(0..^S\right)\in \mathrm{Fin}$$
8	7	a1i	$$⊢\phi \to \left(0..^S\right)\in \mathrm{Fin}$$
9	1 2 3 4	reprsum	$$⊢\phi \to \sum _{a\in \left(0..^S\right)}C\left(a\right)=M$$
10	1	adantr	$$⊢\left(\phi \wedge a\in \left(0..^S\right)\right)\to A\subseteq \mathbb{N}$$
11	1 2 3 4	reprf	$$⊢\phi \to C:\left(0..^S\right)⟶A$$
12	11	ffvelcdmda	$$⊢\left(\phi \wedge a\in \left(0..^S\right)\right)\to C\left(a\right)\in A$$
13	10 12	sseldd	$$⊢\left(\phi \wedge a\in \left(0..^S\right)\right)\to C\left(a\right)\in \mathbb{N}$$
14	13	nnrpd	$$⊢\left(\phi \wedge a\in \left(0..^S\right)\right)\to C\left(a\right)\in {ℝ}^{+}$$
15	6 8 9 14 5	fsumub	$$⊢\phi \to C\left(X\right)\le M$$