Theorem 3dvds

Description: A rule for divisibility by 3 of a number written in base 10. This is Metamath 100 proof #85. (Contributed by Mario Carneiro, 14-Jul-2014) (Revised by Mario Carneiro, 17-Jan-2015) (Revised by AV, 8-Sep-2021)

	Ref	Expression
Assertion	3dvds	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to \left(3\parallel \sum _{k=0}^{N}F\left(k\right){10}^k\leftrightarrow 3\parallel \sum _{k=0}^{N}F\left(k\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		3z	$$⊢3\in \mathbb{Z}$$
2	1	a1i	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to 3\in \mathbb{Z}$$
3		fzfid	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to \left(0\dots N\right)\in \mathrm{Fin}$$
4		ffvelcdm	$$⊢\left(F:\left(0\dots N\right)⟶\mathbb{Z}\wedge k\in \left(0\dots N\right)\right)\to F\left(k\right)\in \mathbb{Z}$$
5	4	adantll	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to F\left(k\right)\in \mathbb{Z}$$
6		10nn	$$⊢10\in \mathbb{N}$$
7	6	nnzi	$$⊢10\in \mathbb{Z}$$
8		elfznn0	$$⊢k\in \left(0\dots N\right)\to k\in {\mathbb{N}}_0$$
9	8	adantl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to k\in {\mathbb{N}}_0$$
10		zexpcl	$$⊢\left(10\in \mathbb{Z}\wedge k\in {\mathbb{N}}_0\right)\to {10}^k\in \mathbb{Z}$$
11	7 9 10	sylancr	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to {10}^k\in \mathbb{Z}$$
12	5 11	zmulcld	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to F\left(k\right){10}^k\in \mathbb{Z}$$
13	3 12	fsumzcl	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to \sum _{k=0}^{N}F\left(k\right){10}^k\in \mathbb{Z}$$
14	3 5	fsumzcl	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to \sum _{k=0}^{N}F\left(k\right)\in \mathbb{Z}$$
15	12 5	zsubcld	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to F\left(k\right){10}^k-F\left(k\right)\in \mathbb{Z}$$
16		ax-1cn	$$⊢1\in ℂ$$
17	6	nncni	$$⊢10\in ℂ$$
18	16 17	negsubdi2i	$$⊢-\left(1-10\right)=10-1$$
19		9p1e10	$$⊢9+1=10$$
20	19	eqcomi	$$⊢10=9+1$$
21	20	oveq1i	$$⊢10-1=9+1-1$$
22		9cn	$$⊢9\in ℂ$$
23	22 16	pncan3oi	$$⊢9+1-1=9$$
24	18 21 23	3eqtri	$$⊢-\left(1-10\right)=9$$
25		3t3e9	$$⊢3\cdot 3=9$$
26	24 25	eqtr4i	$$⊢-\left(1-10\right)=3\cdot 3$$
27	17	a1i	$$⊢k\in {\mathbb{N}}_0\to 10\in ℂ$$
28		1re	$$⊢1\in ℝ$$
29		1lt10	$$⊢1<10$$
30	28 29	gtneii	$$⊢10\ne 1$$
31	30	a1i	$$⊢k\in {\mathbb{N}}_0\to 10\ne 1$$
32		id	$$⊢k\in {\mathbb{N}}_0\to k\in {\mathbb{N}}_0$$
33	27 31 32	geoser	$$⊢k\in {\mathbb{N}}_0\to \sum _{j=0}^{k-1}{10}^j=\frac{1-{10}^k}{1-10}$$
34		fzfid	$$⊢k\in {\mathbb{N}}_0\to \left(0\dots k-1\right)\in \mathrm{Fin}$$
35		elfznn0	$$⊢j\in \left(0\dots k-1\right)\to j\in {\mathbb{N}}_0$$
36	35	adantl	$$⊢\left(k\in {\mathbb{N}}_0\wedge j\in \left(0\dots k-1\right)\right)\to j\in {\mathbb{N}}_0$$
37		zexpcl	$$⊢\left(10\in \mathbb{Z}\wedge j\in {\mathbb{N}}_0\right)\to {10}^j\in \mathbb{Z}$$
38	7 36 37	sylancr	$$⊢\left(k\in {\mathbb{N}}_0\wedge j\in \left(0\dots k-1\right)\right)\to {10}^j\in \mathbb{Z}$$
39	34 38	fsumzcl	$$⊢k\in {\mathbb{N}}_0\to \sum _{j=0}^{k-1}{10}^j\in \mathbb{Z}$$
40	33 39	eqeltrrd	$$⊢k\in {\mathbb{N}}_0\to \frac{1-{10}^k}{1-10}\in \mathbb{Z}$$
41		1z	$$⊢1\in \mathbb{Z}$$
42		zsubcl	$$⊢\left(1\in \mathbb{Z}\wedge 10\in \mathbb{Z}\right)\to 1-10\in \mathbb{Z}$$
43	41 7 42	mp2an	$$⊢1-10\in \mathbb{Z}$$
44	28 29	ltneii	$$⊢1\ne 10$$
45	16 17	subeq0i	$$⊢1-10=0\leftrightarrow 1=10$$
46	45	necon3bii	$$⊢1-10\ne 0\leftrightarrow 1\ne 10$$
47	44 46	mpbir	$$⊢1-10\ne 0$$
48	7 32 10	sylancr	$$⊢k\in {\mathbb{N}}_0\to {10}^k\in \mathbb{Z}$$
49		zsubcl	$$⊢\left(1\in \mathbb{Z}\wedge {10}^k\in \mathbb{Z}\right)\to 1-{10}^k\in \mathbb{Z}$$
50	41 48 49	sylancr	$$⊢k\in {\mathbb{N}}_0\to 1-{10}^k\in \mathbb{Z}$$
51		dvdsval2	$$⊢\left(1-10\in \mathbb{Z}\wedge 1-10\ne 0\wedge 1-{10}^k\in \mathbb{Z}\right)\to \left(\left(1-10\right)\parallel \left(1-{10}^k\right)\leftrightarrow \frac{1-{10}^k}{1-10}\in \mathbb{Z}\right)$$
52	43 47 50 51	mp3an12i	$$⊢k\in {\mathbb{N}}_0\to \left(\left(1-10\right)\parallel \left(1-{10}^k\right)\leftrightarrow \frac{1-{10}^k}{1-10}\in \mathbb{Z}\right)$$
53	40 52	mpbird	$$⊢k\in {\mathbb{N}}_0\to \left(1-10\right)\parallel \left(1-{10}^k\right)$$
54	48	zcnd	$$⊢k\in {\mathbb{N}}_0\to {10}^k\in ℂ$$
55		negsubdi2	$$⊢\left({10}^k\in ℂ\wedge 1\in ℂ\right)\to -\left({10}^k-1\right)=1-{10}^k$$
56	54 16 55	sylancl	$$⊢k\in {\mathbb{N}}_0\to -\left({10}^k-1\right)=1-{10}^k$$
57	53 56	breqtrrd	$$⊢k\in {\mathbb{N}}_0\to \left(1-10\right)\parallel \left(-\left({10}^k-1\right)\right)$$
58		peano2zm	$$⊢{10}^k\in \mathbb{Z}\to {10}^k-1\in \mathbb{Z}$$
59	48 58	syl	$$⊢k\in {\mathbb{N}}_0\to {10}^k-1\in \mathbb{Z}$$
60		dvdsnegb	$$⊢\left(1-10\in \mathbb{Z}\wedge {10}^k-1\in \mathbb{Z}\right)\to \left(\left(1-10\right)\parallel \left({10}^k-1\right)\leftrightarrow \left(1-10\right)\parallel \left(-\left({10}^k-1\right)\right)\right)$$
61	43 59 60	sylancr	$$⊢k\in {\mathbb{N}}_0\to \left(\left(1-10\right)\parallel \left({10}^k-1\right)\leftrightarrow \left(1-10\right)\parallel \left(-\left({10}^k-1\right)\right)\right)$$
62	57 61	mpbird	$$⊢k\in {\mathbb{N}}_0\to \left(1-10\right)\parallel \left({10}^k-1\right)$$
63		negdvdsb	$$⊢\left(1-10\in \mathbb{Z}\wedge {10}^k-1\in \mathbb{Z}\right)\to \left(\left(1-10\right)\parallel \left({10}^k-1\right)\leftrightarrow \left(-\left(1-10\right)\right)\parallel \left({10}^k-1\right)\right)$$
64	43 59 63	sylancr	$$⊢k\in {\mathbb{N}}_0\to \left(\left(1-10\right)\parallel \left({10}^k-1\right)\leftrightarrow \left(-\left(1-10\right)\right)\parallel \left({10}^k-1\right)\right)$$
65	62 64	mpbid	$$⊢k\in {\mathbb{N}}_0\to \left(-\left(1-10\right)\right)\parallel \left({10}^k-1\right)$$
66	26 65	eqbrtrrid	$$⊢k\in {\mathbb{N}}_0\to 3\cdot 3\parallel \left({10}^k-1\right)$$
67		muldvds1	$$⊢\left(3\in \mathbb{Z}\wedge 3\in \mathbb{Z}\wedge {10}^k-1\in \mathbb{Z}\right)\to \left(3\cdot 3\parallel \left({10}^k-1\right)\to 3\parallel \left({10}^k-1\right)\right)$$
68	1 1 59 67	mp3an12i	$$⊢k\in {\mathbb{N}}_0\to \left(3\cdot 3\parallel \left({10}^k-1\right)\to 3\parallel \left({10}^k-1\right)\right)$$
69	66 68	mpd	$$⊢k\in {\mathbb{N}}_0\to 3\parallel \left({10}^k-1\right)$$
70	9 69	syl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to 3\parallel \left({10}^k-1\right)$$
71	11 58	syl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to {10}^k-1\in \mathbb{Z}$$
72		dvdsmultr2	$$⊢\left(3\in \mathbb{Z}\wedge F\left(k\right)\in \mathbb{Z}\wedge {10}^k-1\in \mathbb{Z}\right)\to \left(3\parallel \left({10}^k-1\right)\to 3\parallel F\left(k\right)\left({10}^k-1\right)\right)$$
73	1 5 71 72	mp3an2i	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to \left(3\parallel \left({10}^k-1\right)\to 3\parallel F\left(k\right)\left({10}^k-1\right)\right)$$
74	70 73	mpd	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to 3\parallel F\left(k\right)\left({10}^k-1\right)$$
75	5	zcnd	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to F\left(k\right)\in ℂ$$
76	11	zcnd	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to {10}^k\in ℂ$$
77	75 76	muls1d	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to F\left(k\right)\left({10}^k-1\right)=F\left(k\right){10}^k-F\left(k\right)$$
78	74 77	breqtrd	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to 3\parallel \left(F\left(k\right){10}^k-F\left(k\right)\right)$$
79	3 2 15 78	fsumdvds	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to 3\parallel \sum _{k=0}^N\left(F\left(k\right){10}^k-F\left(k\right)\right)$$
80	12	zcnd	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\wedge k\in \left(0\dots N\right)\right)\to F\left(k\right){10}^k\in ℂ$$
81	3 80 75	fsumsub	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to \sum _{k=0}^N\left(F\left(k\right){10}^k-F\left(k\right)\right)=\sum _{k=0}^{N}F\left(k\right){10}^k-\sum _{k=0}^{N}F\left(k\right)$$
82	79 81	breqtrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to 3\parallel \left(\sum _{k=0}^{N}F\left(k\right){10}^k-\sum _{k=0}^{N}F\left(k\right)\right)$$
83		dvdssub2	$$⊢\left(\left(3\in \mathbb{Z}\wedge \sum _{k=0}^{N}F\left(k\right){10}^k\in \mathbb{Z}\wedge \sum _{k=0}^{N}F\left(k\right)\in \mathbb{Z}\right)\wedge 3\parallel \left(\sum _{k=0}^{N}F\left(k\right){10}^k-\sum _{k=0}^{N}F\left(k\right)\right)\right)\to \left(3\parallel \sum _{k=0}^{N}F\left(k\right){10}^k\leftrightarrow 3\parallel \sum _{k=0}^{N}F\left(k\right)\right)$$
84	2 13 14 82 83	syl31anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶\mathbb{Z}\right)\to \left(3\parallel \sum _{k=0}^{N}F\left(k\right){10}^k\leftrightarrow 3\parallel \sum _{k=0}^{N}F\left(k\right)\right)$$