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 
|- ( ph -> A C_ NN )
hashrepr.m 
|- ( ph -> M e. NN0 )
hashrepr.s 
|- ( ph -> S e. NN0 )
Assertion hashrepr 
|- ( ph -> ( # ` ( A ( repr ` S ) M ) ) = sum_ c e. ( NN ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )

Proof

Step Hyp Ref Expression
1 hashrepr.a 
 |-  ( ph -> A C_ NN )
2 hashrepr.m 
 |-  ( ph -> M e. NN0 )
3 hashrepr.s 
 |-  ( ph -> S e. NN0 )
4 2 nn0zd 
 |-  ( ph -> M e. ZZ )
5 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
6 fz1ssnn 
 |-  ( 1 ... M ) C_ NN
7 6 a1i 
 |-  ( ph -> ( 1 ... M ) C_ NN )
8 1 4 3 5 7 hashreprin 
 |-  ( ph -> ( # ` ( ( A i^i ( 1 ... M ) ) ( repr ` S ) M ) ) = sum_ c e. ( ( 1 ... M ) ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
9 2 3 1 reprinfz1 
 |-  ( ph -> ( A ( repr ` S ) M ) = ( ( A i^i ( 1 ... M ) ) ( repr ` S ) M ) )
10 9 fveq2d 
 |-  ( ph -> ( # ` ( A ( repr ` S ) M ) ) = ( # ` ( ( A i^i ( 1 ... M ) ) ( repr ` S ) M ) ) )
11 2 3 reprfz1 
 |-  ( ph -> ( NN ( repr ` S ) M ) = ( ( 1 ... M ) ( repr ` S ) M ) )
12 11 sumeq1d 
 |-  ( ph -> sum_ c e. ( NN ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) = sum_ c e. ( ( 1 ... M ) ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
13 8 10 12 3eqtr4d 
 |-  ( ph -> ( # ` ( A ( repr ` S ) M ) ) = sum_ c e. ( NN ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )