let n, b be Nat; :: thesis: ( b > 1 implies ( b divides n iff (digits n,b) . 0 = 0 ) )
reconsider B = b as Element of NAT by ORDINAL1:def 13;
assume A1: b > 1 ; :: thesis: ( b divides n iff (digits n,b) . 0 = 0 )
thus ( b divides n implies (digits n,b) . 0 = 0 ) :: thesis: ( (digits n,b) . 0 = 0 implies b divides n )

proof

assume A2: b divides n ; :: thesis: (digits n,b) . 0 = 0
consider d being XFinSequence of such that
A3: ( dom d = dom (digits n,b) & ( for i being Nat st i in dom d holds
d . i = ((digits n,b) . i) * (b |^ i) ) & value (digits n,b),b = Sum d ) by Def1;
A4: len (digits n,b) >= 1 by A1, Th7;

per cases ( len (digits n,b) = 1 or len (digits n,b) > 1 ) by A4, XXREAL_0:1;

suppose A5: len (digits n,b) = 1 ; :: thesis: (digits n,b) . 0 = 0

then A6: 0 in dom (digits n,b) by NAT_1:45;
len d = 1 by A5, A3;
then d = <%(d . 0 )%> by AFINSQ_1:38;
then A7: Sum d = d . 0 by STIRL2_1:44
.= ((digits n,b) . 0 ) * (b |^ 0 ) by A3, A6 ;
b divides Sum d by A1, A2, A3, Th8;
then A8: b divides ((digits n,b) . 0 ) * 1 by A7, NEWTON:9;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: (digits n,b) . 0 = 0

then digits n,b = <%0 %> by A1, Def2;
hence (digits n,b) . 0 = 0 by AFINSQ_1:38; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (digits n,b) . 0 = 0

then (digits n,b) . 0 < b by A1, A6, Def2;
then (digits n,b) . 0 <= 0 by A8, NAT_D:7;
hence (digits n,b) . 0 = 0 ; :: thesis: verum

end;

end;

end;

suppose A9: len (digits n,b) > 1 ; :: thesis: (digits n,b) . 0 = 0

then reconsider k = (len (digits n,b)) - 1 as Element of NAT by NAT_1:21;
A10: 0 in dom (digits n,b) by A9, NAT_1:45;
defpred S₁[ Element of NAT , set ] means $2 = d . ($1 + 1);
A11: for u being Element of NAT st u in k holds
ex x being Element of NAT st S₁[u,x] ;
consider d' being XFinSequence of such that
A12: ( dom d' = k & ( for x being Element of NAT st x in k holds
S₁[x,d' . x] ) ) from STIRL2_1:sch 6(A11);

now

let i be Nat; :: thesis: ( i in dom d' implies b divides d' . i )
assume A13: i in dom d' ; :: thesis: b divides d' . i
then i < k by A12, NAT_1:45;
then i + 1 < k + 1 by XREAL_1:10;
then A14: i + 1 in dom d by A3, NAT_1:45;
d' . i = d . (i + 1) by A12, A13
.= ((digits n,b) . (i + 1)) * (b |^ (i + 1)) by A3, A14
.= ((digits n,b) . (i + 1)) * ((b |^ i) * b) by NEWTON:11
.= b * (((digits n,b) . (i + 1)) * (b |^ i)) ;
hence b divides d' . i by NAT_D:def 3; :: thesis: verum

end;

then b divides Sum d' by Th5;
then A15: (Sum d') mod B = 0 by A1, PEPIN:6;
A16: dom d = k + 1 by A3
.= (len <%(d . 0 )%>) + (len d') by A12, AFINSQ_1:36 ;

A17: now

let l be Element of NAT ; :: thesis: ( l in dom <%(d . 0 )%> implies d . l = <%(d . 0 )%> . l )
assume l in dom <%(d . 0 )%> ; :: thesis: d . l = <%(d . 0 )%> . l
then l in 1 by AFINSQ_1:def 5;
then l < 1 by NAT_1:45;
then l = 0 by NAT_1:14;
hence d . l = <%(d . 0 )%> . l by AFINSQ_1:38; :: thesis: verum

end;

now

let l be Element of NAT ; :: thesis: ( l in dom d' implies d . ((len <%(d . 0 )%>) + l) = d' . l )
assume A18: l in dom d' ; :: thesis: d . ((len <%(d . 0 )%>) + l) = d' . l
(len <%(d . 0 )%>) + l = l + 1 by AFINSQ_1:38;
hence d . ((len <%(d . 0 )%>) + l) = d' . l by A12, A18; :: thesis: verum

end;

then d = <%(d . 0 )%> ^ d' by A16, A17, AFINSQ_1:def 4;
then Sum d = (Sum <%(d . 0 )%>) + (Sum d') by Th1;
then n = (Sum <%(d . 0 )%>) + (Sum d') by A1, A3, Th8;
then n = (d . 0 ) + (Sum d') by STIRL2_1:44;
then ((d . 0 ) + (Sum d')) mod B = 0 by A1, A2, PEPIN:6;
then (d . 0 ) mod b = 0 by A15, NAT_D:17;
then B divides d . 0 by A1, PEPIN:6;
then b divides ((digits n,b) . 0 ) * (b |^ 0 ) by A3, A10;
then A19: b divides ((digits n,b) . 0 ) * 1 by NEWTON:9;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: (digits n,b) . 0 = 0

then digits n,b = <%0 %> by A1, Def2;
hence (digits n,b) . 0 = 0 by AFINSQ_1:38; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (digits n,b) . 0 = 0

then (digits n,b) . 0 < b by A1, A10, Def2;
then (digits n,b) . 0 <= 0 by A19, NAT_D:7;
hence (digits n,b) . 0 = 0 ; :: thesis: verum

end;

end;

end;

end;

end;

assume A20: (digits n,b) . 0 = 0 ; :: thesis: b divides n
consider d being XFinSequence of such that
A21: ( dom d = dom (digits n,b) & ( for i being Nat st i in dom d holds
d . i = ((digits n,b) . i) * (b |^ i) ) & value (digits n,b),b = Sum d ) by Def1;

now

let i be Nat; :: thesis: ( i in dom d implies b divides d . b₁ )
assume A22: i in dom d ; :: thesis: b divides d . b₁

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: b divides d . b₁

then d . i = ((digits n,b) . 0 ) * (b |^ 0 ) by A21, A22
.= ((digits n,b) . 0 ) * 1 by NEWTON:9 ;
hence b divides d . i by A20, NAT_D:6; :: thesis: verum

end;

suppose i > 0 ; :: thesis: b divides d . b₁

then consider j being Nat such that
A23: j + 1 = i by NAT_1:6;
d . i = ((digits n,b) . i) * (b |^ (j + 1)) by A21, A22, A23
.= ((digits n,b) . i) * ((b |^ j) * b) by NEWTON:11
.= b * (((digits n,b) . i) * (b |^ j)) ;
hence b divides d . i by NAT_D:def 3; :: thesis: verum

end;

end;

end;

then b divides value (digits n,b),b by A21, Th5;
hence b divides n by A1, Th8; :: thesis: verum