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	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to AB=\sum _{k=1}^{A}B$$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$$⊢A\in {\mathbb{N}}_0\to \left(1\dots A\right)\in \mathrm{Fin}$$
2		nn0cn	$$⊢B\in {\mathbb{N}}_0\to B\in ℂ$$
3		fsumconst	$$⊢\left(\left(1\dots A\right)\in \mathrm{Fin}\wedge B\in ℂ\right)\to \sum _{k=1}^{A}B=\left|\left(1\dots A\right)\right|B$$
4	1 2 3	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \sum _{k=1}^{A}B=\left|\left(1\dots A\right)\right|B$$
5		hashfz1	$$⊢A\in {\mathbb{N}}_0\to \left|\left(1\dots A\right)\right|=A$$
6	5	adantr	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left|\left(1\dots A\right)\right|=A$$
7	6	oveq1d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left|\left(1\dots A\right)\right|B=AB$$
8	4 7	eqtr2d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to AB=\sum _{k=1}^{A}B$$