:: by Adam Naumowicz

::

:: Received December 31, 2006

:: Copyright (c) 2006-2016 Association of Mizar Users

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

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

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;

ex b_{1} 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_{1} = Sum d9 )

for b_{1}, b_{2} 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_{1} = 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_{2} = Sum d9 ) holds

b_{1} = b_{2}

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

ex b

( dom d9 = dom d & ( for i being Nat st i in dom d9 holds

d9 . i = (d . i) * (b |^ i) ) & b

proof end;

uniqueness for b

( dom d9 = dom d & ( for i being Nat st i in dom d9 holds

d9 . i = (d . i) * (b |^ i) ) & b

( dom d9 = dom d & ( for i being Nat st i in dom d9 holds

d9 . i = (d . i) * (b |^ i) ) & b

b

proof end;

:: deftheorem Def1 defines value NUMERAL1:def 1 :

for d being XFinSequence of NAT

for b, b_{3} being Nat holds

( b_{3} = 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_{3} = Sum d9 ) );

for d being XFinSequence of NAT

for b, b

( b

( dom d9 = dom d & ( for i being Nat st i in dom d9 holds

d9 . i = (d . i) * (b |^ i) ) & b

definition

let n, b be Nat;

assume A1: b > 1 ;

for b_{1} being XFinSequence of NAT holds verum
;

existence

( ( n <> 0 implies ex b_{1} being XFinSequence of NAT st

( value (b_{1},b) = n & b_{1} . ((len b_{1}) - 1) <> 0 & ( for i being Nat st i in dom b_{1} holds

( 0 <= b_{1} . i & b_{1} . i < b ) ) ) ) & ( not n <> 0 implies ex b_{1} being XFinSequence of NAT st b_{1} = <%0%> ) )

for b_{1}, b_{2} being XFinSequence of NAT holds

( ( n <> 0 & value (b_{1},b) = n & b_{1} . ((len b_{1}) - 1) <> 0 & ( for i being Nat st i in dom b_{1} holds

( 0 <= b_{1} . i & b_{1} . i < b ) ) & value (b_{2},b) = n & b_{2} . ((len b_{2}) - 1) <> 0 & ( for i being Nat st i in dom b_{2} holds

( 0 <= b_{2} . i & b_{2} . i < b ) ) implies b_{1} = b_{2} ) & ( not n <> 0 & b_{1} = <%0%> & b_{2} = <%0%> implies b_{1} = b_{2} ) )

end;
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 ( 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%>;

for b

existence

( ( n <> 0 implies ex b

( value (b

( 0 <= b

proof end;

uniqueness for b

( ( n <> 0 & value (b

( 0 <= b

( 0 <= b

proof end;

:: deftheorem Def2 defines digits NUMERAL1:def 2 :

for n, b being Nat st b > 1 holds

for b_{3} being XFinSequence of NAT holds

( ( n <> 0 implies ( b_{3} = digits (n,b) iff ( value (b_{3},b) = n & b_{3} . ((len b_{3}) - 1) <> 0 & ( for i being Nat st i in dom b_{3} holds

( 0 <= b_{3} . i & b_{3} . i < b ) ) ) ) ) & ( not n <> 0 implies ( b_{3} = digits (n,b) iff b_{3} = <%0%> ) ) );

for n, b being Nat st b > 1 holds

for b

( ( n <> 0 implies ( b

( 0 <= b

:: Divisibility by 3 Rule