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 
|- ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> ( 3 || sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) <-> 3 || sum_ k e. ( 0 ... N ) ( F ` k ) ) )

Proof

Step Hyp Ref Expression
1 3z 
 |-  3 e. ZZ
2 1 a1i 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> 3 e. ZZ )
3 fzfid 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> ( 0 ... N ) e. Fin )
4 ffvelrn 
 |-  ( ( F : ( 0 ... N ) --> ZZ /\ k e. ( 0 ... N ) ) -> ( F ` k ) e. ZZ )
5 4 adantll 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( F ` k ) e. ZZ )
6 10nn 
 |-  ; 1 0 e. NN
7 6 nnzi 
 |-  ; 1 0 e. ZZ
8 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
9 8 adantl 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
10 zexpcl 
 |-  ( ( ; 1 0 e. ZZ /\ k e. NN0 ) -> ( ; 1 0 ^ k ) e. ZZ )
11 7 9 10 sylancr 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( ; 1 0 ^ k ) e. ZZ )
12 5 11 zmulcld 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( ( F ` k ) x. ( ; 1 0 ^ k ) ) e. ZZ )
13 3 12 fsumzcl 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) e. ZZ )
14 3 5 fsumzcl 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> sum_ k e. ( 0 ... N ) ( F ` k ) e. ZZ )
15 12 5 zsubcld 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - ( F ` k ) ) e. ZZ )
16 ax-1cn 
 |-  1 e. CC
17 6 nncni 
 |-  ; 1 0 e. CC
18 16 17 negsubdi2i 
 |-  -u ( 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 e. CC
23 22 16 pncan3oi 
 |-  ( ( 9 + 1 ) - 1 ) = 9
24 18 21 23 3eqtri 
 |-  -u ( 1 - ; 1 0 ) = 9
25 3t3e9 
 |-  ( 3 x. 3 ) = 9
26 24 25 eqtr4i 
 |-  -u ( 1 - ; 1 0 ) = ( 3 x. 3 )
27 17 a1i 
 |-  ( k e. NN0 -> ; 1 0 e. CC )
28 1re 
 |-  1 e. RR
29 1lt10 
 |-  1 < ; 1 0
30 28 29 gtneii 
 |-  ; 1 0 =/= 1
31 30 a1i 
 |-  ( k e. NN0 -> ; 1 0 =/= 1 )
32 id 
 |-  ( k e. NN0 -> k e. NN0 )
33 27 31 32 geoser 
 |-  ( k e. NN0 -> sum_ j e. ( 0 ... ( k - 1 ) ) ( ; 1 0 ^ j ) = ( ( 1 - ( ; 1 0 ^ k ) ) / ( 1 - ; 1 0 ) ) )
34 fzfid 
 |-  ( k e. NN0 -> ( 0 ... ( k - 1 ) ) e. Fin )
35 elfznn0 
 |-  ( j e. ( 0 ... ( k - 1 ) ) -> j e. NN0 )
36 35 adantl 
 |-  ( ( k e. NN0 /\ j e. ( 0 ... ( k - 1 ) ) ) -> j e. NN0 )
37 zexpcl 
 |-  ( ( ; 1 0 e. ZZ /\ j e. NN0 ) -> ( ; 1 0 ^ j ) e. ZZ )
38 7 36 37 sylancr 
 |-  ( ( k e. NN0 /\ j e. ( 0 ... ( k - 1 ) ) ) -> ( ; 1 0 ^ j ) e. ZZ )
39 34 38 fsumzcl 
 |-  ( k e. NN0 -> sum_ j e. ( 0 ... ( k - 1 ) ) ( ; 1 0 ^ j ) e. ZZ )
40 33 39 eqeltrrd 
 |-  ( k e. NN0 -> ( ( 1 - ( ; 1 0 ^ k ) ) / ( 1 - ; 1 0 ) ) e. ZZ )
41 1z 
 |-  1 e. ZZ
42 zsubcl 
 |-  ( ( 1 e. ZZ /\ ; 1 0 e. ZZ ) -> ( 1 - ; 1 0 ) e. ZZ )
43 41 7 42 mp2an 
 |-  ( 1 - ; 1 0 ) e. ZZ
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 
 |-  ( k e. NN0 -> ( ; 1 0 ^ k ) e. ZZ )
49 zsubcl 
 |-  ( ( 1 e. ZZ /\ ( ; 1 0 ^ k ) e. ZZ ) -> ( 1 - ( ; 1 0 ^ k ) ) e. ZZ )
50 41 48 49 sylancr 
 |-  ( k e. NN0 -> ( 1 - ( ; 1 0 ^ k ) ) e. ZZ )
51 dvdsval2 
 |-  ( ( ( 1 - ; 1 0 ) e. ZZ /\ ( 1 - ; 1 0 ) =/= 0 /\ ( 1 - ( ; 1 0 ^ k ) ) e. ZZ ) -> ( ( 1 - ; 1 0 ) || ( 1 - ( ; 1 0 ^ k ) ) <-> ( ( 1 - ( ; 1 0 ^ k ) ) / ( 1 - ; 1 0 ) ) e. ZZ ) )
52 43 47 50 51 mp3an12i 
 |-  ( k e. NN0 -> ( ( 1 - ; 1 0 ) || ( 1 - ( ; 1 0 ^ k ) ) <-> ( ( 1 - ( ; 1 0 ^ k ) ) / ( 1 - ; 1 0 ) ) e. ZZ ) )
53 40 52 mpbird 
 |-  ( k e. NN0 -> ( 1 - ; 1 0 ) || ( 1 - ( ; 1 0 ^ k ) ) )
54 48 zcnd 
 |-  ( k e. NN0 -> ( ; 1 0 ^ k ) e. CC )
55 negsubdi2 
 |-  ( ( ( ; 1 0 ^ k ) e. CC /\ 1 e. CC ) -> -u ( ( ; 1 0 ^ k ) - 1 ) = ( 1 - ( ; 1 0 ^ k ) ) )
56 54 16 55 sylancl 
 |-  ( k e. NN0 -> -u ( ( ; 1 0 ^ k ) - 1 ) = ( 1 - ( ; 1 0 ^ k ) ) )
57 53 56 breqtrrd 
 |-  ( k e. NN0 -> ( 1 - ; 1 0 ) || -u ( ( ; 1 0 ^ k ) - 1 ) )
58 peano2zm 
 |-  ( ( ; 1 0 ^ k ) e. ZZ -> ( ( ; 1 0 ^ k ) - 1 ) e. ZZ )
59 48 58 syl 
 |-  ( k e. NN0 -> ( ( ; 1 0 ^ k ) - 1 ) e. ZZ )
60 dvdsnegb 
 |-  ( ( ( 1 - ; 1 0 ) e. ZZ /\ ( ( ; 1 0 ^ k ) - 1 ) e. ZZ ) -> ( ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) <-> ( 1 - ; 1 0 ) || -u ( ( ; 1 0 ^ k ) - 1 ) ) )
61 43 59 60 sylancr 
 |-  ( k e. NN0 -> ( ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) <-> ( 1 - ; 1 0 ) || -u ( ( ; 1 0 ^ k ) - 1 ) ) )
62 57 61 mpbird 
 |-  ( k e. NN0 -> ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) )
63 negdvdsb 
 |-  ( ( ( 1 - ; 1 0 ) e. ZZ /\ ( ( ; 1 0 ^ k ) - 1 ) e. ZZ ) -> ( ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) <-> -u ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) ) )
64 43 59 63 sylancr 
 |-  ( k e. NN0 -> ( ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) <-> -u ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) ) )
65 62 64 mpbid 
 |-  ( k e. NN0 -> -u ( 1 - ; 1 0 ) || ( ( ; 1 0 ^ k ) - 1 ) )
66 26 65 eqbrtrrid 
 |-  ( k e. NN0 -> ( 3 x. 3 ) || ( ( ; 1 0 ^ k ) - 1 ) )
67 muldvds1 
 |-  ( ( 3 e. ZZ /\ 3 e. ZZ /\ ( ( ; 1 0 ^ k ) - 1 ) e. ZZ ) -> ( ( 3 x. 3 ) || ( ( ; 1 0 ^ k ) - 1 ) -> 3 || ( ( ; 1 0 ^ k ) - 1 ) ) )
68 1 1 59 67 mp3an12i 
 |-  ( k e. NN0 -> ( ( 3 x. 3 ) || ( ( ; 1 0 ^ k ) - 1 ) -> 3 || ( ( ; 1 0 ^ k ) - 1 ) ) )
69 66 68 mpd 
 |-  ( k e. NN0 -> 3 || ( ( ; 1 0 ^ k ) - 1 ) )
70 9 69 syl 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> 3 || ( ( ; 1 0 ^ k ) - 1 ) )
71 11 58 syl 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( ( ; 1 0 ^ k ) - 1 ) e. ZZ )
72 dvdsmultr2 
 |-  ( ( 3 e. ZZ /\ ( F ` k ) e. ZZ /\ ( ( ; 1 0 ^ k ) - 1 ) e. ZZ ) -> ( 3 || ( ( ; 1 0 ^ k ) - 1 ) -> 3 || ( ( F ` k ) x. ( ( ; 1 0 ^ k ) - 1 ) ) ) )
73 1 5 71 72 mp3an2i 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( 3 || ( ( ; 1 0 ^ k ) - 1 ) -> 3 || ( ( F ` k ) x. ( ( ; 1 0 ^ k ) - 1 ) ) ) )
74 70 73 mpd 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> 3 || ( ( F ` k ) x. ( ( ; 1 0 ^ k ) - 1 ) ) )
75 5 zcnd 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( F ` k ) e. CC )
76 11 zcnd 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( ; 1 0 ^ k ) e. CC )
77 75 76 muls1d 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( ( F ` k ) x. ( ( ; 1 0 ^ k ) - 1 ) ) = ( ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - ( F ` k ) ) )
78 74 77 breqtrd 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> 3 || ( ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - ( F ` k ) ) )
79 3 2 15 78 fsumdvds 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> 3 || sum_ k e. ( 0 ... N ) ( ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - ( F ` k ) ) )
80 12 zcnd 
 |-  ( ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) /\ k e. ( 0 ... N ) ) -> ( ( F ` k ) x. ( ; 1 0 ^ k ) ) e. CC )
81 3 80 75 fsumsub 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> sum_ k e. ( 0 ... N ) ( ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - ( F ` k ) ) = ( sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - sum_ k e. ( 0 ... N ) ( F ` k ) ) )
82 79 81 breqtrd 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> 3 || ( sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - sum_ k e. ( 0 ... N ) ( F ` k ) ) )
83 dvdssub2 
 |-  ( ( ( 3 e. ZZ /\ sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) e. ZZ /\ sum_ k e. ( 0 ... N ) ( F ` k ) e. ZZ ) /\ 3 || ( sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) - sum_ k e. ( 0 ... N ) ( F ` k ) ) ) -> ( 3 || sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) <-> 3 || sum_ k e. ( 0 ... N ) ( F ` k ) ) )
84 2 13 14 82 83 syl31anc 
 |-  ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> ( 3 || sum_ k e. ( 0 ... N ) ( ( F ` k ) x. ( ; 1 0 ^ k ) ) <-> 3 || sum_ k e. ( 0 ... N ) ( F ` k ) ) )