Metamath Proof Explorer

Theorem 3dvds2dec

Description: A decimal number is divisible by three iff the sum of its three "digits" is divisible by three. The term "digits" in its narrow sense is only correct if A , B and C actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers A , B and C . (Contributed by AV, 14-Jun-2021) (Revised by AV, 1-Aug-2021)

Ref Expression
Hypotheses 3dvdsdec.a ⊢ 𝐴 ∈ ℕ0
3dvdsdec.b ⊢ 𝐵 ∈ ℕ0
3dvds2dec.c ⊢ 𝐶 ∈ ℕ0
Assertion 3dvds2dec ( 3 ∥ 𝐴 𝐵 𝐶 ↔ 3 ∥ ( ( 𝐴 + 𝐵 ) + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 3dvdsdec.a ⊢ 𝐴 ∈ ℕ0
2 3dvdsdec.b ⊢ 𝐵 ∈ ℕ0
3 3dvds2dec.c ⊢ 𝐶 ∈ ℕ0
4 1 2 3dec ⊢ 𝐴 𝐵 𝐶 = ( ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 )
5 sq10e99m1 ⊢ ( 1 0 ↑ 2 ) = ( 9 9 + 1 )
6 5 oveq1i ⊢ ( ( 1 0 ↑ 2 ) · 𝐴 ) = ( ( 9 9 + 1 ) · 𝐴 )
7 9nn0 ⊢ 9 ∈ ℕ0
8 7 7 deccl ⊢ 9 9 ∈ ℕ0
9 8 nn0cni ⊢ 9 9 ∈ ℂ
10 ax-1cn ⊢ 1 ∈ ℂ
11 1 nn0cni ⊢ 𝐴 ∈ ℂ
12 9 10 11 adddiri ⊢ ( ( 9 9 + 1 ) · 𝐴 ) = ( ( 9 9 · 𝐴 ) + ( 1 · 𝐴 ) )
13 11 mulid2i ⊢ ( 1 · 𝐴 ) = 𝐴
14 13 oveq2i ⊢ ( ( 9 9 · 𝐴 ) + ( 1 · 𝐴 ) ) = ( ( 9 9 · 𝐴 ) + 𝐴 )
15 6 12 14 3eqtri ⊢ ( ( 1 0 ↑ 2 ) · 𝐴 ) = ( ( 9 9 · 𝐴 ) + 𝐴 )
16 9p1e10 ⊢ ( 9 + 1 ) = 1 0
17 16 eqcomi ⊢ 1 0 = ( 9 + 1 )
18 17 oveq1i ⊢ ( 1 0 · 𝐵 ) = ( ( 9 + 1 ) · 𝐵 )
19 9cn ⊢ 9 ∈ ℂ
20 2 nn0cni ⊢ 𝐵 ∈ ℂ
21 19 10 20 adddiri ⊢ ( ( 9 + 1 ) · 𝐵 ) = ( ( 9 · 𝐵 ) + ( 1 · 𝐵 ) )
22 20 mulid2i ⊢ ( 1 · 𝐵 ) = 𝐵
23 22 oveq2i ⊢ ( ( 9 · 𝐵 ) + ( 1 · 𝐵 ) ) = ( ( 9 · 𝐵 ) + 𝐵 )
24 18 21 23 3eqtri ⊢ ( 1 0 · 𝐵 ) = ( ( 9 · 𝐵 ) + 𝐵 )
25 15 24 oveq12i ⊢ ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) ) = ( ( ( 9 9 · 𝐴 ) + 𝐴 ) + ( ( 9 · 𝐵 ) + 𝐵 ) )
26 25 oveq1i ⊢ ( ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 ) = ( ( ( ( 9 9 · 𝐴 ) + 𝐴 ) + ( ( 9 · 𝐵 ) + 𝐵 ) ) + 𝐶 )
27 9 11 mulcli ⊢ ( 9 9 · 𝐴 ) ∈ ℂ
28 19 20 mulcli ⊢ ( 9 · 𝐵 ) ∈ ℂ
29 add4 ⊢ ( ( ( ( 9 9 · 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) ∧ ( ( 9 · 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( ( ( 9 9 · 𝐴 ) + 𝐴 ) + ( ( 9 · 𝐵 ) + 𝐵 ) ) = ( ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) + ( 𝐴 + 𝐵 ) ) )
30 29 oveq1d ⊢ ( ( ( ( 9 9 · 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) ∧ ( ( 9 · 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( ( ( ( 9 9 · 𝐴 ) + 𝐴 ) + ( ( 9 · 𝐵 ) + 𝐵 ) ) + 𝐶 ) = ( ( ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) + ( 𝐴 + 𝐵 ) ) + 𝐶 ) )
31 27 11 28 20 30 mp4an ⊢ ( ( ( ( 9 9 · 𝐴 ) + 𝐴 ) + ( ( 9 · 𝐵 ) + 𝐵 ) ) + 𝐶 ) = ( ( ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) + ( 𝐴 + 𝐵 ) ) + 𝐶 )
32 27 28 addcli ⊢ ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) ∈ ℂ
33 11 20 addcli ⊢ ( 𝐴 + 𝐵 ) ∈ ℂ
34 3 nn0cni ⊢ 𝐶 ∈ ℂ
35 32 33 34 addassi ⊢ ( ( ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) + ( 𝐴 + 𝐵 ) ) + 𝐶 ) = ( ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) )
36 9t11e99 ⊢ ( 9 · 1 1 ) = 9 9
37 36 eqcomi ⊢ 9 9 = ( 9 · 1 1 )
38 37 oveq1i ⊢ ( 9 9 · 𝐴 ) = ( ( 9 · 1 1 ) · 𝐴 )
39 1nn0 ⊢ 1 ∈ ℕ0
40 39 39 deccl ⊢ 1 1 ∈ ℕ0
41 40 nn0cni ⊢ 1 1 ∈ ℂ
42 19 41 11 mulassi ⊢ ( ( 9 · 1 1 ) · 𝐴 ) = ( 9 · ( 1 1 · 𝐴 ) )
43 38 42 eqtri ⊢ ( 9 9 · 𝐴 ) = ( 9 · ( 1 1 · 𝐴 ) )
44 43 oveq1i ⊢ ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) = ( ( 9 · ( 1 1 · 𝐴 ) ) + ( 9 · 𝐵 ) )
45 41 11 mulcli ⊢ ( 1 1 · 𝐴 ) ∈ ℂ
46 19 45 20 adddii ⊢ ( 9 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) = ( ( 9 · ( 1 1 · 𝐴 ) ) + ( 9 · 𝐵 ) )
47 46 eqcomi ⊢ ( ( 9 · ( 1 1 · 𝐴 ) ) + ( 9 · 𝐵 ) ) = ( 9 · ( ( 1 1 · 𝐴 ) + 𝐵 ) )
48 3t3e9 ⊢ ( 3 · 3 ) = 9
49 48 eqcomi ⊢ 9 = ( 3 · 3 )
50 49 oveq1i ⊢ ( 9 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) = ( ( 3 · 3 ) · ( ( 1 1 · 𝐴 ) + 𝐵 ) )
51 3cn ⊢ 3 ∈ ℂ
52 45 20 addcli ⊢ ( ( 1 1 · 𝐴 ) + 𝐵 ) ∈ ℂ
53 51 51 52 mulassi ⊢ ( ( 3 · 3 ) · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) = ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) )
54 50 53 eqtri ⊢ ( 9 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) = ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) )
55 44 47 54 3eqtri ⊢ ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) = ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) )
56 55 oveq1i ⊢ ( ( ( 9 9 · 𝐴 ) + ( 9 · 𝐵 ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) ) = ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) )
57 31 35 56 3eqtri ⊢ ( ( ( ( 9 9 · 𝐴 ) + 𝐴 ) + ( ( 9 · 𝐵 ) + 𝐵 ) ) + 𝐶 ) = ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) )
58 4 26 57 3eqtri ⊢ 𝐴 𝐵 𝐶 = ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) )
59 58 breq2i ⊢ ( 3 ∥ 𝐴 𝐵 𝐶 ↔ 3 ∥ ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) ) )
60 3z ⊢ 3 ∈ ℤ
61 1 nn0zi ⊢ 𝐴 ∈ ℤ
62 2 nn0zi ⊢ 𝐵 ∈ ℤ
63 zaddcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
64 61 62 63 mp2an ⊢ ( 𝐴 + 𝐵 ) ∈ ℤ
65 3 nn0zi ⊢ 𝐶 ∈ ℤ
66 zaddcl ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) ∈ ℤ )
67 64 65 66 mp2an ⊢ ( ( 𝐴 + 𝐵 ) + 𝐶 ) ∈ ℤ
68 40 nn0zi ⊢ 1 1 ∈ ℤ
69 zmulcl ⊢ ( ( 1 1 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 1 · 𝐴 ) ∈ ℤ )
70 68 61 69 mp2an ⊢ ( 1 1 · 𝐴 ) ∈ ℤ
71 zaddcl ⊢ ( ( ( 1 1 · 𝐴 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 1 1 · 𝐴 ) + 𝐵 ) ∈ ℤ )
72 70 62 71 mp2an ⊢ ( ( 1 1 · 𝐴 ) + 𝐵 ) ∈ ℤ
73 zmulcl ⊢ ( ( 3 ∈ ℤ ∧ ( ( 1 1 · 𝐴 ) + 𝐵 ) ∈ ℤ ) → ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ∈ ℤ )
74 60 72 73 mp2an ⊢ ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ∈ ℤ
75 zmulcl ⊢ ( ( 3 ∈ ℤ ∧ ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ∈ ℤ ) → ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) ∈ ℤ )
76 60 74 75 mp2an ⊢ ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) ∈ ℤ
77 dvdsmul1 ⊢ ( ( 3 ∈ ℤ ∧ ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ∈ ℤ ) → 3 ∥ ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) )
78 60 74 77 mp2an ⊢ 3 ∥ ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) )
79 76 78 pm3.2i ⊢ ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) ∈ ℤ ∧ 3 ∥ ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) )
80 dvdsadd2b ⊢ ( ( 3 ∈ ℤ ∧ ( ( 𝐴 + 𝐵 ) + 𝐶 ) ∈ ℤ ∧ ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) ∈ ℤ ∧ 3 ∥ ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) ) ) → ( 3 ∥ ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↔ 3 ∥ ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) ) ) )
81 60 67 79 80 mp3an ⊢ ( 3 ∥ ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↔ 3 ∥ ( ( 3 · ( 3 · ( ( 1 1 · 𝐴 ) + 𝐵 ) ) ) + ( ( 𝐴 + 𝐵 ) + 𝐶 ) ) )
82 59 81 bitr4i ⊢ ( 3 ∥ 𝐴 𝐵 𝐶 ↔ 3 ∥ ( ( 𝐴 + 𝐵 ) + 𝐶 ) )