Theorem nn0mullong

Description: Standard algorithm (also known as "long multiplication" or "grade-school multiplication") to calculate the product of two nonnegative integers a and b by multiplying the multiplicand b by each digit of the multiplier a and then add up all the properly shifted results. Here, the binary representation of the multiplier a is used, i.e., the above mentioned "digits" are 0 or 1. This is a similar result as provided by smumul . (Contributed by AV, 7-Jun-2020)

	Ref	Expression
Assertion	nn0mullong	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) x. B ) )

Proof

Step	Hyp	Ref	Expression
1		nn0sumshdig	|- ( A e. NN0 -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )
2	1	adantr	|- ( ( A e. NN0 /\ B e. NN0 ) -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )
3	2	oveq1d	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = ( sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) x. B ) )
4		fzofi	|- ( 0 ..^ ( #b ` A ) ) e. Fin
5	4	a1i	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( 0 ..^ ( #b ` A ) ) e. Fin )
6		nn0cn	|- ( B e. NN0 -> B e. CC )
7	6	adantl	|- ( ( A e. NN0 /\ B e. NN0 ) -> B e. CC )
8		2nn	|- 2 e. NN
9	8	a1i	|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> 2 e. NN )
10		elfzoelz	|- ( k e. ( 0 ..^ ( #b ` A ) ) -> k e. ZZ )
11	10	adantl	|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> k e. ZZ )
12		nn0rp0	|- ( A e. NN0 -> A e. ( 0 [,) +oo ) )
13	12	adantr	|- ( ( A e. NN0 /\ B e. NN0 ) -> A e. ( 0 [,) +oo ) )
14	13	adantr	|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> A e. ( 0 [,) +oo ) )
15		digvalnn0	|- ( ( 2 e. NN /\ k e. ZZ /\ A e. ( 0 [,) +oo ) ) -> ( k ( digit ` 2 ) A ) e. NN0 )
16	9 11 14 15	syl3anc	|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> ( k ( digit ` 2 ) A ) e. NN0 )
17	16	nn0cnd	|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> ( k ( digit ` 2 ) A ) e. CC )
18		2nn0	|- 2 e. NN0
19	18	a1i	|- ( k e. ( 0 ..^ ( #b ` A ) ) -> 2 e. NN0 )
20		elfzonn0	|- ( k e. ( 0 ..^ ( #b ` A ) ) -> k e. NN0 )
21	19 20	nn0expcld	|- ( k e. ( 0 ..^ ( #b ` A ) ) -> ( 2 ^ k ) e. NN0 )
22	21	nn0cnd	|- ( k e. ( 0 ..^ ( #b ` A ) ) -> ( 2 ^ k ) e. CC )
23	22	adantl	|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> ( 2 ^ k ) e. CC )
24	17 23	mulcld	|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) e. CC )
25	5 7 24	fsummulc1	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) x. B ) = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) x. B ) )
26	3 25	eqtrd	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) x. B ) )