let n be Nat; ( 3 divides n iff 3 divides Sum (digits (n,10)) )
consider p being XFinSequence of NAT such that
A1:
dom p = dom (digits (n,10))
and
A2:
for i being Nat st i in dom p holds
p . i = ((digits (n,10)) . i) * (10 |^ i)
and
A3:
value ((digits (n,10)),10) = Sum p
by Def1;
reconsider dop = dom p as Element of NAT by ORDINAL1:def 12;
defpred S1[ set , set ] means $2 = (p . $1) mod 3;
A4:
for k being Nat st k in Segm dop holds
ex x being Element of NAT st S1[k,x]
;
consider p9 being XFinSequence of NAT such that
A5:
( dom p9 = Segm dop & ( for k being Nat st k in Segm dop holds
S1[k,p9 . k] ) )
from STIRL2_1:sch 5(A4);
A6:
now for i being Nat st i in dom p holds
p9 . i = ((digits (n,10)) . i) mod 3let i be
Nat;
( i in dom p implies p9 . i = ((digits (n,10)) . i) mod 3 )reconsider dz =
(10 |^ i) - 1 as
Nat by NAT_1:20, NEWTON:83;
reconsider dz =
dz as
Element of
NAT by ORDINAL1:def 12;
( 3
divides 3
* 3 & 9
divides dz )
by Th6, NAT_D:def 3;
then
3
divides dz
by NAT_D:4;
then
3
divides ((digits (n,10)) . i) * dz
by NAT_D:9;
then A7:
(((digits (n,10)) . i) * dz) mod 3
= 0
by PEPIN:6;
assume A8:
i in dom p
;
p9 . i = ((digits (n,10)) . i) mod 3hence p9 . i =
(p . i) mod 3
by A5
.=
(((digits (n,10)) . i) * (dz + 1)) mod 3
by A2, A8
.=
((((digits (n,10)) . i) * dz) + ((digits (n,10)) . i)) mod 3
.=
(0 + ((digits (n,10)) . i)) mod 3
by A7, NAT_D:22
.=
((digits (n,10)) . i) mod 3
;
verum end;
thus
( 3 divides n implies 3 divides Sum (digits (n,10)) )
( 3 divides Sum (digits (n,10)) implies 3 divides n )
assume
3 divides Sum (digits (n,10))
; 3 divides n
then
(Sum (digits (n,10))) mod 3 = 0
by PEPIN:6;
then
(Sum p9) mod 3 = 0
by A1, A5, A6, Th3;
then
(Sum p) mod 3 = 0
by A5, Th3;
then
3 divides Sum p
by PEPIN:6;
hence
3 divides n
by A3, Th5; verum