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\in {\mathbb{N}}_0$$
	3dvdsdec.b	$$⊢B\in {\mathbb{N}}_0$$
	3dvds2dec.c	$$⊢C\in {\mathbb{N}}_0$$
Assertion	3dvds2dec	Could not format assertion : No typesetting found for |- ( 3 || ; ; A B C <-> 3 || ( ( A + B ) + C ) ) with typecode |-

Proof

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