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

theorem Th1: :: NUMERAL1:1

for d, e being XFinSequence of NAT holds Sum (d ^ e) = (Sum d) + (Sum e)

proof end;

theorem Th2: :: NUMERAL1:2

for S being Real_Sequence
for d being XFinSequence of NAT
for n being Nat st d = S | (n + 1) holds
Sum d = (Partial_Sums S) . n

proof end;

theorem Th3: :: NUMERAL1:3

for k, l, m being Nat holds (k (#) (l GeoSeq )) | m is XFinSequence of NAT

proof end;

theorem Th4: :: NUMERAL1:4

for d, e being XFinSequence of NAT st len d >= 1 & len d = len e & ( for i being Nat st i in dom d holds
d . i <= e . i ) holds
Sum d <= Sum e

proof end;

theorem Th5: :: NUMERAL1:5

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 Th6: :: NUMERAL1:6

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 d' being XFinSequence of NAT st
( dom d' = dom d & ( for i being Nat st i in dom d' holds
d' . i = (d . i) * (b |^ i) ) & it = Sum d' );
existence
ex b₁ being Nat ex d' being XFinSequence of NAT st
( dom d' = dom d & ( for i being Nat st i in dom d' holds
d' . i = (d . i) * (b |^ i) ) & b₁ = Sum d' )

proof end;

uniqueness
for b₁, b₂ being Nat st ex d' being XFinSequence of NAT st
( dom d' = dom d & ( for i being Nat st i in dom d' holds
d' . i = (d . i) * (b |^ i) ) & b₁ = Sum d' ) & ex d' being XFinSequence of NAT st
( dom d' = dom d & ( for i being Nat st i in dom d' holds
d' . i = (d . i) * (b |^ i) ) & b₂ = Sum d' ) 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 d' being XFinSequence of NAT st
( dom d' = dom d & ( for i being Nat st i in dom d' holds
d' . i = (d . i) * (b |^ i) ) & b₃ = Sum d' ) );

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 = <%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 Th7: :: NUMERAL1:7

for n, b being Nat st b > 1 holds
len (digits n,b) >= 1

proof end;

theorem Th8: :: NUMERAL1:8

for n, b being Nat st b > 1 holds
value (digits n,b),b = n

proof end;

theorem Th9: :: NUMERAL1:9

for n, k being Nat st k = (10 |^ n) - 1 holds
9 divides k

proof end;

theorem :: NUMERAL1:10

for n, b being Nat st b > 1 holds
( b divides n iff (digits n,b) . 0 = 0 )

proof end;

theorem :: NUMERAL1:11

for n being Nat holds
( 2 divides n iff 2 divides (digits n,10) . 0 )

proof end;

theorem :: NUMERAL1:12

for n being Nat holds
( 3 divides n iff 3 divides Sum (digits n,10) )

proof end;

theorem :: NUMERAL1:13

for n being Nat holds
( 5 divides n iff 5 divides (digits n,10) . 0 )

proof end;