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 A0
3dvdsdec.b B0
Assertion 3dvdsdec Could not format assertion : No typesetting found for |- ( 3 || ; A B <-> 3 || ( A + B ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 3dvdsdec.a A0
2 3dvdsdec.b B0
3 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
4 9p1e10 9+1=10
5 4 eqcomi 10=9+1
6 5 oveq1i 10A=9+1A
7 9cn 9
8 ax-1cn 1
9 1 nn0cni A
10 7 8 9 adddiri 9+1A=9A+1A
11 9 mulid2i 1A=A
12 11 oveq2i 9A+1A=9A+A
13 6 10 12 3eqtri 10A=9A+A
14 13 oveq1i 10A+B=9A+A+B
15 7 9 mulcli 9A
16 2 nn0cni B
17 15 9 16 addassi 9A+A+B=9A+A+B
18 3 14 17 3eqtri Could not format ; A B = ( ( 9 x. A ) + ( A + B ) ) : No typesetting found for |- ; A B = ( ( 9 x. A ) + ( A + B ) ) with typecode |-
19 18 breq2i Could not format ( 3 || ; A B <-> 3 || ( ( 9 x. A ) + ( A + B ) ) ) : No typesetting found for |- ( 3 || ; A B <-> 3 || ( ( 9 x. A ) + ( A + B ) ) ) with typecode |-
20 3z 3
21 1 nn0zi A
22 2 nn0zi B
23 zaddcl ABA+B
24 21 22 23 mp2an A+B
25 9nn 9
26 25 nnzi 9
27 zmulcl 9A9A
28 26 21 27 mp2an 9A
29 zmulcl 3A3A
30 20 21 29 mp2an 3A
31 dvdsmul1 33A333A
32 20 30 31 mp2an 333A
33 3t3e9 33=9
34 33 eqcomi 9=33
35 34 oveq1i 9A=33A
36 3cn 3
37 36 36 9 mulassi 33A=33A
38 35 37 eqtri 9A=33A
39 32 38 breqtrri 39A
40 28 39 pm3.2i 9A39A
41 dvdsadd2b 3A+B9A39A3A+B39A+A+B
42 20 24 40 41 mp3an 3A+B39A+A+B
43 19 42 bitr4i Could not format ( 3 || ; A B <-> 3 || ( A + B ) ) : No typesetting found for |- ( 3 || ; A B <-> 3 || ( A + B ) ) with typecode |-