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_{1}[ 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_{1}[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_{1}[k,p9 . k] ) )
from STIRL2_1:sch 5(A4);

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

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

A4: for k being Nat st k in Segm dop holds

ex x being Element of NAT st S

consider p9 being XFinSequence of NAT such that

A5: ( dom p9 = Segm dop & ( for k being Nat st k in Segm dop holds

S

A6: now :: thesis: for i being Nat st i in dom p holds

p9 . i = ((digits (n,10)) . i) mod 3

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

proof

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

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