Proof of Theorem dpmul
Step | Hyp | Ref
| Expression |
1 | | dpmul.a |
. . . . 5
⊢ 𝐴 ∈
ℕ0 |
2 | | dpmul.b |
. . . . 5
⊢ 𝐵 ∈
ℕ0 |
3 | 1, 2 | deccl 11512 |
. . . 4
⊢ ;𝐴𝐵 ∈ ℕ0 |
4 | | dpmul.c |
. . . 4
⊢ 𝐶 ∈
ℕ0 |
5 | | dpmul.d |
. . . 4
⊢ 𝐷 ∈
ℕ0 |
6 | | eqid 2622 |
. . . 4
⊢ ;𝐶𝐷 = ;𝐶𝐷 |
7 | | dpmul.k |
. . . 4
⊢ 𝐾 ∈
ℕ0 |
8 | | dpmul.2 |
. . . . . 6
⊢ (𝐴 · 𝐷) = 𝑀 |
9 | 1, 5 | nn0mulcli 11331 |
. . . . . 6
⊢ (𝐴 · 𝐷) ∈
ℕ0 |
10 | 8, 9 | eqeltrri 2698 |
. . . . 5
⊢ 𝑀 ∈
ℕ0 |
11 | | dpmul.e |
. . . . 5
⊢ 𝐸 ∈
ℕ0 |
12 | 10, 11 | nn0addcli 11330 |
. . . 4
⊢ (𝑀 + 𝐸) ∈
ℕ0 |
13 | | eqid 2622 |
. . . . . . 7
⊢ ;𝐴𝐵 = ;𝐴𝐵 |
14 | | dpmul.3 |
. . . . . . . 8
⊢ (𝐵 · 𝐶) = 𝐿 |
15 | 2, 4 | nn0mulcli 11331 |
. . . . . . . 8
⊢ (𝐵 · 𝐶) ∈
ℕ0 |
16 | 14, 15 | eqeltrri 2698 |
. . . . . . 7
⊢ 𝐿 ∈
ℕ0 |
17 | | dpmul.1 |
. . . . . . 7
⊢ (𝐴 · 𝐶) = 𝐹 |
18 | 4, 1, 2, 13, 16, 17, 14 | decmul1 11585 |
. . . . . 6
⊢ (;𝐴𝐵 · 𝐶) = ;𝐹𝐿 |
19 | 18 | oveq1i 6660 |
. . . . 5
⊢ ((;𝐴𝐵 · 𝐶) + (𝑀 + 𝐸)) = (;𝐹𝐿 + (𝑀 + 𝐸)) |
20 | | dfdec10 11497 |
. . . . . 6
⊢ ;𝐹𝐿 = ((;10 · 𝐹) + 𝐿) |
21 | 20 | oveq1i 6660 |
. . . . 5
⊢ (;𝐹𝐿 + (𝑀 + 𝐸)) = (((;10 · 𝐹) + 𝐿) + (𝑀 + 𝐸)) |
22 | | 10nn0 11516 |
. . . . . . . . 9
⊢ ;10 ∈
ℕ0 |
23 | 22 | nn0cni 11304 |
. . . . . . . 8
⊢ ;10 ∈ ℂ |
24 | 1, 4 | nn0mulcli 11331 |
. . . . . . . . . 10
⊢ (𝐴 · 𝐶) ∈
ℕ0 |
25 | 17, 24 | eqeltrri 2698 |
. . . . . . . . 9
⊢ 𝐹 ∈
ℕ0 |
26 | 25 | nn0cni 11304 |
. . . . . . . 8
⊢ 𝐹 ∈ ℂ |
27 | 23, 26 | mulcli 10045 |
. . . . . . 7
⊢ (;10 · 𝐹) ∈ ℂ |
28 | 16 | nn0cni 11304 |
. . . . . . 7
⊢ 𝐿 ∈ ℂ |
29 | 12 | nn0cni 11304 |
. . . . . . 7
⊢ (𝑀 + 𝐸) ∈ ℂ |
30 | 27, 28, 29 | addassi 10048 |
. . . . . 6
⊢ (((;10 · 𝐹) + 𝐿) + (𝑀 + 𝐸)) = ((;10 · 𝐹) + (𝐿 + (𝑀 + 𝐸))) |
31 | | dpmul.5 |
. . . . . . . 8
⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽 |
32 | 10 | nn0cni 11304 |
. . . . . . . . 9
⊢ 𝑀 ∈ ℂ |
33 | 11 | nn0cni 11304 |
. . . . . . . . 9
⊢ 𝐸 ∈ ℂ |
34 | 28, 32, 33 | addassi 10048 |
. . . . . . . 8
⊢ ((𝐿 + 𝑀) + 𝐸) = (𝐿 + (𝑀 + 𝐸)) |
35 | | dfdec10 11497 |
. . . . . . . 8
⊢ ;𝐺𝐽 = ((;10 · 𝐺) + 𝐽) |
36 | 31, 34, 35 | 3eqtr3ri 2653 |
. . . . . . 7
⊢ ((;10 · 𝐺) + 𝐽) = (𝐿 + (𝑀 + 𝐸)) |
37 | 36 | oveq2i 6661 |
. . . . . 6
⊢ ((;10 · 𝐹) + ((;10 · 𝐺) + 𝐽)) = ((;10 · 𝐹) + (𝐿 + (𝑀 + 𝐸))) |
38 | | dfdec10 11497 |
. . . . . . 7
⊢ ;𝐼𝐽 = ((;10 · 𝐼) + 𝐽) |
39 | | dpmul.g |
. . . . . . . . . . 11
⊢ 𝐺 ∈
ℕ0 |
40 | 39 | nn0cni 11304 |
. . . . . . . . . 10
⊢ 𝐺 ∈ ℂ |
41 | 23, 26, 40 | adddii 10050 |
. . . . . . . . 9
⊢ (;10 · (𝐹 + 𝐺)) = ((;10 · 𝐹) + (;10 · 𝐺)) |
42 | | dpmul.6 |
. . . . . . . . . 10
⊢ (𝐹 + 𝐺) = 𝐼 |
43 | 42 | oveq2i 6661 |
. . . . . . . . 9
⊢ (;10 · (𝐹 + 𝐺)) = (;10 · 𝐼) |
44 | 41, 43 | eqtr3i 2646 |
. . . . . . . 8
⊢ ((;10 · 𝐹) + (;10 · 𝐺)) = (;10 · 𝐼) |
45 | 44 | oveq1i 6660 |
. . . . . . 7
⊢ (((;10 · 𝐹) + (;10 · 𝐺)) + 𝐽) = ((;10 · 𝐼) + 𝐽) |
46 | 23, 40 | mulcli 10045 |
. . . . . . . 8
⊢ (;10 · 𝐺) ∈ ℂ |
47 | | dpmul.j |
. . . . . . . . 9
⊢ 𝐽 ∈
ℕ0 |
48 | 47 | nn0cni 11304 |
. . . . . . . 8
⊢ 𝐽 ∈ ℂ |
49 | 27, 46, 48 | addassi 10048 |
. . . . . . 7
⊢ (((;10 · 𝐹) + (;10 · 𝐺)) + 𝐽) = ((;10 · 𝐹) + ((;10 · 𝐺) + 𝐽)) |
50 | 38, 45, 49 | 3eqtr2ri 2651 |
. . . . . 6
⊢ ((;10 · 𝐹) + ((;10 · 𝐺) + 𝐽)) = ;𝐼𝐽 |
51 | 30, 37, 50 | 3eqtr2i 2650 |
. . . . 5
⊢ (((;10 · 𝐹) + 𝐿) + (𝑀 + 𝐸)) = ;𝐼𝐽 |
52 | 19, 21, 51 | 3eqtri 2648 |
. . . 4
⊢ ((;𝐴𝐵 · 𝐶) + (𝑀 + 𝐸)) = ;𝐼𝐽 |
53 | 8 | oveq1i 6660 |
. . . . 5
⊢ ((𝐴 · 𝐷) + 𝐸) = (𝑀 + 𝐸) |
54 | | dpmul.4 |
. . . . 5
⊢ (𝐵 · 𝐷) = ;𝐸𝐾 |
55 | 5, 1, 2, 13, 7, 11, 53, 54 | decmul1c 11587 |
. . . 4
⊢ (;𝐴𝐵 · 𝐷) = ;(𝑀 + 𝐸)𝐾 |
56 | 3, 4, 5, 6, 7, 12,
52, 55 | decmul2c 11589 |
. . 3
⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐼𝐽𝐾 |
57 | 2 | nn0rei 11303 |
. . . . . . 7
⊢ 𝐵 ∈ ℝ |
58 | | dpcl 29598 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℝ)
→ (𝐴.𝐵) ∈ ℝ) |
59 | 1, 57, 58 | mp2an 708 |
. . . . . 6
⊢ (𝐴.𝐵) ∈ ℝ |
60 | 59 | recni 10052 |
. . . . 5
⊢ (𝐴.𝐵) ∈ ℂ |
61 | 5 | nn0rei 11303 |
. . . . . . 7
⊢ 𝐷 ∈ ℝ |
62 | | dpcl 29598 |
. . . . . . 7
⊢ ((𝐶 ∈ ℕ0
∧ 𝐷 ∈ ℝ)
→ (𝐶.𝐷) ∈ ℝ) |
63 | 4, 61, 62 | mp2an 708 |
. . . . . 6
⊢ (𝐶.𝐷) ∈ ℝ |
64 | 63 | recni 10052 |
. . . . 5
⊢ (𝐶.𝐷) ∈ ℂ |
65 | 60, 64, 23, 23 | mul4i 10233 |
. . . 4
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · (;10 · ;10)) = (((𝐴.𝐵) · ;10) · ((𝐶.𝐷) · ;10)) |
66 | 22 | dec0u 11520 |
. . . . 5
⊢ (;10 · ;10) = ;;100 |
67 | 66 | oveq2i 6661 |
. . . 4
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · (;10 · ;10)) = (((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) |
68 | 1, 57 | dpmul10 29603 |
. . . . 5
⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵 |
69 | 4, 61 | dpmul10 29603 |
. . . . 5
⊢ ((𝐶.𝐷) · ;10) = ;𝐶𝐷 |
70 | 68, 69 | oveq12i 6662 |
. . . 4
⊢ (((𝐴.𝐵) · ;10) · ((𝐶.𝐷) · ;10)) = (;𝐴𝐵 · ;𝐶𝐷) |
71 | 65, 67, 70 | 3eqtr3i 2652 |
. . 3
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
(;𝐴𝐵 · ;𝐶𝐷) |
72 | 25, 39 | nn0addcli 11330 |
. . . . 5
⊢ (𝐹 + 𝐺) ∈
ℕ0 |
73 | 42, 72 | eqeltrri 2698 |
. . . 4
⊢ 𝐼 ∈
ℕ0 |
74 | 7 | nn0rei 11303 |
. . . 4
⊢ 𝐾 ∈ ℝ |
75 | 73, 47, 74 | dpmul100 29605 |
. . 3
⊢ ((𝐼._𝐽𝐾) · ;;100) =
;;𝐼𝐽𝐾 |
76 | 56, 71, 75 | 3eqtr4i 2654 |
. 2
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
((𝐼._𝐽𝐾) · ;;100) |
77 | 60, 64 | mulcli 10045 |
. . 3
⊢ ((𝐴.𝐵) · (𝐶.𝐷)) ∈ ℂ |
78 | 47 | nn0rei 11303 |
. . . . . 6
⊢ 𝐽 ∈ ℝ |
79 | | dp2cl 29587 |
. . . . . 6
⊢ ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ) → _𝐽𝐾 ∈ ℝ) |
80 | 78, 74, 79 | mp2an 708 |
. . . . 5
⊢ _𝐽𝐾 ∈ ℝ |
81 | | dpcl 29598 |
. . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ _𝐽𝐾 ∈ ℝ) → (𝐼._𝐽𝐾) ∈ ℝ) |
82 | 73, 80, 81 | mp2an 708 |
. . . 4
⊢ (𝐼._𝐽𝐾) ∈ ℝ |
83 | 82 | recni 10052 |
. . 3
⊢ (𝐼._𝐽𝐾) ∈ ℂ |
84 | | 10nn 11514 |
. . . . . 6
⊢ ;10 ∈ ℕ |
85 | 84 | decnncl2 11525 |
. . . . 5
⊢ ;;100 ∈ ℕ |
86 | 85 | nncni 11030 |
. . . 4
⊢ ;;100 ∈ ℂ |
87 | 85 | nnne0i 11055 |
. . . 4
⊢ ;;100 ≠ 0 |
88 | 86, 87 | pm3.2i 471 |
. . 3
⊢ (;;100 ∈ ℂ ∧ ;;100
≠ 0) |
89 | | mulcan2 10665 |
. . 3
⊢ ((((𝐴.𝐵) · (𝐶.𝐷)) ∈ ℂ ∧ (𝐼._𝐽𝐾) ∈ ℂ ∧ (;;100
∈ ℂ ∧ ;;100 ≠ 0)) → ((((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
((𝐼._𝐽𝐾) · ;;100)
↔ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾))) |
90 | 77, 83, 88, 89 | mp3an 1424 |
. 2
⊢ ((((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
((𝐼._𝐽𝐾) · ;;100)
↔ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾)) |
91 | 76, 90 | mpbi 220 |
1
⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾) |