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	$⊢ (N \in ℕ_{0} \land F : (0 \dots N) ⟶ ℤ) \to (3 ∥ \sum_{k = 0}^{N} F (k) 10^{k} \leftrightarrow 3 ∥ \sum_{k = 0}^{N} F (k))$

Proof

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

Metamath Proof Explorer

Theorem 3dvds

Proof