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 
|- A e. NN0
3dvdsdec.b 
|- B e. NN0
3dvds2dec.c 
|- C e. NN0
Assertion 3dvds2dec 
|- ( 3 || ; ; A B C <-> 3 || ( ( A + B ) + C ) )

Proof

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