let n be Nat; :: thesis: ( 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 S₁[ 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 S₁[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
S₁[k,p9 . k] ) ) from STIRL2_1:sch 5(A4);

A6: now :: thesis: for i being Nat st i in dom p holds
p9 . i = ((digits (n,10)) . i) mod 3

let i be Nat; :: thesis: ( 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 ; :: thesis: p9 . i = ((digits (n,10)) . i) mod 3
hence 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 ;
:: thesis: verum

end;

thus ( 3 divides n implies 3 divides Sum (digits (n,10)) ) :: thesis: ( 3 divides Sum (digits (n,10)) implies 3 divides n )

proof

assume 3 divides n ; :: thesis: 3 divides Sum (digits (n,10))
then 3 divides Sum p by A3, Th5;
then (Sum p) mod 3 = 0 by PEPIN:6;
then (Sum p9) mod 3 = 0 by A5, Th3;
then (Sum (digits (n,10))) mod 3 = 0 by A1, A5, A6, Th3;
hence 3 divides Sum (digits (n,10)) by PEPIN:6; :: thesis: verum

end;

assume 3 divides Sum (digits (n,10)) ; :: thesis: 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; :: thesis: verum