Proof of Theorem 3dvds2dec
| Step | Hyp | Ref
| Expression |
| 1 | | 3dvdsdec.a |
. . . . 5
⊢ 𝐴 ∈
ℕ0 |
| 2 | | 3dvdsdec.b |
. . . . 5
⊢ 𝐵 ∈
ℕ0 |
| 3 | 1, 2 | 3dec 14305 |
. . . 4
⊢ ;;𝐴𝐵𝐶 = ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) |
| 4 | | sq10e99m1 14304 |
. . . . . . . 8
⊢ (;10↑2) = (;99 + 1) |
| 5 | 4 | oveq1i 7441 |
. . . . . . 7
⊢ ((;10↑2) · 𝐴) = ((;99 + 1) · 𝐴) |
| 6 | | 9nn0 12550 |
. . . . . . . . . 10
⊢ 9 ∈
ℕ0 |
| 7 | 6, 6 | deccl 12748 |
. . . . . . . . 9
⊢ ;99 ∈
ℕ0 |
| 8 | 7 | nn0cni 12538 |
. . . . . . . 8
⊢ ;99 ∈ ℂ |
| 9 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 10 | 1 | nn0cni 12538 |
. . . . . . . 8
⊢ 𝐴 ∈ ℂ |
| 11 | 8, 9, 10 | adddiri 11274 |
. . . . . . 7
⊢ ((;99 + 1) · 𝐴) = ((;99 · 𝐴) + (1 · 𝐴)) |
| 12 | 10 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 𝐴) = 𝐴 |
| 13 | 12 | oveq2i 7442 |
. . . . . . 7
⊢ ((;99 · 𝐴) + (1 · 𝐴)) = ((;99 · 𝐴) + 𝐴) |
| 14 | 5, 11, 13 | 3eqtri 2769 |
. . . . . 6
⊢ ((;10↑2) · 𝐴) = ((;99 · 𝐴) + 𝐴) |
| 15 | | 9p1e10 12735 |
. . . . . . . . 9
⊢ (9 + 1) =
;10 |
| 16 | 15 | eqcomi 2746 |
. . . . . . . 8
⊢ ;10 = (9 + 1) |
| 17 | 16 | oveq1i 7441 |
. . . . . . 7
⊢ (;10 · 𝐵) = ((9 + 1) · 𝐵) |
| 18 | | 9cn 12366 |
. . . . . . . 8
⊢ 9 ∈
ℂ |
| 19 | 2 | nn0cni 12538 |
. . . . . . . 8
⊢ 𝐵 ∈ ℂ |
| 20 | 18, 9, 19 | adddiri 11274 |
. . . . . . 7
⊢ ((9 + 1)
· 𝐵) = ((9 ·
𝐵) + (1 · 𝐵)) |
| 21 | 19 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 𝐵) = 𝐵 |
| 22 | 21 | oveq2i 7442 |
. . . . . . 7
⊢ ((9
· 𝐵) + (1 ·
𝐵)) = ((9 · 𝐵) + 𝐵) |
| 23 | 17, 20, 22 | 3eqtri 2769 |
. . . . . 6
⊢ (;10 · 𝐵) = ((9 · 𝐵) + 𝐵) |
| 24 | 14, 23 | oveq12i 7443 |
. . . . 5
⊢ (((;10↑2) · 𝐴) + (;10 · 𝐵)) = (((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) |
| 25 | 24 | oveq1i 7441 |
. . . 4
⊢ ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) = ((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) |
| 26 | 8, 10 | mulcli 11268 |
. . . . . 6
⊢ (;99 · 𝐴) ∈ ℂ |
| 27 | 18, 19 | mulcli 11268 |
. . . . . 6
⊢ (9
· 𝐵) ∈
ℂ |
| 28 | | add4 11482 |
. . . . . . 7
⊢ ((((;99 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) ∧ ((9 · 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ)) →
(((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) = (((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵))) |
| 29 | 28 | oveq1d 7446 |
. . . . . 6
⊢ ((((;99 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) ∧ ((9 · 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ)) →
((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) = ((((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵)) + 𝐶)) |
| 30 | 26, 10, 27, 19, 29 | mp4an 693 |
. . . . 5
⊢ ((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) = ((((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵)) + 𝐶) |
| 31 | 26, 27 | addcli 11267 |
. . . . . 6
⊢ ((;99 · 𝐴) + (9 · 𝐵)) ∈ ℂ |
| 32 | 10, 19 | addcli 11267 |
. . . . . 6
⊢ (𝐴 + 𝐵) ∈ ℂ |
| 33 | | 3dvds2dec.c |
. . . . . . 7
⊢ 𝐶 ∈
ℕ0 |
| 34 | 33 | nn0cni 12538 |
. . . . . 6
⊢ 𝐶 ∈ ℂ |
| 35 | 31, 32, 34 | addassi 11271 |
. . . . 5
⊢ ((((;99 · 𝐴) + (9 · 𝐵)) + (𝐴 + 𝐵)) + 𝐶) = (((;99 · 𝐴) + (9 · 𝐵)) + ((𝐴 + 𝐵) + 𝐶)) |
| 36 | | 9t11e99 12863 |
. . . . . . . . . . 11
⊢ (9
· ;11) = ;99 |
| 37 | 36 | eqcomi 2746 |
. . . . . . . . . 10
⊢ ;99 = (9 · ;11) |
| 38 | 37 | oveq1i 7441 |
. . . . . . . . 9
⊢ (;99 · 𝐴) = ((9 · ;11) · 𝐴) |
| 39 | | 1nn0 12542 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
| 40 | 39, 39 | deccl 12748 |
. . . . . . . . . . 11
⊢ ;11 ∈
ℕ0 |
| 41 | 40 | nn0cni 12538 |
. . . . . . . . . 10
⊢ ;11 ∈ ℂ |
| 42 | 18, 41, 10 | mulassi 11272 |
. . . . . . . . 9
⊢ ((9
· ;11) · 𝐴) = (9 · (;11 · 𝐴)) |
| 43 | 38, 42 | eqtri 2765 |
. . . . . . . 8
⊢ (;99 · 𝐴) = (9 · (;11 · 𝐴)) |
| 44 | 43 | oveq1i 7441 |
. . . . . . 7
⊢ ((;99 · 𝐴) + (9 · 𝐵)) = ((9 · (;11 · 𝐴)) + (9 · 𝐵)) |
| 45 | 41, 10 | mulcli 11268 |
. . . . . . . . 9
⊢ (;11 · 𝐴) ∈ ℂ |
| 46 | 18, 45, 19 | adddii 11273 |
. . . . . . . 8
⊢ (9
· ((;11 · 𝐴) + 𝐵)) = ((9 · (;11 · 𝐴)) + (9 · 𝐵)) |
| 47 | 46 | eqcomi 2746 |
. . . . . . 7
⊢ ((9
· (;11 · 𝐴)) + (9 · 𝐵)) = (9 · ((;11 · 𝐴) + 𝐵)) |
| 48 | | 3t3e9 12433 |
. . . . . . . . . 10
⊢ (3
· 3) = 9 |
| 49 | 48 | eqcomi 2746 |
. . . . . . . . 9
⊢ 9 = (3
· 3) |
| 50 | 49 | oveq1i 7441 |
. . . . . . . 8
⊢ (9
· ((;11 · 𝐴) + 𝐵)) = ((3 · 3) · ((;11 · 𝐴) + 𝐵)) |
| 51 | | 3cn 12347 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
| 52 | 45, 19 | addcli 11267 |
. . . . . . . . 9
⊢ ((;11 · 𝐴) + 𝐵) ∈ ℂ |
| 53 | 51, 51, 52 | mulassi 11272 |
. . . . . . . 8
⊢ ((3
· 3) · ((;11
· 𝐴) + 𝐵)) = (3 · (3 ·
((;11 · 𝐴) + 𝐵))) |
| 54 | 50, 53 | eqtri 2765 |
. . . . . . 7
⊢ (9
· ((;11 · 𝐴) + 𝐵)) = (3 · (3 · ((;11 · 𝐴) + 𝐵))) |
| 55 | 44, 47, 54 | 3eqtri 2769 |
. . . . . 6
⊢ ((;99 · 𝐴) + (9 · 𝐵)) = (3 · (3 · ((;11 · 𝐴) + 𝐵))) |
| 56 | 55 | oveq1i 7441 |
. . . . 5
⊢ (((;99 · 𝐴) + (9 · 𝐵)) + ((𝐴 + 𝐵) + 𝐶)) = ((3 · (3 · ((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)) |
| 57 | 30, 35, 56 | 3eqtri 2769 |
. . . 4
⊢ ((((;99 · 𝐴) + 𝐴) + ((9 · 𝐵) + 𝐵)) + 𝐶) = ((3 · (3 · ((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)) |
| 58 | 3, 25, 57 | 3eqtri 2769 |
. . 3
⊢ ;;𝐴𝐵𝐶 = ((3 · (3 · ((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)) |
| 59 | 58 | breq2i 5151 |
. 2
⊢ (3
∥ ;;𝐴𝐵𝐶 ↔ 3 ∥ ((3 · (3 ·
((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶))) |
| 60 | | 3z 12650 |
. . 3
⊢ 3 ∈
ℤ |
| 61 | 1 | nn0zi 12642 |
. . . . 5
⊢ 𝐴 ∈ ℤ |
| 62 | 2 | nn0zi 12642 |
. . . . 5
⊢ 𝐵 ∈ ℤ |
| 63 | | zaddcl 12657 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℤ) |
| 64 | 61, 62, 63 | mp2an 692 |
. . . 4
⊢ (𝐴 + 𝐵) ∈ ℤ |
| 65 | 33 | nn0zi 12642 |
. . . 4
⊢ 𝐶 ∈ ℤ |
| 66 | | zaddcl 12657 |
. . . 4
⊢ (((𝐴 + 𝐵) ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 + 𝐵) + 𝐶) ∈ ℤ) |
| 67 | 64, 65, 66 | mp2an 692 |
. . 3
⊢ ((𝐴 + 𝐵) + 𝐶) ∈ ℤ |
| 68 | 40 | nn0zi 12642 |
. . . . . . . 8
⊢ ;11 ∈ ℤ |
| 69 | | zmulcl 12666 |
. . . . . . . 8
⊢ ((;11 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (;11 · 𝐴) ∈ ℤ) |
| 70 | 68, 61, 69 | mp2an 692 |
. . . . . . 7
⊢ (;11 · 𝐴) ∈ ℤ |
| 71 | | zaddcl 12657 |
. . . . . . 7
⊢ (((;11 · 𝐴) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((;11 · 𝐴) + 𝐵) ∈ ℤ) |
| 72 | 70, 62, 71 | mp2an 692 |
. . . . . 6
⊢ ((;11 · 𝐴) + 𝐵) ∈ ℤ |
| 73 | | zmulcl 12666 |
. . . . . 6
⊢ ((3
∈ ℤ ∧ ((;11
· 𝐴) + 𝐵) ∈ ℤ) → (3
· ((;11 · 𝐴) + 𝐵)) ∈ ℤ) |
| 74 | 60, 72, 73 | mp2an 692 |
. . . . 5
⊢ (3
· ((;11 · 𝐴) + 𝐵)) ∈ ℤ |
| 75 | | zmulcl 12666 |
. . . . 5
⊢ ((3
∈ ℤ ∧ (3 · ((;11 · 𝐴) + 𝐵)) ∈ ℤ) → (3 · (3
· ((;11 · 𝐴) + 𝐵))) ∈ ℤ) |
| 76 | 60, 74, 75 | mp2an 692 |
. . . 4
⊢ (3
· (3 · ((;11
· 𝐴) + 𝐵))) ∈
ℤ |
| 77 | | dvdsmul1 16315 |
. . . . 5
⊢ ((3
∈ ℤ ∧ (3 · ((;11 · 𝐴) + 𝐵)) ∈ ℤ) → 3 ∥ (3
· (3 · ((;11
· 𝐴) + 𝐵)))) |
| 78 | 60, 74, 77 | mp2an 692 |
. . . 4
⊢ 3 ∥
(3 · (3 · ((;11
· 𝐴) + 𝐵))) |
| 79 | 76, 78 | pm3.2i 470 |
. . 3
⊢ ((3
· (3 · ((;11
· 𝐴) + 𝐵))) ∈ ℤ ∧ 3
∥ (3 · (3 · ((;11 · 𝐴) + 𝐵)))) |
| 80 | | dvdsadd2b 16343 |
. . 3
⊢ ((3
∈ ℤ ∧ ((𝐴 +
𝐵) + 𝐶) ∈ ℤ ∧ ((3 · (3
· ((;11 · 𝐴) + 𝐵))) ∈ ℤ ∧ 3 ∥ (3
· (3 · ((;11
· 𝐴) + 𝐵))))) → (3 ∥ ((𝐴 + 𝐵) + 𝐶) ↔ 3 ∥ ((3 · (3 ·
((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶)))) |
| 81 | 60, 67, 79, 80 | mp3an 1463 |
. 2
⊢ (3
∥ ((𝐴 + 𝐵) + 𝐶) ↔ 3 ∥ ((3 · (3 ·
((;11 · 𝐴) + 𝐵))) + ((𝐴 + 𝐵) + 𝐶))) |
| 82 | 59, 81 | bitr4i 278 |
1
⊢ (3
∥ ;;𝐴𝐵𝐶 ↔ 3 ∥ ((𝐴 + 𝐵) + 𝐶)) |