:: On the Representation of Natural Numbers in Positional Numeral Systems
:: by Adam Naumowicz
::
:: Received December 31, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

theorem Th1: :: NUMERAL1:1
for k, l, m being Nat holds (k (#) (l GeoSeq)) | m is XFinSequence of NAT
proofend;

theorem Th2: :: NUMERAL1:2
for d being XFinSequence of NAT
for n being Nat st ( for i being Nat st i in dom d holds
n divides d . i ) holds
n divides Sum d
proofend;

theorem Th3: :: NUMERAL1:3
for d, e being XFinSequence of NAT
for n being Nat st dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) holds
(Sum d) mod n = (Sum e) mod n
proofend;

begin

definition
let d be XFinSequence of NAT ;
let b be Nat;
func value (d,b) ->  Nat means :Def1: :: NUMERAL1:def 1
 ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & it = Sum d9 );
existence
 ex b1 being Nat ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & b1 = Sum d9 )
proofend;
uniqueness
 for b1, b2 being Nat st ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & b1 = Sum d9 ) & ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & b2 = Sum d9 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines value NUMERAL1:def_1_:_
 for d being XFinSequence of NAT
for b, b3 being Nat holds
( b3 = value (d,b) iff ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & b3 = Sum d9 ) );

definition
let n, b be Nat;
assume A1: b > 1 ;
func digits (n,b) ->  XFinSequence of NAT  means :Def2: :: NUMERAL1:def 2
( value (it,b) = n &amp; it . ((len it) - 1) <> 0 &amp; ( for i being Nat st i in dom it holds
( 0 <= it . i &amp; it . i < b ) ) ) if n <> 0
otherwise it = <%0%>;
consistency
 for b1 being XFinSequence of NAT holds verum ;
existence
 ( ( n <> 0 implies ex b1 being XFinSequence of NAT st
( value (b1,b) = n &amp; b1 . ((len b1) - 1) <> 0 &amp; ( for i being Nat st i in dom b1 holds
( 0 <= b1 . i &amp; b1 . i < b ) ) ) ) &amp; ( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = <%0%> ) )
proofend;
uniqueness
 for b1, b2 being XFinSequence of NAT holds
( ( n <> 0 &amp; value (b1,b) = n &amp; b1 . ((len b1) - 1) <> 0 &amp; ( for i being Nat st i in dom b1 holds
( 0 <= b1 . i &amp; b1 . i < b ) ) &amp; value (b2,b) = n &amp; b2 . ((len b2) - 1) <> 0 &amp; ( for i being Nat st i in dom b2 holds
( 0 <= b2 . i &amp; b2 . i < b ) ) implies b1 = b2 ) &amp; ( not n <> 0 &amp; b1 = <%0%> &amp; b2 = <%0%> implies b1 = b2 ) )
proofend;
end;

:: deftheorem Def2 defines digits NUMERAL1:def_2_:_
 for n, b being Nat st b > 1 holds
for b3 being XFinSequence of NAT holds
( ( n <> 0 implies ( b3 = digits (n,b) iff ( value (b3,b) = n &amp; b3 . ((len b3) - 1) <> 0 &amp; ( for i being Nat st i in dom b3 holds
( 0 <= b3 . i &amp; b3 . i < b ) ) ) ) ) &amp; ( not n <> 0 implies ( b3 = digits (n,b) iff b3 = <%0%> ) ) );

theorem Th4: :: NUMERAL1:4
for n, b being Nat st b > 1 holds
len (digits (n,b)) >= 1
proofend;

theorem Th5: :: NUMERAL1:5
for n, b being Nat st b > 1 holds
value ((digits (n,b)),b) = n
proofend;

begin

theorem Th6: :: NUMERAL1:6
for n, k being Nat st k = (10 |^ n) - 1 holds
9 divides k
proofend;

theorem :: NUMERAL1:7
for n, b being Nat st b > 1 holds
( b divides n iff (digits (n,b)) . 0 = 0 )
proofend;

theorem :: NUMERAL1:8
for n being Nat holds
( 2 divides n iff 2 divides (digits (n,10)) . 0 )
proofend;

:: [WP: ] Divisibility_by_3_Rule
theorem :: NUMERAL1:9
for n being Nat holds
( 3 divides n iff 3 divides Sum (digits (n,10)) )
proofend;

theorem :: NUMERAL1:10
for n being Nat holds
( 5 divides n iff 5 divides (digits (n,10)) . 0 )
proofend;