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

theorem Th1: :: NUMERAL1:1

for k, l, m being Nat holds (k (#) (l GeoSeq)) | 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 b₁ 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) ) & b₁ = Sum d9 )

proof end;

uniqueness
for b₁, b₂ 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) ) & b₁ = 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) ) & b₂ = Sum d9 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines value NUMERAL1:def 1 :
for d being XFinSequence of NAT
for b, b₃ being Nat holds
( b₃ = 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) ) & b₃ = Sum d9 ) );

definition

let n, b be Nat;
assume A1: b > 1 ;

:: Unique Representation of Natural Numbers in Positional Numeral Systems

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 = <%0%>;

consistency
for b₁ being XFinSequence of NAT holds verum ;
existence
( ( n <> 0 implies ex b₁ being XFinSequence of NAT st
( value (b₁,b) = n & b₁ . ((len b₁) - 1) <> 0 & ( for i being Nat st i in dom b₁ holds
( 0 <= b₁ . i & b₁ . i < b ) ) ) ) & ( not n <> 0 implies ex b₁ being XFinSequence of NAT st b₁ = <%0%> ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of NAT holds
( ( n <> 0 & value (b₁,b) = n & b₁ . ((len b₁) - 1) <> 0 & ( for i being Nat st i in dom b₁ holds
( 0 <= b₁ . i & b₁ . i < b ) ) & value (b₂,b) = n & b₂ . ((len b₂) - 1) <> 0 & ( for i being Nat st i in dom b₂ holds
( 0 <= b₂ . i & b₂ . i < b ) ) implies b₁ = b₂ ) & ( not n <> 0 & b₁ = <%0%> & b₂ = <%0%> implies b₁ = b₂ ) )

proof end;

end;

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

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;