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	$⊢ φ \to A \subseteq ℕ$
		reprval.m	$⊢ φ \to M \in ℤ$
		reprval.s	$⊢ φ \to S \in ℕ_{0}$
		reprf.c	$⊢ φ \to C \in (A repr (S) M)$
		reprle.x	$⊢ φ \to X \in (0 ..^S)$
	Assertion	reprle	$⊢ φ \to C (X) \leq M$

Proof

Step	Hyp	Ref	Expression
1		reprval.a	$⊢ φ \to A \subseteq ℕ$
2		reprval.m	$⊢ φ \to M \in ℤ$
3		reprval.s	$⊢ φ \to S \in ℕ_{0}$
4		reprf.c	$⊢ φ \to C \in (A repr (S) M)$
5		reprle.x	$⊢ φ \to X \in (0 ..^S)$
6		fveq2	$⊢ a = X \to C (a) = C (X)$
7		fzofi	$⊢ (0 ..^S) \in Fin$
8	7	a1i	$⊢ φ \to (0 ..^S) \in Fin$
9	1 2 3 4	reprsum	$⊢ φ \to \sum_{a \in (0 ..^S)} C (a) = M$
10	1	adantr	$⊢ (φ \land a \in (0 ..^S)) \to A \subseteq ℕ$
11	1 2 3 4	reprf	$⊢ φ \to C : (0 ..^S) ⟶ A$
12	11	ffvelcdmda	$⊢ (φ \land a \in (0 ..^S)) \to C (a) \in A$
13	10 12	sseldd	$⊢ (φ \land a \in (0 ..^S)) \to C (a) \in ℕ$
14	13	nnrpd	$⊢ (φ \land a \in (0 ..^S)) \to C (a) \in ℝ^{+}$
15	6 8 9 14 5	fsumub	$⊢ φ \to C (X) \leq M$