Metamath Proof Explorer

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 ffvelrn ⊢ ( ( 𝐹 : ( 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 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )