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 φ A
reprval.m φ M
reprval.s φ S 0
reprf.c φ C A repr S M
reprle.x φ X 0 ..^ S
Assertion reprle φ C X M

Proof

Step Hyp Ref Expression
1 reprval.a φ A
2 reprval.m φ M
3 reprval.s φ S 0
4 reprf.c φ C A repr S M
5 reprle.x φ X 0 ..^ S
6 fveq2 a = X C a = C X
7 fzofi 0 ..^ S Fin
8 7 a1i φ 0 ..^ S Fin
9 1 2 3 4 reprsum φ a 0 ..^ S C a = M
10 1 adantr φ a 0 ..^ S A
11 1 2 3 4 reprf φ C : 0 ..^ S A
12 11 ffvelrnda φ a 0 ..^ S C a A
13 10 12 sseldd φ a 0 ..^ S C a
14 13 nnrpd φ a 0 ..^ S C a +
15 6 8 9 14 5 fsumub φ C X M