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	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝐴 ∈ ℕ0 → ( 1 ... 𝐴 ) ∈ Fin )
2		nn0cn	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℂ )
3		fsumconst	⊢ ( ( ( 1 ... 𝐴 ) ∈ Fin ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝐴 ) 𝐵 = ( ( ♯ ‘ ( 1 ... 𝐴 ) ) · 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 1 ... 𝐴 ) 𝐵 = ( ( ♯ ‘ ( 1 ... 𝐴 ) ) · 𝐵 ) )
5		hashfz1	⊢ ( 𝐴 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐴 ) ) = 𝐴 )
6	5	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ♯ ‘ ( 1 ... 𝐴 ) ) = 𝐴 )
7	6	oveq1d	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( ♯ ‘ ( 1 ... 𝐴 ) ) · 𝐵 ) = ( 𝐴 · 𝐵 ) )
8	4 7	eqtr2d	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = Σ 𝑘 ∈ ( 1 ... 𝐴 ) 𝐵 )