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 ∥ ( ( 𝐴 + 𝐵 ) + 𝐶 ) )