Theorem nn0mulfsum

Description: Trivial algorithm to calculate the product of two nonnegative integers a and b by adding b to itself a times. (Contributed by AV, 17-May-2020)

	Ref	Expression
Assertion	nn0mulfsum	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = sum_ k e. ( 1 ... A ) B )

Proof

Step	Hyp	Ref	Expression
1		fzfid	|- ( A e. NN0 -> ( 1 ... A ) e. Fin )
2		nn0cn	|- ( B e. NN0 -> B e. CC )
3		fsumconst	|- ( ( ( 1 ... A ) e. Fin /\ B e. CC ) -> sum_ k e. ( 1 ... A ) B = ( ( # ` ( 1 ... A ) ) x. B ) )
4	1 2 3	syl2an	|- ( ( A e. NN0 /\ B e. NN0 ) -> sum_ k e. ( 1 ... A ) B = ( ( # ` ( 1 ... A ) ) x. B ) )
5		hashfz1	|- ( A e. NN0 -> ( # ` ( 1 ... A ) ) = A )
6	5	adantr	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( # ` ( 1 ... A ) ) = A )
7	6	oveq1d	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( # ` ( 1 ... A ) ) x. B ) = ( A x. B ) )
8	4 7	eqtr2d	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = sum_ k e. ( 1 ... A ) B )