Proof of Theorem 3dvds2dec
Step | Hyp | Ref
| Expression |
1 | | 3dvdsdec.a |
. . . . 5
⊢ 𝐴 ∈
ℕ0 |
2 | | 3dvdsdec.b |
. . . . 5
⊢ 𝐵 ∈
ℕ0 |
3 | 1, 2 | 3dec 10592 |
. . . 4
⊢ ;;𝐴𝐵𝐶 = ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) |
4 | | sq10e99m1 10591 |
. . . . . . . 8
⊢ (;10↑2) = (;99 + 1) |
5 | 4 | oveq1i 5835 |
. . . . . . 7
⊢ ((;10↑2) · 𝐴) = ((;99 + 1) · 𝐴) |
6 | | 9nn0 9115 |
. . . . . . . . . 10
⊢ 9 ∈
ℕ0 |
7 | 6, 6 | deccl 9310 |
. . . . . . . . 9
⊢ ;99 ∈
ℕ0 |
8 | 7 | nn0cni 9103 |
. . . . . . . 8
⊢ ;99 ∈ ℂ |
9 | | ax-1cn 7826 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
10 | 1 | nn0cni 9103 |
. . . . . . . 8
⊢ 𝐴 ∈ ℂ |
11 | 8, 9, 10 | adddiri 7890 |
. . . . . . 7
⊢ ((;99 + 1) · 𝐴) = ((;99 · 𝐴) + (1 · 𝐴)) |
12 | 10 | mulid2i 7882 |
. . . . . . . 8
⊢ (1
· 𝐴) = 𝐴 |
13 | 12 | oveq2i 5836 |
. . . . . . 7
⊢ ((;99 · 𝐴) + (1 · 𝐴)) = ((;99 · 𝐴) + 𝐴) |
14 | 5, 11, 13 | 3eqtri 2182 |
. . . . . 6
⊢ ((;10↑2) · 𝐴) = ((;99 · 𝐴) + 𝐴) |
15 | | 9p1e10 9298 |
. . . . . . . . 9
⊢ (9 + 1) =
;10 |
16 | 15 | eqcomi 2161 |
. . . . . . . 8
⊢ ;10 = (9 + 1) |
17 | 16 | oveq1i 5835 |
. . . . . . 7
⊢ (;10 · 𝐵) = ((9 + 1) · 𝐵) |
18 | | 9cn 8922 |
. . . . . . . 8
⊢ 9 ∈
ℂ |
19 | 2 | nn0cni 9103 |
. . . . . . . 8
⊢ 𝐵 ∈ ℂ |
20 | 18, 9, 19 | adddiri 7890 |
. . . . . . 7
⊢ ((9 + 1)
· 𝐵) = ((9 ·
𝐵) + (1 · 𝐵)) |
21 | 19 | mulid2i 7882 |
. . . . . . . 8
⊢ (1
· 𝐵) = 𝐵 |
22 | 21 | oveq2i 5836 |
. . . . . . 7
⊢ ((9
· 𝐵) + (1 ·
𝐵)) = ((9 · 𝐵) + 𝐵) |
23 | 17, 20, 22 | 3eqtri 2182 |
. . . . . 6
⊢ (;10 · 𝐵) = ((9 · 𝐵) + 𝐵) |
24 | 14, 23 | oveq12i 5837 |
. . . . 5
⊢ (((;10↑2) · 𝐴) + (;10 · 𝐵)) = (((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) |
25 | 24 | oveq1i 5835 |
. . . 4
⊢ ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) = ((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) |
26 | 8, 10 | mulcli 7884 |
. . . . . 6
⊢ (;99 · 𝐴) ∈ ℂ |
27 | 18, 19 | mulcli 7884 |
. . . . . 6
⊢ (9
· 𝐵) ∈
ℂ |
28 | | add4 8037 |
. . . . . . 7
⊢ ((((;99 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) ∧ ((9 · 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ)) →
(((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) = (((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵))) |
29 | 28 | oveq1d 5840 |
. . . . . 6
⊢ ((((;99 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) ∧ ((9 · 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ)) →
((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) = ((((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵)) + 𝐶)) |
30 | 26, 10, 27, 19, 29 | mp4an 424 |
. . . . 5
⊢ ((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) = ((((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵)) + 𝐶) |
31 | 26, 27 | addcli 7883 |
. . . . . 6
⊢ ((;99 · 𝐴) + (9 · 𝐵)) ∈ ℂ |
32 | 10, 19 | addcli 7883 |
. . . . . 6
⊢ (𝐴 + 𝐵) ∈ ℂ |
33 | | 3dvds2dec.c |
. . . . . . 7
⊢ 𝐶 ∈
ℕ0 |
34 | 33 | nn0cni 9103 |
. . . . . 6
⊢ 𝐶 ∈ ℂ |
35 | 31, 32, 34 | addassi 7887 |
. . . . 5
⊢ ((((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵)) + 𝐶) = (((;99 · 𝐴) + (9 · 𝐵)) + ((𝐴 + 𝐵) + 𝐶)) |
36 | | 9t11e99 9425 |
. . . . . . . . . . 11
⊢ (9
· ;11) = ;99 |
37 | 36 | eqcomi 2161 |
. . . . . . . . . 10
⊢ ;99 = (9 · ;11) |
38 | 37 | oveq1i 5835 |
. . . . . . . . 9
⊢ (;99 · 𝐴) = ((9 · ;11) · 𝐴) |
39 | | 1nn0 9107 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
40 | 39, 39 | deccl 9310 |
. . . . . . . . . . 11
⊢ ;11 ∈
ℕ0 |
41 | 40 | nn0cni 9103 |
. . . . . . . . . 10
⊢ ;11 ∈ ℂ |
42 | 18, 41, 10 | mulassi 7888 |
. . . . . . . . 9
⊢ ((9
· ;11) · 𝐴) = (9 · (;11 · 𝐴)) |
43 | 38, 42 | eqtri 2178 |
. . . . . . . 8
⊢ (;99 · 𝐴) = (9 · (;11 · 𝐴)) |
44 | 43 | oveq1i 5835 |
. . . . . . 7
⊢ ((;99 · 𝐴) + (9 · 𝐵)) = ((9 · (;11 · 𝐴)) + (9 · 𝐵)) |
45 | 41, 10 | mulcli 7884 |
. . . . . . . . 9
⊢ (;11 · 𝐴) ∈ ℂ |
46 | 18, 45, 19 | adddii 7889 |
. . . . . . . 8
⊢ (9
· ((;11 · 𝐴) + 𝐵)) = ((9 · (;11 · 𝐴)) + (9 · 𝐵)) |
47 | 46 | eqcomi 2161 |
. . . . . . 7
⊢ ((9
· (;11 · 𝐴)) + (9 · 𝐵)) = (9 · ((;11 · 𝐴) + 𝐵)) |
48 | | 3t3e9 8991 |
. . . . . . . . . 10
⊢ (3
· 3) = 9 |
49 | 48 | eqcomi 2161 |
. . . . . . . . 9
⊢ 9 = (3
· 3) |
50 | 49 | oveq1i 5835 |
. . . . . . . 8
⊢ (9
· ((;11 · 𝐴) + 𝐵)) = ((3 · 3) · ((;11 · 𝐴) + 𝐵)) |
51 | | 3cn 8909 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
52 | 45, 19 | addcli 7883 |
. . . . . . . . 9
⊢ ((;11 · 𝐴) + 𝐵) ∈ ℂ |
53 | 51, 51, 52 | mulassi 7888 |
. . . . . . . 8
⊢ ((3
· 3) · ((;11
· 𝐴) + 𝐵)) = (3 · (3 ·
((;11 · 𝐴) + 𝐵))) |
54 | 50, 53 | eqtri 2178 |
. . . . . . 7
⊢ (9
· ((;11 · 𝐴) + 𝐵)) = (3 · (3 · ((;11 · 𝐴) + 𝐵))) |
55 | 44, 47, 54 | 3eqtri 2182 |
. . . . . 6
⊢ ((;99 · 𝐴) + (9 · 𝐵)) = (3 · (3 · ((;11 · 𝐴) + 𝐵))) |
56 | 55 | oveq1i 5835 |
. . . . 5
⊢ (((;99 · 𝐴) + (9 · 𝐵)) + ((𝐴 + 𝐵) + 𝐶)) = ((3 · (3 · ((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)) |
57 | 30, 35, 56 | 3eqtri 2182 |
. . . 4
⊢ ((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) = ((3 · (3 · ((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)) |
58 | 3, 25, 57 | 3eqtri 2182 |
. . 3
⊢ ;;𝐴𝐵𝐶 = ((3 · (3 · ((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)) |
59 | 58 | breq2i 3974 |
. 2
⊢ (3
∥ ;;𝐴𝐵𝐶 ↔ 3 ∥ ((3 · (3 ·
((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶))) |
60 | | 3z 9197 |
. . 3
⊢ 3 ∈
ℤ |
61 | 1 | nn0zi 9190 |
. . . . 5
⊢ 𝐴 ∈ ℤ |
62 | 2 | nn0zi 9190 |
. . . . 5
⊢ 𝐵 ∈ ℤ |
63 | | zaddcl 9208 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℤ) |
64 | 61, 62, 63 | mp2an 423 |
. . . 4
⊢ (𝐴 + 𝐵) ∈ ℤ |
65 | 33 | nn0zi 9190 |
. . . 4
⊢ 𝐶 ∈ ℤ |
66 | | zaddcl 9208 |
. . . 4
⊢ (((𝐴 + 𝐵) ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 + 𝐵) + 𝐶) ∈ ℤ) |
67 | 64, 65, 66 | mp2an 423 |
. . 3
⊢ ((𝐴 + 𝐵) + 𝐶) ∈ ℤ |
68 | 40 | nn0zi 9190 |
. . . . . . . 8
⊢ ;11 ∈ ℤ |
69 | | zmulcl 9221 |
. . . . . . . 8
⊢ ((;11 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (;11 · 𝐴) ∈ ℤ) |
70 | 68, 61, 69 | mp2an 423 |
. . . . . . 7
⊢ (;11 · 𝐴) ∈ ℤ |
71 | | zaddcl 9208 |
. . . . . . 7
⊢ (((;11 · 𝐴) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((;11 · 𝐴) + 𝐵) ∈ ℤ) |
72 | 70, 62, 71 | mp2an 423 |
. . . . . 6
⊢ ((;11 · 𝐴) + 𝐵) ∈ ℤ |
73 | | zmulcl 9221 |
. . . . . 6
⊢ ((3
∈ ℤ ∧ ((;11
· 𝐴) + 𝐵) ∈ ℤ) → (3
· ((;11 · 𝐴) + 𝐵)) ∈ ℤ) |
74 | 60, 72, 73 | mp2an 423 |
. . . . 5
⊢ (3
· ((;11 · 𝐴) + 𝐵)) ∈ ℤ |
75 | | zmulcl 9221 |
. . . . 5
⊢ ((3
∈ ℤ ∧ (3 · ((;11 · 𝐴) + 𝐵)) ∈ ℤ) → (3 · (3
· ((;11 · 𝐴) + 𝐵))) ∈ ℤ) |
76 | 60, 74, 75 | mp2an 423 |
. . . 4
⊢ (3
· (3 · ((;11
· 𝐴) + 𝐵))) ∈
ℤ |
77 | | dvdsmul1 11713 |
. . . . 5
⊢ ((3
∈ ℤ ∧ (3 · ((;11 · 𝐴) + 𝐵)) ∈ ℤ) → 3 ∥ (3
· (3 · ((;11
· 𝐴) + 𝐵)))) |
78 | 60, 74, 77 | mp2an 423 |
. . . 4
⊢ 3 ∥
(3 · (3 · ((;11
· 𝐴) + 𝐵))) |
79 | 76, 78 | pm3.2i 270 |
. . 3
⊢ ((3
· (3 · ((;11
· 𝐴) + 𝐵))) ∈ ℤ ∧ 3
∥ (3 · (3 · ((;11 · 𝐴) + 𝐵)))) |
80 | | dvdsadd2b 11738 |
. . 3
⊢ ((3
∈ ℤ ∧ ((𝐴 +
𝐵) + 𝐶) ∈ ℤ ∧ ((3 · (3
· ((;11 · 𝐴) + 𝐵))) ∈ ℤ ∧ 3 ∥ (3
· (3 · ((;11
· 𝐴) + 𝐵))))) → (3 ∥ ((𝐴 + 𝐵) + 𝐶) ↔ 3 ∥ ((3 · (3 ·
((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)))) |
81 | 60, 67, 79, 80 | mp3an 1319 |
. 2
⊢ (3
∥ ((𝐴 + 𝐵) + 𝐶) ↔ 3 ∥ ((3 · (3 ·
((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶))) |
82 | 59, 81 | bitr4i 186 |
1
⊢ (3
∥ ;;𝐴𝐵𝐶 ↔ 3 ∥ ((𝐴 + 𝐵) + 𝐶)) |