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 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
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 ;
reconsider dz = dz as Element of NAT by ORDINAL1:def 12;
( 3 divides 3 * 3 & 9 divides dz ) by ;
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
.= ((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 ;
then (Sum p) mod 3 = 0 by PEPIN:6;
then (Sum p9) mod 3 = 0 by ;
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 ;
then 3 divides Sum p by PEPIN:6;
hence 3 divides n by ; :: thesis: verum