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 )

hence b divides n by A3, Th5; :: thesis: verum

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

assume A24:
(digits (n,b)) . 0 = 0
; :: thesis: b divides n
A4:
len (digits (n,b)) >= 1
by A3, Th4;

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;

end;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 A4, XXREAL_0:1;

end;

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 A9, AFINSQ_1:86;

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 A10, NEWTON:4;

end;A11: 0 in dom (digits (n,b)) by A9, AFINSQ_1:86;

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 A10, NEWTON:4;

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 S_{1}[ Nat, set ] means $2 = d . ($1 + 1);

ex x being Element of NAT st S_{1}[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

S_{1}[x,d9 . x] ) )
from STIRL2_1:sch 5(A15);

then A19: (Sum d9) mod B = 0 by A3, PEPIN:6;

dom d = k + 1 by A6

.= (len <%(d . 0)%>) + (len d9) by A16, AFINSQ_1:33 ;

then d = <%(d . 0)%> ^ d9 by A14, A20, AFINSQ_1:def 3;

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 A3, A5, PEPIN:6;

then (d . 0) mod b = 0 by A19, NAT_D:17;

then B divides d . 0 by A3, PEPIN:6;

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;

end;defpred S

A14: now :: thesis: for l being Nat st l in dom <%(d . 0)%> holds

d . l = <%(d . 0)%> . l

A15:
for u being Nat st u in Segm k 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;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

ex x being Element of NAT st S

consider d9 being XFinSequence of NAT such that

A16: ( dom d9 = Segm k & ( for x being Nat st x in Segm k holds

S

now :: thesis: for i being Nat st i in dom d9 holds

b divides d9 . i

then
b divides Sum d9
by Th2;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 A16, NAT_1:44;

then i + 1 < k + 1 by XREAL_1:8, A16;

then A18: i + 1 in dom d by A6, AFINSQ_1:86;

d9 . i = d . (i + 1) by A16, A17

.= ((digits (n,b)) . (i + 1)) * (b |^ (i + 1)) by A7, A18

.= ((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;assume A17: i in dom d9 ; :: thesis: b divides d9 . i

then i < len d9 by A16, NAT_1:44;

then i + 1 < k + 1 by XREAL_1:8, A16;

then A18: i + 1 in dom d by A6, AFINSQ_1:86;

d9 . i = d . (i + 1) by A16, A17

.= ((digits (n,b)) . (i + 1)) * (b |^ (i + 1)) by A7, A18

.= ((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

then A19: (Sum d9) mod B = 0 by A3, PEPIN:6;

A20: now :: thesis: for l being Nat st l in dom d9 holds

d . ((len <%(d . 0)%>) + l) = d9 . l

A22:
0 in dom (digits (n,b))
by A13, AFINSQ_1:86;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 A16, A21; :: thesis: verum

end;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 A16, A21; :: thesis: verum

dom d = k + 1 by A6

.= (len <%(d . 0)%>) + (len d9) by A16, AFINSQ_1:33 ;

then d = <%(d . 0)%> ^ d9 by A14, A20, AFINSQ_1:def 3;

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 A3, A5, PEPIN:6;

then (d . 0) mod b = 0 by A19, NAT_D:17;

then B divides d . 0 by A3, PEPIN:6;

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;

now :: thesis: for i being Nat st i in dom d holds

b divides d . i

then
b divides value ((digits (n,b)),b)
by A2, Th2;b divides d . i

let i be Nat; :: thesis: ( i in dom d implies b divides d . b_{1} )

assume A25: i in dom d ; :: thesis: b divides d . b_{1}

end;assume A25: i in dom d ; :: thesis: b divides d . b

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

end;

suppose
i = 0
; :: thesis: b divides d . b_{1}

then d . i =
((digits (n,b)) . 0) * (b |^ 0)
by A1, A25

.= ((digits (n,b)) . 0) * 1 by NEWTON:4 ;

hence b divides d . i by A24, NAT_D:6; :: thesis: verum

end;.= ((digits (n,b)) . 0) * 1 by NEWTON:4 ;

hence b divides d . i by A24, NAT_D:6; :: thesis: verum

suppose
i > 0
; :: thesis: b divides d . b_{1}

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;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

hence b divides n by A3, Th5; :: thesis: verum