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