:: On the Representation of Natural Numbers in Positional Numeral Systems
::
:: Copyright (c) 2006-2021 Association of Mizar Users

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

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

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

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 )
proof end;
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
proof end;
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 & it . ((len it) - 1) <> 0 & ( for i being Nat st i in dom it holds
( 0 <= it . i & it . i < b ) ) ) if n <> 0
otherwise it = ;
consistency
for b1 being XFinSequence of NAT holds verum
;
existence
( ( n <> 0 implies ex b1 being XFinSequence of NAT st
( value (b1,b) = n & b1 . ((len b1) - 1) <> 0 & ( for i being Nat st i in dom b1 holds
( 0 <= b1 . i & b1 . i < b ) ) ) ) & ( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = ) )
proof end;
uniqueness
for b1, b2 being XFinSequence of NAT holds
( ( n <> 0 & value (b1,b) = n & b1 . ((len b1) - 1) <> 0 & ( for i being Nat st i in dom b1 holds
( 0 <= b1 . i & b1 . i < b ) ) & value (b2,b) = n & b2 . ((len b2) - 1) <> 0 & ( for i being Nat st i in dom b2 holds
( 0 <= b2 . i & b2 . i < b ) ) implies b1 = b2 ) & ( not n <> 0 & b1 = & b2 = implies b1 = b2 ) )
proof end;
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 & b3 . ((len b3) - 1) <> 0 & ( for i being Nat st i in dom b3 holds
( 0 <= b3 . i & b3 . i < b ) ) ) ) ) & ( not n <> 0 implies ( b3 = digits (n,b) iff b3 = ) ) );

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

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

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

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

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

:: Divisibility by 3 Rule
theorem :: NUMERAL1:9
for n being Nat holds
( 3 divides n iff 3 divides Sum (digits (n,10)) )
proof end;

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