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 ⊢ 𝐴 ∈ ℕ0
karatsuba.b ⊢ 𝐵 ∈ ℕ0
karatsuba.c ⊢ 𝐶 ∈ ℕ0
karatsuba.d ⊢ 𝐷 ∈ ℕ0
karatsuba.s ⊢ 𝑆 ∈ ℕ0
karatsuba.m ⊢ 𝑀 ∈ ℕ0
karatsuba.r ⊢ ( 𝐴 · 𝐶 ) = 𝑅
karatsuba.t ⊢ ( 𝐵 · 𝐷 ) = 𝑇
karatsuba.e ⊢ ( ( 𝐴 + 𝐵 ) · ( 𝐶 + 𝐷 ) ) = ( ( 𝑅 + 𝑆 ) + 𝑇 )
karatsuba.x ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) = 𝑋
karatsuba.y ⊢ ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) + 𝐷 ) = 𝑌
karatsuba.w ⊢ ( ( 𝑅 · ( 1 0 ↑ 𝑀 ) ) + 𝑆 ) = 𝑊
karatsuba.z ⊢ ( ( 𝑊 · ( 1 0 ↑ 𝑀 ) ) + 𝑇 ) = 𝑍
Assertion karatsuba ( 𝑋 · 𝑌 ) = 𝑍

Proof

Step Hyp Ref Expression
1 karatsuba.a ⊢ 𝐴 ∈ ℕ0
2 karatsuba.b ⊢ 𝐵 ∈ ℕ0
3 karatsuba.c ⊢ 𝐶 ∈ ℕ0
4 karatsuba.d ⊢ 𝐷 ∈ ℕ0
5 karatsuba.s ⊢ 𝑆 ∈ ℕ0
6 karatsuba.m ⊢ 𝑀 ∈ ℕ0
7 karatsuba.r ⊢ ( 𝐴 · 𝐶 ) = 𝑅
8 karatsuba.t ⊢ ( 𝐵 · 𝐷 ) = 𝑇
9 karatsuba.e ⊢ ( ( 𝐴 + 𝐵 ) · ( 𝐶 + 𝐷 ) ) = ( ( 𝑅 + 𝑆 ) + 𝑇 )
10 karatsuba.x ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) = 𝑋
11 karatsuba.y ⊢ ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) + 𝐷 ) = 𝑌
12 karatsuba.w ⊢ ( ( 𝑅 · ( 1 0 ↑ 𝑀 ) ) + 𝑆 ) = 𝑊
13 karatsuba.z ⊢ ( ( 𝑊 · ( 1 0 ↑ 𝑀 ) ) + 𝑇 ) = 𝑍
14 1 nn0cni ⊢ 𝐴 ∈ ℂ
15 10nn0 ⊢ 1 0 ∈ ℕ0
16 15 nn0cni ⊢ 1 0 ∈ ℂ
17 expcl ⊢ ( ( 1 0 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 1 0 ↑ 𝑀 ) ∈ ℂ )
18 16 6 17 mp2an ⊢ ( 1 0 ↑ 𝑀 ) ∈ ℂ
19 14 18 mulcli ⊢ ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ∈ ℂ
20 2 nn0cni ⊢ 𝐵 ∈ ℂ
21 3 nn0cni ⊢ 𝐶 ∈ ℂ
22 21 18 mulcli ⊢ ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ∈ ℂ
23 4 nn0cni ⊢ 𝐷 ∈ ℂ
24 19 20 22 23 muladdi ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) · ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) + 𝐷 ) ) = ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ) + ( 𝐷 · 𝐵 ) ) + ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ) )
25 19 22 mulcli ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ) ∈ ℂ
26 23 20 mulcli ⊢ ( 𝐷 · 𝐵 ) ∈ ℂ
27 19 23 mulcli ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) ∈ ℂ
28 22 20 mulcli ⊢ ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ∈ ℂ
29 27 28 addcli ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ) ∈ ℂ
30 25 26 29 add32i ⊢ ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ) + ( 𝐷 · 𝐵 ) ) + ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ) ) = ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ) + ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ) ) + ( 𝐷 · 𝐵 ) )
31 19 21 mulcli ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) ∈ ℂ
32 5 nn0cni ⊢ 𝑆 ∈ ℂ
33 31 32 18 adddiri ⊢ ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) + 𝑆 ) · ( 1 0 ↑ 𝑀 ) ) = ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) · ( 1 0 ↑ 𝑀 ) ) + ( 𝑆 · ( 1 0 ↑ 𝑀 ) ) )
34 14 18 21 mul32i ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) · ( 1 0 ↑ 𝑀 ) )
35 7 oveq1i ⊢ ( ( 𝐴 · 𝐶 ) · ( 1 0 ↑ 𝑀 ) ) = ( 𝑅 · ( 1 0 ↑ 𝑀 ) )
36 34 35 eqtri ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) = ( 𝑅 · ( 1 0 ↑ 𝑀 ) )
37 36 oveq1i ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) + 𝑆 ) = ( ( 𝑅 · ( 1 0 ↑ 𝑀 ) ) + 𝑆 )
38 37 12 eqtri ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) + 𝑆 ) = 𝑊
39 38 oveq1i ⊢ ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) + 𝑆 ) · ( 1 0 ↑ 𝑀 ) ) = ( 𝑊 · ( 1 0 ↑ 𝑀 ) )
40 19 21 18 mulassi ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) · ( 1 0 ↑ 𝑀 ) ) = ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) )
41 14 21 mulcli ⊢ ( 𝐴 · 𝐶 ) ∈ ℂ
42 41 26 32 add32i ⊢ ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + 𝑆 ) = ( ( ( 𝐴 · 𝐶 ) + 𝑆 ) + ( 𝐷 · 𝐵 ) )
43 7 oveq1i ⊢ ( ( 𝐴 · 𝐶 ) + 𝑆 ) = ( 𝑅 + 𝑆 )
44 20 23 8 mulcomli ⊢ ( 𝐷 · 𝐵 ) = 𝑇
45 43 44 oveq12i ⊢ ( ( ( 𝐴 · 𝐶 ) + 𝑆 ) + ( 𝐷 · 𝐵 ) ) = ( ( 𝑅 + 𝑆 ) + 𝑇 )
46 42 45 eqtri ⊢ ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + 𝑆 ) = ( ( 𝑅 + 𝑆 ) + 𝑇 )
47 14 20 21 23 muladdi ⊢ ( ( 𝐴 + 𝐵 ) · ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) )
48 46 9 47 3eqtr2i ⊢ ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + 𝑆 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) )
49 41 26 addcli ⊢ ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) ∈ ℂ
50 14 23 mulcli ⊢ ( 𝐴 · 𝐷 ) ∈ ℂ
51 21 20 mulcli ⊢ ( 𝐶 · 𝐵 ) ∈ ℂ
52 50 51 addcli ⊢ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℂ
53 49 32 52 addcani ⊢ ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + 𝑆 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) ↔ 𝑆 = ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) )
54 48 53 mpbi ⊢ 𝑆 = ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) )
55 54 oveq1i ⊢ ( 𝑆 · ( 1 0 ↑ 𝑀 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( 1 0 ↑ 𝑀 ) )
56 50 51 18 adddiri ⊢ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( 1 0 ↑ 𝑀 ) ) = ( ( ( 𝐴 · 𝐷 ) · ( 1 0 ↑ 𝑀 ) ) + ( ( 𝐶 · 𝐵 ) · ( 1 0 ↑ 𝑀 ) ) )
57 14 23 18 mul32i ⊢ ( ( 𝐴 · 𝐷 ) · ( 1 0 ↑ 𝑀 ) ) = ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 )
58 21 20 18 mul32i ⊢ ( ( 𝐶 · 𝐵 ) · ( 1 0 ↑ 𝑀 ) ) = ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 )
59 57 58 oveq12i ⊢ ( ( ( 𝐴 · 𝐷 ) · ( 1 0 ↑ 𝑀 ) ) + ( ( 𝐶 · 𝐵 ) · ( 1 0 ↑ 𝑀 ) ) ) = ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) )
60 55 56 59 3eqtri ⊢ ( 𝑆 · ( 1 0 ↑ 𝑀 ) ) = ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) )
61 40 60 oveq12i ⊢ ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐶 ) · ( 1 0 ↑ 𝑀 ) ) + ( 𝑆 · ( 1 0 ↑ 𝑀 ) ) ) = ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ) + ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ) )
62 33 39 61 3eqtr3ri ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ) + ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ) ) = ( 𝑊 · ( 1 0 ↑ 𝑀 ) )
63 62 44 oveq12i ⊢ ( ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) ) + ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) · 𝐷 ) + ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) · 𝐵 ) ) ) + ( 𝐷 · 𝐵 ) ) = ( ( 𝑊 · ( 1 0 ↑ 𝑀 ) ) + 𝑇 )
64 24 30 63 3eqtri ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) · ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) + 𝐷 ) ) = ( ( 𝑊 · ( 1 0 ↑ 𝑀 ) ) + 𝑇 )
65 10 11 oveq12i ⊢ ( ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) · ( ( 𝐶 · ( 1 0 ↑ 𝑀 ) ) + 𝐷 ) ) = ( 𝑋 · 𝑌 )
66 64 65 13 3eqtr3i ⊢ ( 𝑋 · 𝑌 ) = 𝑍