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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
	reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	reprf.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
	reprle.x	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝑆 ) )
Assertion	reprle	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) ≤ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		reprval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2		reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4		reprf.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
5		reprle.x	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝑆 ) )
6		fveq2	⊢ ( 𝑎 = 𝑋 → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ 𝑋 ) )
7		fzofi	⊢ ( 0 ..^ 𝑆 ) ∈ Fin
8	7	a1i	⊢ ( 𝜑 → ( 0 ..^ 𝑆 ) ∈ Fin )
9	1 2 3 4	reprsum	⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 )
10	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℕ )
11	1 2 3 4	reprf	⊢ ( 𝜑 → 𝐶 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
12	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐶 ‘ 𝑎 ) ∈ 𝐴 )
13	10 12	sseldd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐶 ‘ 𝑎 ) ∈ ℕ )
14	13	nnrpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐶 ‘ 𝑎 ) ∈ ℝ+ )
15	6 8 9 14 5	fsumub	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) ≤ 𝑀 )