Proof of Theorem dpmul
Step | Hyp | Ref
| Expression |
1 | | dpmul.a |
. . . . 5
⊢ 𝐴 ∈
ℕ0 |
2 | | dpmul.b |
. . . . 5
⊢ 𝐵 ∈
ℕ0 |
3 | 1, 2 | deccl 12397 |
. . . 4
⊢ ;𝐴𝐵 ∈ ℕ0 |
4 | | dpmul.c |
. . . 4
⊢ 𝐶 ∈
ℕ0 |
5 | | dpmul.d |
. . . 4
⊢ 𝐷 ∈
ℕ0 |
6 | | eqid 2737 |
. . . 4
⊢ ;𝐶𝐷 = ;𝐶𝐷 |
7 | | dpmul.k |
. . . 4
⊢ 𝐾 ∈
ℕ0 |
8 | | dpmul.2 |
. . . . . 6
⊢ (𝐴 · 𝐷) = 𝑀 |
9 | 1, 5 | nn0mulcli 12217 |
. . . . . 6
⊢ (𝐴 · 𝐷) ∈
ℕ0 |
10 | 8, 9 | eqeltrri 2834 |
. . . . 5
⊢ 𝑀 ∈
ℕ0 |
11 | | dpmul.e |
. . . . 5
⊢ 𝐸 ∈
ℕ0 |
12 | 10, 11 | nn0addcli 12216 |
. . . 4
⊢ (𝑀 + 𝐸) ∈
ℕ0 |
13 | | eqid 2737 |
. . . . . . 7
⊢ ;𝐴𝐵 = ;𝐴𝐵 |
14 | | dpmul.1 |
. . . . . . 7
⊢ (𝐴 · 𝐶) = 𝐹 |
15 | | dpmul.3 |
. . . . . . 7
⊢ (𝐵 · 𝐶) = 𝐿 |
16 | 4, 1, 2, 13, 14, 15 | decmul1 12446 |
. . . . . 6
⊢ (;𝐴𝐵 · 𝐶) = ;𝐹𝐿 |
17 | 16 | oveq1i 7270 |
. . . . 5
⊢ ((;𝐴𝐵 · 𝐶) + (𝑀 + 𝐸)) = (;𝐹𝐿 + (𝑀 + 𝐸)) |
18 | | dfdec10 12385 |
. . . . . 6
⊢ ;𝐹𝐿 = ((;10 · 𝐹) + 𝐿) |
19 | 18 | oveq1i 7270 |
. . . . 5
⊢ (;𝐹𝐿 + (𝑀 + 𝐸)) = (((;10 · 𝐹) + 𝐿) + (𝑀 + 𝐸)) |
20 | | 10nn0 12400 |
. . . . . . . . 9
⊢ ;10 ∈
ℕ0 |
21 | 20 | nn0cni 12191 |
. . . . . . . 8
⊢ ;10 ∈ ℂ |
22 | 1, 4 | nn0mulcli 12217 |
. . . . . . . . . 10
⊢ (𝐴 · 𝐶) ∈
ℕ0 |
23 | 14, 22 | eqeltrri 2834 |
. . . . . . . . 9
⊢ 𝐹 ∈
ℕ0 |
24 | 23 | nn0cni 12191 |
. . . . . . . 8
⊢ 𝐹 ∈ ℂ |
25 | 21, 24 | mulcli 10929 |
. . . . . . 7
⊢ (;10 · 𝐹) ∈ ℂ |
26 | 2, 4 | nn0mulcli 12217 |
. . . . . . . . 9
⊢ (𝐵 · 𝐶) ∈
ℕ0 |
27 | 15, 26 | eqeltrri 2834 |
. . . . . . . 8
⊢ 𝐿 ∈
ℕ0 |
28 | 27 | nn0cni 12191 |
. . . . . . 7
⊢ 𝐿 ∈ ℂ |
29 | 12 | nn0cni 12191 |
. . . . . . 7
⊢ (𝑀 + 𝐸) ∈ ℂ |
30 | 25, 28, 29 | addassi 10932 |
. . . . . 6
⊢ (((;10 · 𝐹) + 𝐿) + (𝑀 + 𝐸)) = ((;10 · 𝐹) + (𝐿 + (𝑀 + 𝐸))) |
31 | | dpmul.5 |
. . . . . . . 8
⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽 |
32 | 10 | nn0cni 12191 |
. . . . . . . . 9
⊢ 𝑀 ∈ ℂ |
33 | 11 | nn0cni 12191 |
. . . . . . . . 9
⊢ 𝐸 ∈ ℂ |
34 | 28, 32, 33 | addassi 10932 |
. . . . . . . 8
⊢ ((𝐿 + 𝑀) + 𝐸) = (𝐿 + (𝑀 + 𝐸)) |
35 | | dfdec10 12385 |
. . . . . . . 8
⊢ ;𝐺𝐽 = ((;10 · 𝐺) + 𝐽) |
36 | 31, 34, 35 | 3eqtr3ri 2774 |
. . . . . . 7
⊢ ((;10 · 𝐺) + 𝐽) = (𝐿 + (𝑀 + 𝐸)) |
37 | 36 | oveq2i 7271 |
. . . . . 6
⊢ ((;10 · 𝐹) + ((;10 · 𝐺) + 𝐽)) = ((;10 · 𝐹) + (𝐿 + (𝑀 + 𝐸))) |
38 | | dfdec10 12385 |
. . . . . . 7
⊢ ;𝐼𝐽 = ((;10 · 𝐼) + 𝐽) |
39 | | dpmul.g |
. . . . . . . . . . 11
⊢ 𝐺 ∈
ℕ0 |
40 | 39 | nn0cni 12191 |
. . . . . . . . . 10
⊢ 𝐺 ∈ ℂ |
41 | 21, 24, 40 | adddii 10934 |
. . . . . . . . 9
⊢ (;10 · (𝐹 + 𝐺)) = ((;10 · 𝐹) + (;10 · 𝐺)) |
42 | | dpmul.6 |
. . . . . . . . . 10
⊢ (𝐹 + 𝐺) = 𝐼 |
43 | 42 | oveq2i 7271 |
. . . . . . . . 9
⊢ (;10 · (𝐹 + 𝐺)) = (;10 · 𝐼) |
44 | 41, 43 | eqtr3i 2767 |
. . . . . . . 8
⊢ ((;10 · 𝐹) + (;10 · 𝐺)) = (;10 · 𝐼) |
45 | 44 | oveq1i 7270 |
. . . . . . 7
⊢ (((;10 · 𝐹) + (;10 · 𝐺)) + 𝐽) = ((;10 · 𝐼) + 𝐽) |
46 | 21, 40 | mulcli 10929 |
. . . . . . . 8
⊢ (;10 · 𝐺) ∈ ℂ |
47 | | dpmul.j |
. . . . . . . . 9
⊢ 𝐽 ∈
ℕ0 |
48 | 47 | nn0cni 12191 |
. . . . . . . 8
⊢ 𝐽 ∈ ℂ |
49 | 25, 46, 48 | addassi 10932 |
. . . . . . 7
⊢ (((;10 · 𝐹) + (;10 · 𝐺)) + 𝐽) = ((;10 · 𝐹) + ((;10 · 𝐺) + 𝐽)) |
50 | 38, 45, 49 | 3eqtr2ri 2772 |
. . . . . 6
⊢ ((;10 · 𝐹) + ((;10 · 𝐺) + 𝐽)) = ;𝐼𝐽 |
51 | 30, 37, 50 | 3eqtr2i 2771 |
. . . . 5
⊢ (((;10 · 𝐹) + 𝐿) + (𝑀 + 𝐸)) = ;𝐼𝐽 |
52 | 17, 19, 51 | 3eqtri 2769 |
. . . 4
⊢ ((;𝐴𝐵 · 𝐶) + (𝑀 + 𝐸)) = ;𝐼𝐽 |
53 | 8 | oveq1i 7270 |
. . . . 5
⊢ ((𝐴 · 𝐷) + 𝐸) = (𝑀 + 𝐸) |
54 | | dpmul.4 |
. . . . 5
⊢ (𝐵 · 𝐷) = ;𝐸𝐾 |
55 | 5, 1, 2, 13, 7, 11, 53, 54 | decmul1c 12447 |
. . . 4
⊢ (;𝐴𝐵 · 𝐷) = ;(𝑀 + 𝐸)𝐾 |
56 | 3, 4, 5, 6, 7, 12,
52, 55 | decmul2c 12448 |
. . 3
⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐼𝐽𝐾 |
57 | 2 | nn0rei 12190 |
. . . . . . 7
⊢ 𝐵 ∈ ℝ |
58 | | dpcl 31107 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℝ)
→ (𝐴.𝐵) ∈ ℝ) |
59 | 1, 57, 58 | mp2an 688 |
. . . . . 6
⊢ (𝐴.𝐵) ∈ ℝ |
60 | 59 | recni 10936 |
. . . . 5
⊢ (𝐴.𝐵) ∈ ℂ |
61 | 5 | nn0rei 12190 |
. . . . . . 7
⊢ 𝐷 ∈ ℝ |
62 | | dpcl 31107 |
. . . . . . 7
⊢ ((𝐶 ∈ ℕ0
∧ 𝐷 ∈ ℝ)
→ (𝐶.𝐷) ∈ ℝ) |
63 | 4, 61, 62 | mp2an 688 |
. . . . . 6
⊢ (𝐶.𝐷) ∈ ℝ |
64 | 63 | recni 10936 |
. . . . 5
⊢ (𝐶.𝐷) ∈ ℂ |
65 | 60, 64, 21, 21 | mul4i 11118 |
. . . 4
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · (;10 · ;10)) = (((𝐴.𝐵) · ;10) · ((𝐶.𝐷) · ;10)) |
66 | 20 | dec0u 12403 |
. . . . 5
⊢ (;10 · ;10) = ;;100 |
67 | 66 | oveq2i 7271 |
. . . 4
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · (;10 · ;10)) = (((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) |
68 | 1, 57 | dpmul10 31111 |
. . . . 5
⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵 |
69 | 4, 61 | dpmul10 31111 |
. . . . 5
⊢ ((𝐶.𝐷) · ;10) = ;𝐶𝐷 |
70 | 68, 69 | oveq12i 7272 |
. . . 4
⊢ (((𝐴.𝐵) · ;10) · ((𝐶.𝐷) · ;10)) = (;𝐴𝐵 · ;𝐶𝐷) |
71 | 65, 67, 70 | 3eqtr3i 2773 |
. . 3
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
(;𝐴𝐵 · ;𝐶𝐷) |
72 | 23, 39 | nn0addcli 12216 |
. . . . 5
⊢ (𝐹 + 𝐺) ∈
ℕ0 |
73 | 42, 72 | eqeltrri 2834 |
. . . 4
⊢ 𝐼 ∈
ℕ0 |
74 | 7 | nn0rei 12190 |
. . . 4
⊢ 𝐾 ∈ ℝ |
75 | 73, 47, 74 | dpmul100 31113 |
. . 3
⊢ ((𝐼._𝐽𝐾) · ;;100) =
;;𝐼𝐽𝐾 |
76 | 56, 71, 75 | 3eqtr4i 2775 |
. 2
⊢ (((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
((𝐼._𝐽𝐾) · ;;100) |
77 | 60, 64 | mulcli 10929 |
. . 3
⊢ ((𝐴.𝐵) · (𝐶.𝐷)) ∈ ℂ |
78 | 47 | nn0rei 12190 |
. . . . . 6
⊢ 𝐽 ∈ ℝ |
79 | | dp2cl 31096 |
. . . . . 6
⊢ ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ) → _𝐽𝐾 ∈ ℝ) |
80 | 78, 74, 79 | mp2an 688 |
. . . . 5
⊢ _𝐽𝐾 ∈ ℝ |
81 | | dpcl 31107 |
. . . . 5
⊢ ((𝐼 ∈ ℕ0
∧ _𝐽𝐾 ∈ ℝ) → (𝐼._𝐽𝐾) ∈ ℝ) |
82 | 73, 80, 81 | mp2an 688 |
. . . 4
⊢ (𝐼._𝐽𝐾) ∈ ℝ |
83 | 82 | recni 10936 |
. . 3
⊢ (𝐼._𝐽𝐾) ∈ ℂ |
84 | | 10nn 12398 |
. . . . . 6
⊢ ;10 ∈ ℕ |
85 | 84 | decnncl2 12406 |
. . . . 5
⊢ ;;100 ∈ ℕ |
86 | 85 | nncni 11929 |
. . . 4
⊢ ;;100 ∈ ℂ |
87 | 85 | nnne0i 11959 |
. . . 4
⊢ ;;100 ≠ 0 |
88 | 86, 87 | pm3.2i 470 |
. . 3
⊢ (;;100 ∈ ℂ ∧ ;;100
≠ 0) |
89 | | mulcan2 11559 |
. . 3
⊢ ((((𝐴.𝐵) · (𝐶.𝐷)) ∈ ℂ ∧ (𝐼._𝐽𝐾) ∈ ℂ ∧ (;;100
∈ ℂ ∧ ;;100 ≠ 0)) → ((((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
((𝐼._𝐽𝐾) · ;;100)
↔ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾))) |
90 | 77, 83, 88, 89 | mp3an 1459 |
. 2
⊢ ((((𝐴.𝐵) · (𝐶.𝐷)) · ;;100) =
((𝐼._𝐽𝐾) · ;;100)
↔ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾)) |
91 | 76, 90 | mpbi 229 |
1
⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾) |