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 12;
consider d being XFinSequence of NAT such that
dom d = dom (digits (n,b)) and
A1: for i being Nat st i in dom d holds
d . i = ((digits (n,b)) . i) * (b |^ i) and
A2: value ((digits (n,b)),b) = Sum d by Def1;
assume A3: 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
A4: len (digits (n,b)) >= 1 by ;
assume A5: b divides n ; :: thesis: (digits (n,b)) . 0 = 0
consider d being XFinSequence of NAT such that
A6: dom d = dom (digits (n,b)) and
A7: for i being Nat st i in dom d holds
d . i = ((digits (n,b)) . i) * (b |^ i) and
A8: value ((digits (n,b)),b) = Sum d by Def1;
per cases ( len (digits (n,b)) = 1 or len (digits (n,b)) > 1 ) by ;
suppose A9: len (digits (n,b)) = 1 ; :: thesis: (digits (n,b)) . 0 = 0
A10: b divides Sum d by A3, A5, A8, Th5;
A11: 0 in dom (digits (n,b)) by ;
len d = 1 by A6, A9;
then d = <%(d . 0)%> by AFINSQ_1:34;
then Sum d = d . 0 by AFINSQ_2:53
.= ((digits (n,b)) . 0) * (b |^ 0) by A6, A7, A11 ;
then A12: b divides ((digits (n,b)) . 0) * 1 by ;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: (digits (n,b)) . 0 = 0
then digits (n,b) = by ;
hence (digits (n,b)) . 0 = 0 ; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: (digits (n,b)) . 0 = 0
then (digits (n,b)) . 0 < b by ;
hence (digits (n,b)) . 0 = 0 by ; :: thesis: verum
end;
end;
end;
suppose A13: 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;
defpred S1[ Nat, set ] means \$2 = d . (\$1 + 1);
A14: now :: thesis: for l being Nat st l in dom <%(d . 0)%> holds
d . l = <%(d . 0)%> . l
let l be 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 Segm 1 by AFINSQ_1:def 4;
then l < 1 by NAT_1:44;
then l = 0 by NAT_1:14;
hence d . l = <%(d . 0)%> . l ; :: thesis: verum
end;
A15: for u being Nat st u in Segm k holds
ex x being Element of NAT st S1[u,x] ;
consider d9 being XFinSequence of NAT such that
A16: ( dom d9 = Segm k & ( for x being Nat st x in Segm k holds
S1[x,d9 . x] ) ) from
now :: thesis: for i being Nat st i in dom d9 holds
b divides d9 . i
let i be Nat; :: thesis: ( i in dom d9 implies b divides d9 . i )
assume A17: i in dom d9 ; :: thesis: b divides d9 . i
then i < len d9 by ;
then i + 1 < k + 1 by ;
then A18: i + 1 in dom d by ;
d9 . i = d . (i + 1) by
.= ((digits (n,b)) . (i + 1)) * (b |^ (i + 1)) by
.= ((digits (n,b)) . (i + 1)) * ((b |^ i) * b) by NEWTON:6
.= b * (((digits (n,b)) . (i + 1)) * (b |^ i)) ;
hence b divides d9 . i by NAT_D:def 3; :: thesis: verum
end;
then b divides Sum d9 by Th2;
then A19: (Sum d9) mod B = 0 by ;
A20: now :: thesis: for l being Nat st l in dom d9 holds
d . ((len <%(d . 0)%>) + l) = d9 . l
let l be Nat; :: thesis: ( l in dom d9 implies d . ((len <%(d . 0)%>) + l) = d9 . l )
A21: (len <%(d . 0)%>) + l = l + 1 by AFINSQ_1:34;
assume l in dom d9 ; :: thesis: d . ((len <%(d . 0)%>) + l) = d9 . l
hence d . ((len <%(d . 0)%>) + l) = d9 . l by ; :: thesis: verum
end;
A22: 0 in dom (digits (n,b)) by ;
dom d = k + 1 by A6
.= (len <%(d . 0)%>) + (len d9) by ;
then d = <%(d . 0)%> ^ d9 by ;
then Sum d = (Sum <%(d . 0)%>) + (Sum d9) by AFINSQ_2:55;
then n = (Sum <%(d . 0)%>) + (Sum d9) by A3, A8, Th5;
then n = (d . 0) + (Sum d9) by AFINSQ_2:53;
then ((d . 0) + (Sum d9)) mod B = 0 by ;
then (d . 0) mod b = 0 by ;
then B divides d . 0 by ;
then b divides ((digits (n,b)) . 0) * (b |^ 0) by A6, A7, A22;
then A23: b divides ((digits (n,b)) . 0) * 1 by NEWTON:4;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: (digits (n,b)) . 0 = 0
then digits (n,b) = by ;
hence (digits (n,b)) . 0 = 0 ; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: (digits (n,b)) . 0 = 0
then (digits (n,b)) . 0 < b by ;
hence (digits (n,b)) . 0 = 0 by ; :: thesis: verum
end;
end;
end;
end;
end;
assume A24: (digits (n,b)) . 0 = 0 ; :: thesis: b divides n
now :: thesis: for i being Nat st i in dom d holds
b divides d . i
let i be Nat; :: thesis: ( i in dom d implies b divides d . b1 )
assume A25: i in dom d ; :: thesis: b divides d . b1
per cases ( i = 0 or i > 0 ) ;
suppose i = 0 ; :: thesis: b divides d . b1
then d . i = ((digits (n,b)) . 0) * (b |^ 0) by
.= ((digits (n,b)) . 0) * 1 by NEWTON:4 ;
hence b divides d . i by ; :: thesis: verum
end;
suppose i > 0 ; :: thesis: b divides d . b1
then consider j being Nat such that
A26: j + 1 = i by NAT_1:6;
d . i = ((digits (n,b)) . i) * (b |^ (j + 1)) by A1, A25, A26
.= ((digits (n,b)) . i) * ((b |^ j) * b) by NEWTON:6
.= 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 ;
hence b divides n by ; :: thesis: verum