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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → ( 3 ∥ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) ↔ 3 ∥ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3z	⊢ 3 ∈ ℤ
2	1	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → 3 ∈ ℤ )
3		fzfid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → ( 0 ... 𝑁 ) ∈ Fin )
4		ffvelcdm	⊢ ( ( 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
5	4	adantll	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
6		10nn	⊢ ; 1 0 ∈ ℕ
7	6	nnzi	⊢ ; 1 0 ∈ ℤ
8		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
9	8	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
10		zexpcl	⊢ ( ( ; 1 0 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( ; 1 0 ↑ 𝑘 ) ∈ ℤ )
11	7 9 10	sylancr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ; 1 0 ↑ 𝑘 ) ∈ ℤ )
12	5 11	zmulcld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) ∈ ℤ )
13	3 12	fsumzcl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) ∈ ℤ )
14	3 5	fsumzcl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
15	12 5	zsubcld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − ( 𝐹 ‘ 𝑘 ) ) ∈ ℤ )
16		ax-1cn	⊢ 1 ∈ ℂ
17	6	nncni	⊢ ; 1 0 ∈ ℂ
18	16 17	negsubdi2i	⊢ - ( 1 − ; 1 0 ) = ( ; 1 0 − 1 )
19		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
20	19	eqcomi	⊢ ; 1 0 = ( 9 + 1 )
21	20	oveq1i	⊢ ( ; 1 0 − 1 ) = ( ( 9 + 1 ) − 1 )
22		9cn	⊢ 9 ∈ ℂ
23	22 16	pncan3oi	⊢ ( ( 9 + 1 ) − 1 ) = 9
24	18 21 23	3eqtri	⊢ - ( 1 − ; 1 0 ) = 9
25		3t3e9	⊢ ( 3 · 3 ) = 9
26	24 25	eqtr4i	⊢ - ( 1 − ; 1 0 ) = ( 3 · 3 )
27	17	a1i	⊢ ( 𝑘 ∈ ℕ0 → ; 1 0 ∈ ℂ )
28		1re	⊢ 1 ∈ ℝ
29		1lt10	⊢ 1 < ; 1 0
30	28 29	gtneii	⊢ ; 1 0 ≠ 1
31	30	a1i	⊢ ( 𝑘 ∈ ℕ0 → ; 1 0 ≠ 1 )
32		id	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℕ0 )
33	27 31 32	geoser	⊢ ( 𝑘 ∈ ℕ0 → Σ 𝑗 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( ; 1 0 ↑ 𝑗 ) = ( ( 1 − ( ; 1 0 ↑ 𝑘 ) ) / ( 1 − ; 1 0 ) ) )
34		fzfid	⊢ ( 𝑘 ∈ ℕ0 → ( 0 ... ( 𝑘 − 1 ) ) ∈ Fin )
35		elfznn0	⊢ ( 𝑗 ∈ ( 0 ... ( 𝑘 − 1 ) ) → 𝑗 ∈ ℕ0 )
36	35	adantl	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 ∈ ( 0 ... ( 𝑘 − 1 ) ) ) → 𝑗 ∈ ℕ0 )
37		zexpcl	⊢ ( ( ; 1 0 ∈ ℤ ∧ 𝑗 ∈ ℕ0 ) → ( ; 1 0 ↑ 𝑗 ) ∈ ℤ )
38	7 36 37	sylancr	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 ∈ ( 0 ... ( 𝑘 − 1 ) ) ) → ( ; 1 0 ↑ 𝑗 ) ∈ ℤ )
39	34 38	fsumzcl	⊢ ( 𝑘 ∈ ℕ0 → Σ 𝑗 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( ; 1 0 ↑ 𝑗 ) ∈ ℤ )
40	33 39	eqeltrrd	⊢ ( 𝑘 ∈ ℕ0 → ( ( 1 − ( ; 1 0 ↑ 𝑘 ) ) / ( 1 − ; 1 0 ) ) ∈ ℤ )
41		1z	⊢ 1 ∈ ℤ
42		zsubcl	⊢ ( ( 1 ∈ ℤ ∧ ; 1 0 ∈ ℤ ) → ( 1 − ; 1 0 ) ∈ ℤ )
43	41 7 42	mp2an	⊢ ( 1 − ; 1 0 ) ∈ ℤ
44	28 29	ltneii	⊢ 1 ≠ ; 1 0
45	16 17	subeq0i	⊢ ( ( 1 − ; 1 0 ) = 0 ↔ 1 = ; 1 0 )
46	45	necon3bii	⊢ ( ( 1 − ; 1 0 ) ≠ 0 ↔ 1 ≠ ; 1 0 )
47	44 46	mpbir	⊢ ( 1 − ; 1 0 ) ≠ 0
48	7 32 10	sylancr	⊢ ( 𝑘 ∈ ℕ0 → ( ; 1 0 ↑ 𝑘 ) ∈ ℤ )
49		zsubcl	⊢ ( ( 1 ∈ ℤ ∧ ( ; 1 0 ↑ 𝑘 ) ∈ ℤ ) → ( 1 − ( ; 1 0 ↑ 𝑘 ) ) ∈ ℤ )
50	41 48 49	sylancr	⊢ ( 𝑘 ∈ ℕ0 → ( 1 − ( ; 1 0 ↑ 𝑘 ) ) ∈ ℤ )
51		dvdsval2	⊢ ( ( ( 1 − ; 1 0 ) ∈ ℤ ∧ ( 1 − ; 1 0 ) ≠ 0 ∧ ( 1 − ( ; 1 0 ↑ 𝑘 ) ) ∈ ℤ ) → ( ( 1 − ; 1 0 ) ∥ ( 1 − ( ; 1 0 ↑ 𝑘 ) ) ↔ ( ( 1 − ( ; 1 0 ↑ 𝑘 ) ) / ( 1 − ; 1 0 ) ) ∈ ℤ ) )
52	43 47 50 51	mp3an12i	⊢ ( 𝑘 ∈ ℕ0 → ( ( 1 − ; 1 0 ) ∥ ( 1 − ( ; 1 0 ↑ 𝑘 ) ) ↔ ( ( 1 − ( ; 1 0 ↑ 𝑘 ) ) / ( 1 − ; 1 0 ) ) ∈ ℤ ) )
53	40 52	mpbird	⊢ ( 𝑘 ∈ ℕ0 → ( 1 − ; 1 0 ) ∥ ( 1 − ( ; 1 0 ↑ 𝑘 ) ) )
54	48	zcnd	⊢ ( 𝑘 ∈ ℕ0 → ( ; 1 0 ↑ 𝑘 ) ∈ ℂ )
55		negsubdi2	⊢ ( ( ( ; 1 0 ↑ 𝑘 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( ; 1 0 ↑ 𝑘 ) − 1 ) = ( 1 − ( ; 1 0 ↑ 𝑘 ) ) )
56	54 16 55	sylancl	⊢ ( 𝑘 ∈ ℕ0 → - ( ( ; 1 0 ↑ 𝑘 ) − 1 ) = ( 1 − ( ; 1 0 ↑ 𝑘 ) ) )
57	53 56	breqtrrd	⊢ ( 𝑘 ∈ ℕ0 → ( 1 − ; 1 0 ) ∥ - ( ( ; 1 0 ↑ 𝑘 ) − 1 ) )
58		peano2zm	⊢ ( ( ; 1 0 ↑ 𝑘 ) ∈ ℤ → ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ∈ ℤ )
59	48 58	syl	⊢ ( 𝑘 ∈ ℕ0 → ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ∈ ℤ )
60		dvdsnegb	⊢ ( ( ( 1 − ; 1 0 ) ∈ ℤ ∧ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ∈ ℤ ) → ( ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ↔ ( 1 − ; 1 0 ) ∥ - ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) )
61	43 59 60	sylancr	⊢ ( 𝑘 ∈ ℕ0 → ( ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ↔ ( 1 − ; 1 0 ) ∥ - ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) )
62	57 61	mpbird	⊢ ( 𝑘 ∈ ℕ0 → ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) )
63		negdvdsb	⊢ ( ( ( 1 − ; 1 0 ) ∈ ℤ ∧ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ∈ ℤ ) → ( ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ↔ - ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) )
64	43 59 63	sylancr	⊢ ( 𝑘 ∈ ℕ0 → ( ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ↔ - ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) )
65	62 64	mpbid	⊢ ( 𝑘 ∈ ℕ0 → - ( 1 − ; 1 0 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) )
66	26 65	eqbrtrrid	⊢ ( 𝑘 ∈ ℕ0 → ( 3 · 3 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) )
67		muldvds1	⊢ ( ( 3 ∈ ℤ ∧ 3 ∈ ℤ ∧ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ∈ ℤ ) → ( ( 3 · 3 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) → 3 ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) )
68	1 1 59 67	mp3an12i	⊢ ( 𝑘 ∈ ℕ0 → ( ( 3 · 3 ) ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) → 3 ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) )
69	66 68	mpd	⊢ ( 𝑘 ∈ ℕ0 → 3 ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) )
70	9 69	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 3 ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) )
71	11 58	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ∈ ℤ )
72		dvdsmultr2	⊢ ( ( 3 ∈ ℤ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℤ ∧ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ∈ ℤ ) → ( 3 ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) → 3 ∥ ( ( 𝐹 ‘ 𝑘 ) · ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) ) )
73	1 5 71 72	mp3an2i	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 3 ∥ ( ( ; 1 0 ↑ 𝑘 ) − 1 ) → 3 ∥ ( ( 𝐹 ‘ 𝑘 ) · ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) ) )
74	70 73	mpd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 3 ∥ ( ( 𝐹 ‘ 𝑘 ) · ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) )
75	5	zcnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
76	11	zcnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ; 1 0 ↑ 𝑘 ) ∈ ℂ )
77	75 76	muls1d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑘 ) · ( ( ; 1 0 ↑ 𝑘 ) − 1 ) ) = ( ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − ( 𝐹 ‘ 𝑘 ) ) )
78	74 77	breqtrd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 3 ∥ ( ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − ( 𝐹 ‘ 𝑘 ) ) )
79	3 2 15 78	fsumdvds	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → 3 ∥ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − ( 𝐹 ‘ 𝑘 ) ) )
80	12	zcnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) ∈ ℂ )
81	3 80 75	fsumsub	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − ( 𝐹 ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )
82	79 81	breqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → 3 ∥ ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )
83		dvdssub2	⊢ ( ( ( 3 ∈ ℤ ∧ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) ∈ ℤ ∧ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℤ ) ∧ 3 ∥ ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) − Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) → ( 3 ∥ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) ↔ 3 ∥ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )
84	2 13 14 82 83	syl31anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ ℤ ) → ( 3 ∥ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ 𝑘 ) · ( ; 1 0 ↑ 𝑘 ) ) ↔ 3 ∥ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )