Metamath Proof Explorer


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 A0
karatsuba.b B0
karatsuba.c C0
karatsuba.d D0
karatsuba.s S0
karatsuba.m M0
karatsuba.r AC=R
karatsuba.t BD=T
karatsuba.e A+BC+D=R+S+T
karatsuba.x A10M+B=X
karatsuba.y C10M+D=Y
karatsuba.w R10M+S=W
karatsuba.z W10M+T=Z
Assertion karatsuba XY=Z

Proof

Step Hyp Ref Expression
1 karatsuba.a A0
2 karatsuba.b B0
3 karatsuba.c C0
4 karatsuba.d D0
5 karatsuba.s S0
6 karatsuba.m M0
7 karatsuba.r AC=R
8 karatsuba.t BD=T
9 karatsuba.e A+BC+D=R+S+T
10 karatsuba.x A10M+B=X
11 karatsuba.y C10M+D=Y
12 karatsuba.w R10M+S=W
13 karatsuba.z W10M+T=Z
14 1 nn0cni A
15 10nn0 100
16 15 nn0cni 10
17 expcl 10M010M
18 16 6 17 mp2an 10M
19 14 18 mulcli A10M
20 2 nn0cni B
21 3 nn0cni C
22 21 18 mulcli C10M
23 4 nn0cni D
24 19 20 22 23 muladdi A10M+BC10M+D=A10MC10M+DB+A10MD+C10MB
25 19 22 mulcli A10MC10M
26 23 20 mulcli DB
27 19 23 mulcli A10MD
28 22 20 mulcli C10MB
29 27 28 addcli A10MD+C10MB
30 25 26 29 add32i A10MC10M+DB+A10MD+C10MB=A10MC10M+A10MD+C10MB+DB
31 19 21 mulcli A10MC
32 5 nn0cni S
33 31 32 18 adddiri A10MC+S10M=A10MC10M+S10M
34 14 18 21 mul32i A10MC=AC10M
35 7 oveq1i AC10M=R10M
36 34 35 eqtri A10MC=R10M
37 36 oveq1i A10MC+S=R10M+S
38 37 12 eqtri A10MC+S=W
39 38 oveq1i A10MC+S10M=W10M
40 19 21 18 mulassi A10MC10M=A10MC10M
41 14 21 mulcli AC
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 A+BC+D=AC+DB+AD+CB
48 46 9 47 3eqtr2i AC+DB+S=AC+DB+AD+CB
49 41 26 addcli AC+DB
50 14 23 mulcli AD
51 21 20 mulcli CB
52 50 51 addcli AD+CB
53 49 32 52 addcani AC+DB+S=AC+DB+AD+CBS=AD+CB
54 48 53 mpbi S=AD+CB
55 54 oveq1i S10M=AD+CB10M
56 50 51 18 adddiri AD+CB10M=AD10M+CB10M
57 14 23 18 mul32i AD10M=A10MD
58 21 20 18 mul32i CB10M=C10MB
59 57 58 oveq12i AD10M+CB10M=A10MD+C10MB
60 55 56 59 3eqtri S10M=A10MD+C10MB
61 40 60 oveq12i A10MC10M+S10M=A10MC10M+A10MD+C10MB
62 33 39 61 3eqtr3ri A10MC10M+A10MD+C10MB=W10M
63 62 44 oveq12i A10MC10M+A10MD+C10MB+DB=W10M+T
64 24 30 63 3eqtri A10M+BC10M+D=W10M+T
65 10 11 oveq12i A10M+BC10M+D=XY
66 64 65 13 3eqtr3i XY=Z