Theorem karatsuba

Description: The Karatsuba multiplication algorithm. If X and Y are decomposed into two groups of digits of length M (only the lower group is known to be this size but the algorithm is most efficient when the partition is chosen near the middle of the digit string), then X Y can be written in three groups of digits, where each group needs only one multiplication. Thus, we can halve both inputs with only three multiplications on the smaller operands, yielding an asymptotic improvement of n^(log_2 3) instead of n^2 for the "naive" algorithm decmul1c . (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 9-Sep-2021)

	Ref	Expression
Hypotheses	karatsuba.a	$$⊢A\in {\mathbb{N}}_0$$
	karatsuba.b	$$⊢B\in {\mathbb{N}}_0$$
	karatsuba.c	$$⊢C\in {\mathbb{N}}_0$$
	karatsuba.d	$$⊢D\in {\mathbb{N}}_0$$
	karatsuba.s	$$⊢S\in {\mathbb{N}}_0$$
	karatsuba.m	$$⊢M\in {\mathbb{N}}_0$$
	karatsuba.r	$$⊢AC=R$$
	karatsuba.t	$$⊢BD=T$$
	karatsuba.e	$$⊢\left(A+B\right)\left(C+D\right)=R+S+T$$
	karatsuba.x	$$⊢A{10}^M+B=X$$
	karatsuba.y	$$⊢C{10}^M+D=Y$$
	karatsuba.w	$$⊢R{10}^M+S=W$$
	karatsuba.z	$$⊢W{10}^M+T=Z$$
Assertion	karatsuba	$$⊢XY=Z$$

Proof

Step	Hyp	Ref	Expression
1		karatsuba.a	$$⊢A\in {\mathbb{N}}_0$$
2		karatsuba.b	$$⊢B\in {\mathbb{N}}_0$$
3		karatsuba.c	$$⊢C\in {\mathbb{N}}_0$$
4		karatsuba.d	$$⊢D\in {\mathbb{N}}_0$$
5		karatsuba.s	$$⊢S\in {\mathbb{N}}_0$$
6		karatsuba.m	$$⊢M\in {\mathbb{N}}_0$$
7		karatsuba.r	$$⊢AC=R$$
8		karatsuba.t	$$⊢BD=T$$
9		karatsuba.e	$$⊢\left(A+B\right)\left(C+D\right)=R+S+T$$
10		karatsuba.x	$$⊢A{10}^M+B=X$$
11		karatsuba.y	$$⊢C{10}^M+D=Y$$
12		karatsuba.w	$$⊢R{10}^M+S=W$$
13		karatsuba.z	$$⊢W{10}^M+T=Z$$
14	1	nn0cni	$$⊢A\in ℂ$$
15		10nn0	$$⊢10\in {\mathbb{N}}_0$$
16	15	nn0cni	$$⊢10\in ℂ$$
17		expcl	$$⊢\left(10\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to {10}^M\in ℂ$$
18	16 6 17	mp2an	$$⊢{10}^M\in ℂ$$
19	14 18	mulcli	$$⊢A{10}^M\in ℂ$$
20	2	nn0cni	$$⊢B\in ℂ$$
21	3	nn0cni	$$⊢C\in ℂ$$
22	21 18	mulcli	$$⊢C{10}^M\in ℂ$$
23	4	nn0cni	$$⊢D\in ℂ$$
24	19 20 22 23	muladdi	$$⊢\left(A{10}^M+B\right)\left(C{10}^M+D\right)=A{10}^{M}C{10}^M+DB+A{10}^{M}D+C{10}^{M}B$$
25	19 22	mulcli	$$⊢A{10}^{M}C{10}^M\in ℂ$$
26	23 20	mulcli	$$⊢DB\in ℂ$$
27	19 23	mulcli	$$⊢A{10}^{M}D\in ℂ$$
28	22 20	mulcli	$$⊢C{10}^{M}B\in ℂ$$
29	27 28	addcli	$$⊢A{10}^{M}D+C{10}^{M}B\in ℂ$$
30	25 26 29	add32i	$$⊢A{10}^{M}C{10}^M+DB+A{10}^{M}D+C{10}^{M}B=A{10}^{M}C{10}^M+\left(A{10}^{M}D+C{10}^{M}B\right)+DB$$
31	19 21	mulcli	$$⊢A{10}^{M}C\in ℂ$$
32	5	nn0cni	$$⊢S\in ℂ$$
33	31 32 18	adddiri	$$⊢\left(A{10}^{M}C+S\right){10}^M=A{10}^{M}C{10}^M+S{10}^M$$
34	14 18 21	mul32i	$$⊢A{10}^{M}C=AC{10}^M$$
35	7	oveq1i	$$⊢AC{10}^M=R{10}^M$$
36	34 35	eqtri	$$⊢A{10}^{M}C=R{10}^M$$
37	36	oveq1i	$$⊢A{10}^{M}C+S=R{10}^M+S$$
38	37 12	eqtri	$$⊢A{10}^{M}C+S=W$$
39	38	oveq1i	$$⊢\left(A{10}^{M}C+S\right){10}^M=W{10}^M$$
40	19 21 18	mulassi	$$⊢A{10}^{M}C{10}^M=A{10}^{M}C{10}^M$$
41	14 21	mulcli	$$⊢AC\in ℂ$$
42	41 26 32	add32i	$$⊢AC+DB+S=AC+S+DB$$
43	7	oveq1i	$$⊢AC+S=R+S$$
44	20 23 8	mulcomli	$$⊢DB=T$$
45	43 44	oveq12i	$$⊢AC+S+DB=R+S+T$$
46	42 45	eqtri	$$⊢AC+DB+S=R+S+T$$
47	14 20 21 23	muladdi	$$⊢\left(A+B\right)\left(C+D\right)=AC+DB+AD+CB$$
48	46 9 47	3eqtr2i	$$⊢AC+DB+S=AC+DB+AD+CB$$
49	41 26	addcli	$$⊢AC+DB\in ℂ$$
50	14 23	mulcli	$$⊢AD\in ℂ$$
51	21 20	mulcli	$$⊢CB\in ℂ$$
52	50 51	addcli	$$⊢AD+CB\in ℂ$$
53	49 32 52	addcani	$$⊢AC+DB+S=AC+DB+AD+CB\leftrightarrow S=AD+CB$$
54	48 53	mpbi	$$⊢S=AD+CB$$
55	54	oveq1i	$$⊢S{10}^M=\left(AD+CB\right){10}^M$$
56	50 51 18	adddiri	$$⊢\left(AD+CB\right){10}^M=AD{10}^M+CB{10}^M$$
57	14 23 18	mul32i	$$⊢AD{10}^M=A{10}^{M}D$$
58	21 20 18	mul32i	$$⊢CB{10}^M=C{10}^{M}B$$
59	57 58	oveq12i	$$⊢AD{10}^M+CB{10}^M=A{10}^{M}D+C{10}^{M}B$$
60	55 56 59	3eqtri	$$⊢S{10}^M=A{10}^{M}D+C{10}^{M}B$$
61	40 60	oveq12i	$$⊢A{10}^{M}C{10}^M+S{10}^M=A{10}^{M}C{10}^M+A{10}^{M}D+C{10}^{M}B$$
62	33 39 61	3eqtr3ri	$$⊢A{10}^{M}C{10}^M+A{10}^{M}D+C{10}^{M}B=W{10}^M$$
63	62 44	oveq12i	$$⊢A{10}^{M}C{10}^M+\left(A{10}^{M}D+C{10}^{M}B\right)+DB=W{10}^M+T$$
64	24 30 63	3eqtri	$$⊢\left(A{10}^M+B\right)\left(C{10}^M+D\right)=W{10}^M+T$$
65	10 11	oveq12i	$$⊢\left(A{10}^M+B\right)\left(C{10}^M+D\right)=XY$$
66	64 65 13	3eqtr3i	$$⊢XY=Z$$