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\in {\mathbb{N}}_0$$
	3dvdsdec.b	$$⊢B\in {\mathbb{N}}_0$$
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	$$⊢A\in {\mathbb{N}}_0$$
2		3dvdsdec.b	$$⊢B\in {\mathbb{N}}_0$$
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=\left(9+1\right)A$$
7		9cn	$$⊢9\in ℂ$$
8		ax-1cn	$$⊢1\in ℂ$$
9	1	nn0cni	$$⊢A\in ℂ$$
10	7 8 9	adddiri	$$⊢\left(9+1\right)A=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\in ℂ$$
16	2	nn0cni	$$⊢B\in ℂ$$
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\in \mathbb{Z}$$
21	1	nn0zi	$$⊢A\in \mathbb{Z}$$
22	2	nn0zi	$$⊢B\in \mathbb{Z}$$
23		zaddcl	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A+B\in \mathbb{Z}$$
24	21 22 23	mp2an	$$⊢A+B\in \mathbb{Z}$$
25		9nn	$$⊢9\in \mathbb{N}$$
26	25	nnzi	$$⊢9\in \mathbb{Z}$$
27		zmulcl	$$⊢\left(9\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to 9A\in \mathbb{Z}$$
28	26 21 27	mp2an	$$⊢9A\in \mathbb{Z}$$
29		zmulcl	$$⊢\left(3\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to 3A\in \mathbb{Z}$$
30	20 21 29	mp2an	$$⊢3A\in \mathbb{Z}$$
31		dvdsmul1	$$⊢\left(3\in \mathbb{Z}\wedge 3A\in \mathbb{Z}\right)\to 3\parallel 33A$$
32	20 30 31	mp2an	$$⊢3\parallel 33A$$
33		3t3e9	$$⊢3\cdot 3=9$$
34	33	eqcomi	$$⊢9=3\cdot 3$$
35	34	oveq1i	$$⊢9A=3\cdot 3A$$
36		3cn	$$⊢3\in ℂ$$
37	36 36 9	mulassi	$$⊢3\cdot 3A=33A$$
38	35 37	eqtri	$$⊢9A=33A$$
39	32 38	breqtrri	$$⊢3\parallel 9A$$
40	28 39	pm3.2i	$$⊢\left(9A\in \mathbb{Z}\wedge 3\parallel 9A\right)$$
41		dvdsadd2b	$$⊢\left(3\in \mathbb{Z}\wedge A+B\in \mathbb{Z}\wedge \left(9A\in \mathbb{Z}\wedge 3\parallel 9A\right)\right)\to \left(3\parallel \left(A+B\right)\leftrightarrow 3\parallel \left(9A+A+B\right)\right)$$
42	20 24 40 41	mp3an	$$⊢3\parallel \left(A+B\right)\leftrightarrow 3\parallel \left(9A+A+B\right)$$
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 |-