Metamath Proof Explorer

Theorem 3dvdsdec

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

Ref Expression
Hypotheses 3dvdsdec.a 
|- A e. NN0
3dvdsdec.b 
|- B e. NN0
Assertion 3dvdsdec 
|- ( 3 || ; A B <-> 3 || ( A + B ) )

Proof

Step Hyp Ref Expression
1 3dvdsdec.a 
 |-  A e. NN0
2 3dvdsdec.b 
 |-  B e. NN0
3 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
4 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
5 4 eqcomi 
 |-  ; 1 0 = ( 9 + 1 )
6 5 oveq1i 
 |-  ( ; 1 0 x. A ) = ( ( 9 + 1 ) x. A )
7 9cn 
 |-  9 e. CC
8 ax-1cn 
 |-  1 e. CC
9 1 nn0cni 
 |-  A e. CC
10 7 8 9 adddiri 
 |-  ( ( 9 + 1 ) x. A ) = ( ( 9 x. A ) + ( 1 x. A ) )
11 9 mullidi 
 |-  ( 1 x. A ) = A
12 11 oveq2i 
 |-  ( ( 9 x. A ) + ( 1 x. A ) ) = ( ( 9 x. A ) + A )
13 6 10 12 3eqtri 
 |-  ( ; 1 0 x. A ) = ( ( 9 x. A ) + A )
14 13 oveq1i 
 |-  ( ( ; 1 0 x. A ) + B ) = ( ( ( 9 x. A ) + A ) + B )
15 7 9 mulcli 
 |-  ( 9 x. A ) e. CC
16 2 nn0cni 
 |-  B e. CC
17 15 9 16 addassi 
 |-  ( ( ( 9 x. A ) + A ) + B ) = ( ( 9 x. A ) + ( A + B ) )
18 3 14 17 3eqtri 
 |-  ; A B = ( ( 9 x. A ) + ( A + B ) )
19 18 breq2i 
 |-  ( 3 || ; A B <-> 3 || ( ( 9 x. A ) + ( A + B ) ) )
20 3z 
 |-  3 e. ZZ
21 1 nn0zi 
 |-  A e. ZZ
22 2 nn0zi 
 |-  B e. ZZ
23 zaddcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
24 21 22 23 mp2an 
 |-  ( A + B ) e. ZZ
25 9nn 
 |-  9 e. NN
26 25 nnzi 
 |-  9 e. ZZ
27 zmulcl 
 |-  ( ( 9 e. ZZ /\ A e. ZZ ) -> ( 9 x. A ) e. ZZ )
28 26 21 27 mp2an 
 |-  ( 9 x. A ) e. ZZ
29 zmulcl 
 |-  ( ( 3 e. ZZ /\ A e. ZZ ) -> ( 3 x. A ) e. ZZ )
30 20 21 29 mp2an 
 |-  ( 3 x. A ) e. ZZ
31 dvdsmul1 
 |-  ( ( 3 e. ZZ /\ ( 3 x. A ) e. ZZ ) -> 3 || ( 3 x. ( 3 x. A ) ) )
32 20 30 31 mp2an 
 |-  3 || ( 3 x. ( 3 x. A ) )
33 3t3e9 
 |-  ( 3 x. 3 ) = 9
34 33 eqcomi 
 |-  9 = ( 3 x. 3 )
35 34 oveq1i 
 |-  ( 9 x. A ) = ( ( 3 x. 3 ) x. A )
36 3cn 
 |-  3 e. CC
37 36 36 9 mulassi 
 |-  ( ( 3 x. 3 ) x. A ) = ( 3 x. ( 3 x. A ) )
38 35 37 eqtri 
 |-  ( 9 x. A ) = ( 3 x. ( 3 x. A ) )
39 32 38 breqtrri 
 |-  3 || ( 9 x. A )
40 28 39 pm3.2i 
 |-  ( ( 9 x. A ) e. ZZ /\ 3 || ( 9 x. A ) )
41 dvdsadd2b 
 |-  ( ( 3 e. ZZ /\ ( A + B ) e. ZZ /\ ( ( 9 x. A ) e. ZZ /\ 3 || ( 9 x. A ) ) ) -> ( 3 || ( A + B ) <-> 3 || ( ( 9 x. A ) + ( A + B ) ) ) )
42 20 24 40 41 mp3an 
 |-  ( 3 || ( A + B ) <-> 3 || ( ( 9 x. A ) + ( A + B ) ) )
43 19 42 bitr4i 
 |-  ( 3 || ; A B <-> 3 || ( A + B ) )