This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashrepr

Description: Develop the number of representations of an integer M as a sum of nonnegative integers in set A . (Contributed by Thierry Arnoux, 14-Dec-2021)

		Ref	Expression
	Hypotheses	hashrepr.a	$⊢ φ \to A \subseteq ℕ$
		hashrepr.m	$⊢ φ \to M \in ℕ_{0}$
		hashrepr.s	$⊢ φ \to S \in ℕ_{0}$
	Assertion	hashrepr	$⊢ φ \to \|A repr (S) M\| = \sum_{c \in ℕ repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$

Proof

Step	Hyp	Ref	Expression
1		hashrepr.a	$⊢ φ \to A \subseteq ℕ$
2		hashrepr.m	$⊢ φ \to M \in ℕ_{0}$
3		hashrepr.s	$⊢ φ \to S \in ℕ_{0}$
4	2	nn0zd	$⊢ φ \to M \in ℤ$
5		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
6		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
7	6	a1i	$⊢ φ \to (1 \dots M) \subseteq ℕ$
8	1 4 3 5 7	hashreprin	$⊢ φ \to \|(A \cap (1 \dots M)) repr (S) M\| = \sum_{c \in (1 \dots M) repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
9	2 3 1	reprinfz1	$⊢ φ \to A repr (S) M = (A \cap (1 \dots M)) repr (S) M$
10	9	fveq2d	$⊢ φ \to \|A repr (S) M\| = \|(A \cap (1 \dots M)) repr (S) M\|$
11	2 3	reprfz1	$⊢ φ \to ℕ repr (S) M = (1 \dots M) repr (S) M$
12	11	sumeq1d	$⊢ φ \to \sum_{c \in ℕ repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) = \sum_{c \in (1 \dots M) repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
13	8 10 12	3eqtr4d	$⊢ φ \to \|A repr (S) M\| = \sum_{c \in ℕ repr (S) M} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$