:: by Masaaki Niimura and Yasushi Fuwa

::

:: Received November 7, 2003

:: Copyright (c) 2003-2017 Association of Mizar Users

Lm1: for m being Nat st m >= 1 holds

m + 2 > 1

proof end;

theorem Th1: :: RADIX_6:1

for n being Nat st n >= 1 holds

for m, k being Nat st m >= 1 & k >= 2 holds

SDDec (Fmin ((m + n),m,k)) = SDDec (Fmin (m,m,k))

for m, k being Nat st m >= 1 & k >= 2 holds

SDDec (Fmin ((m + n),m,k)) = SDDec (Fmin (m,m,k))

proof end;

definition

let i, m, k be Nat;

let r be Tuple of m + 2,k -SD ;

assume A1: i in Seg (m + 2) ;

coherence

( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies 0 is Element of k -SD ) )

for b_{1} being Element of k -SD holds verum
;

end;
let r be Tuple of m + 2,k -SD ;

assume A1: i in Seg (m + 2) ;

coherence

( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies 0 is Element of k -SD ) )

proof end;

consistency for b

:: deftheorem Def1 defines M0Digit RADIX_6:def 1 :

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds

( ( i >= m implies M0Digit (r,i) = r . i ) & ( not i >= m implies M0Digit (r,i) = 0 ) );

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds

( ( i >= m implies M0Digit (r,i) = r . i ) & ( not i >= m implies M0Digit (r,i) = 0 ) );

definition

let m, k be Nat;

let r be Tuple of m + 2,k -SD ;

ex b_{1} being Tuple of m + 2,k -SD st

for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = M0Digit (r,i)

for b_{1}, b_{2} being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = M0Digit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{2},i) = M0Digit (r,i) ) holds

b_{1} = b_{2}

end;
let r be Tuple of m + 2,k -SD ;

func M0 r -> Tuple of m + 2,k -SD means :Def2: :: RADIX_6:def 2

for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = M0Digit (r,i);

existence for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = M0Digit (r,i);

ex b

for i being Nat st i in Seg (m + 2) holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def2 defines M0 RADIX_6:def 2 :

for m, k being Nat

for r, b_{4} being Tuple of m + 2,k -SD holds

( b_{4} = M0 r iff for i being Nat st i in Seg (m + 2) holds

DigA (b_{4},i) = M0Digit (r,i) );

for m, k being Nat

for r, b

( b

DigA (b

definition

let i, m, k be Nat;

let r be Tuple of m + 2,k -SD ;

assume that

A1: k >= 2 and

A2: i in Seg (m + 2) ;

( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (Radix k) - 1 is Element of k -SD ) )

for b_{1} being Element of k -SD holds verum
;

end;
let r be Tuple of m + 2,k -SD ;

assume that

A1: k >= 2 and

A2: i in Seg (m + 2) ;

func MmaxDigit (r,i) -> Element of k -SD equals :Def3: :: RADIX_6:def 3

r . i if i >= m

otherwise (Radix k) - 1;

coherence r . i if i >= m

otherwise (Radix k) - 1;

( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (Radix k) - 1 is Element of k -SD ) )

proof end;

consistency for b

:: deftheorem Def3 defines MmaxDigit RADIX_6:def 3 :

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds

( ( i >= m implies MmaxDigit (r,i) = r . i ) & ( not i >= m implies MmaxDigit (r,i) = (Radix k) - 1 ) );

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds

( ( i >= m implies MmaxDigit (r,i) = r . i ) & ( not i >= m implies MmaxDigit (r,i) = (Radix k) - 1 ) );

definition

let m, k be Nat;

let r be Tuple of m + 2,k -SD ;

ex b_{1} being Tuple of m + 2,k -SD st

for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = MmaxDigit (r,i)

for b_{1}, b_{2} being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = MmaxDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{2},i) = MmaxDigit (r,i) ) holds

b_{1} = b_{2}

end;
let r be Tuple of m + 2,k -SD ;

func Mmax r -> Tuple of m + 2,k -SD means :Def4: :: RADIX_6:def 4

for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = MmaxDigit (r,i);

existence for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = MmaxDigit (r,i);

ex b

for i being Nat st i in Seg (m + 2) holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def4 defines Mmax RADIX_6:def 4 :

for m, k being Nat

for r, b_{4} being Tuple of m + 2,k -SD holds

( b_{4} = Mmax r iff for i being Nat st i in Seg (m + 2) holds

DigA (b_{4},i) = MmaxDigit (r,i) );

for m, k being Nat

for r, b

( b

DigA (b

definition

let i, m, k be Nat;

let r be Tuple of m + 2,k -SD ;

assume that

A1: k >= 2 and

A2: i in Seg (m + 2) ;

( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (- (Radix k)) + 1 is Element of k -SD ) )

for b_{1} being Element of k -SD holds verum
;

end;
let r be Tuple of m + 2,k -SD ;

assume that

A1: k >= 2 and

A2: i in Seg (m + 2) ;

func MminDigit (r,i) -> Element of k -SD equals :Def5: :: RADIX_6:def 5

r . i if i >= m

otherwise (- (Radix k)) + 1;

coherence r . i if i >= m

otherwise (- (Radix k)) + 1;

( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (- (Radix k)) + 1 is Element of k -SD ) )

proof end;

consistency for b

:: deftheorem Def5 defines MminDigit RADIX_6:def 5 :

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds

( ( i >= m implies MminDigit (r,i) = r . i ) & ( not i >= m implies MminDigit (r,i) = (- (Radix k)) + 1 ) );

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds

( ( i >= m implies MminDigit (r,i) = r . i ) & ( not i >= m implies MminDigit (r,i) = (- (Radix k)) + 1 ) );

definition

let m, k be Nat;

let r be Tuple of m + 2,k -SD ;

ex b_{1} being Tuple of m + 2,k -SD st

for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = MminDigit (r,i)

for b_{1}, b_{2} being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = MminDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{2},i) = MminDigit (r,i) ) holds

b_{1} = b_{2}

end;
let r be Tuple of m + 2,k -SD ;

func Mmin r -> Tuple of m + 2,k -SD means :Def6: :: RADIX_6:def 6

for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = MminDigit (r,i);

existence for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = MminDigit (r,i);

ex b

for i being Nat st i in Seg (m + 2) holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def6 defines Mmin RADIX_6:def 6 :

for m, k being Nat

for r, b_{4} being Tuple of m + 2,k -SD holds

( b_{4} = Mmin r iff for i being Nat st i in Seg (m + 2) holds

DigA (b_{4},i) = MminDigit (r,i) );

for m, k being Nat

for r, b

( b

DigA (b

definition

let n, k be Nat;

let x be Integer;

end;
let x be Integer;

pred x needs_digits_of n,k means :: RADIX_6:def 7

( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) );

( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) );

:: deftheorem defines needs_digits_of RADIX_6:def 7 :

for n, k being Nat

for x being Integer holds

( x needs_digits_of n,k iff ( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) ) );

for n, k being Nat

for x being Integer holds

( x needs_digits_of n,k iff ( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) ) );

theorem Th7: :: RADIX_6:7

for f, m, k being Nat st m >= 1 & k >= 2 & f needs_digits_of m,k holds

f >= SDDec (Fmin ((m + 2),m,k))

f >= SDDec (Fmin ((m + 2),m,k))

proof end;

theorem Th8: :: RADIX_6:8

for mlow, mhigh, f being Integer st mhigh < mlow + f & f > 0 holds

ex s being Integer st

( - f < mlow - (s * f) & mhigh - (s * f) < f )

ex s being Integer st

( - f < mlow - (s * f) & mhigh - (s * f) < f )

proof end;

theorem Th9: :: RADIX_6:9

for m, k being Nat st k >= 2 holds

for r being Tuple of m + 2,k -SD holds (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k)))

for r being Tuple of m + 2,k -SD holds (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k)))

proof end;

theorem Th10: :: RADIX_6:10

for m, k being Nat st m >= 1 & k >= 2 holds

for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k)))

for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k)))

proof end;

theorem Th11: :: RADIX_6:11

for m, k being Nat st k >= 2 holds

for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))

for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))

proof end;

theorem Th12: :: RADIX_6:12

for m, k being Nat

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 holds

(SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k)))

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 holds

(SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k)))

proof end;

theorem Th13: :: RADIX_6:13

for m, k being Nat st m >= 1 & k >= 2 holds

for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))

for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))

proof end;

theorem :: RADIX_6:14

for m, k, f being Nat

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds

ex s being Integer st

( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f )

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds

ex s being Integer st

( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f )

proof end;

theorem :: RADIX_6:15

for m, k, f being Nat

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds

ex s being Integer st

( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds

ex s being Integer st

( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )

proof end;

theorem :: RADIX_6:16

for m, k being Nat

for r being Tuple of m + 2,k -SD holds

( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )

for r being Tuple of m + 2,k -SD holds

( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )

proof end;

definition

let i, m, k be Nat;

let r be Tuple of m + 2,k -SD ;

assume A1: i in Seg (m + 2) ;

( ( i < m implies r . i is Element of k -SD ) & ( not i < m implies 0 is Element of k -SD ) )

for b_{1} being Element of k -SD holds verum
;

end;
let r be Tuple of m + 2,k -SD ;

assume A1: i in Seg (m + 2) ;

func MmaskDigit (r,i) -> Element of k -SD equals :Def8: :: RADIX_6:def 8

r . i if i < m

otherwise 0 ;

coherence r . i if i < m

otherwise 0 ;

( ( i < m implies r . i is Element of k -SD ) & ( not i < m implies 0 is Element of k -SD ) )

proof end;

consistency for b

:: deftheorem Def8 defines MmaskDigit RADIX_6:def 8 :

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds

( ( i < m implies MmaskDigit (r,i) = r . i ) & ( not i < m implies MmaskDigit (r,i) = 0 ) );

for i, m, k being Nat

for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds

( ( i < m implies MmaskDigit (r,i) = r . i ) & ( not i < m implies MmaskDigit (r,i) = 0 ) );

definition

let m, k be Nat;

let r be Tuple of m + 2,k -SD ;

ex b_{1} being Tuple of m + 2,k -SD st

for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = MmaskDigit (r,i)

for b_{1}, b_{2} being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{1},i) = MmaskDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds

DigA (b_{2},i) = MmaskDigit (r,i) ) holds

b_{1} = b_{2}

end;
let r be Tuple of m + 2,k -SD ;

func Mmask r -> Tuple of m + 2,k -SD means :Def9: :: RADIX_6:def 9

for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = MmaskDigit (r,i);

existence for i being Nat st i in Seg (m + 2) holds

DigA (it,i) = MmaskDigit (r,i);

ex b

for i being Nat st i in Seg (m + 2) holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def9 defines Mmask RADIX_6:def 9 :

for m, k being Nat

for r, b_{4} being Tuple of m + 2,k -SD holds

( b_{4} = Mmask r iff for i being Nat st i in Seg (m + 2) holds

DigA (b_{4},i) = MmaskDigit (r,i) );

for m, k being Nat

for r, b

( b

DigA (b

theorem Th17: :: RADIX_6:17

for m, k being Nat

for r being Tuple of m + 2,k -SD st k >= 2 holds

(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k)))

for r being Tuple of m + 2,k -SD st k >= 2 holds

(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k)))

proof end;

theorem :: RADIX_6:18

for m, k being Nat

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds

SDDec r > SDDec (M0 r)

for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds

SDDec r > SDDec (M0 r)

proof end;

definition

let i, m, k be Nat;

assume A1: k >= 2 ;

( ( i > m implies 0 is Element of k -SD ) & ( i = m implies 1 is Element of k -SD ) & ( not i > m & not i = m implies (- (Radix k)) + 1 is Element of k -SD ) )

for b_{1} being Element of k -SD st i > m & i = m holds

( b_{1} = 0 iff b_{1} = 1 )
;

end;
assume A1: k >= 2 ;

func FSDMinDigit (m,k,i) -> Element of k -SD equals :Def10: :: RADIX_6:def 10

0 if i > m

1 if i = m

otherwise (- (Radix k)) + 1;

coherence 0 if i > m

1 if i = m

otherwise (- (Radix k)) + 1;

( ( i > m implies 0 is Element of k -SD ) & ( i = m implies 1 is Element of k -SD ) & ( not i > m & not i = m implies (- (Radix k)) + 1 is Element of k -SD ) )

proof end;

consistency for b

( b

:: deftheorem Def10 defines FSDMinDigit RADIX_6:def 10 :

for i, m, k being Nat st k >= 2 holds

( ( i > m implies FSDMinDigit (m,k,i) = 0 ) & ( i = m implies FSDMinDigit (m,k,i) = 1 ) & ( not i > m & not i = m implies FSDMinDigit (m,k,i) = (- (Radix k)) + 1 ) );

for i, m, k being Nat st k >= 2 holds

( ( i > m implies FSDMinDigit (m,k,i) = 0 ) & ( i = m implies FSDMinDigit (m,k,i) = 1 ) & ( not i > m & not i = m implies FSDMinDigit (m,k,i) = (- (Radix k)) + 1 ) );

definition

let n, m, k be Nat;

ex b_{1} being Tuple of n,k -SD st

for i being Nat st i in Seg n holds

DigA (b_{1},i) = FSDMinDigit (m,k,i)

for b_{1}, b_{2} being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

DigA (b_{1},i) = FSDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds

DigA (b_{2},i) = FSDMinDigit (m,k,i) ) holds

b_{1} = b_{2}

end;
func FSDMin (n,m,k) -> Tuple of n,k -SD means :Def11: :: RADIX_6:def 11

for i being Nat st i in Seg n holds

DigA (it,i) = FSDMinDigit (m,k,i);

existence for i being Nat st i in Seg n holds

DigA (it,i) = FSDMinDigit (m,k,i);

ex b

for i being Nat st i in Seg n holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def11 defines FSDMin RADIX_6:def 11 :

for n, m, k being Nat

for b_{4} being Tuple of n,k -SD holds

( b_{4} = FSDMin (n,m,k) iff for i being Nat st i in Seg n holds

DigA (b_{4},i) = FSDMinDigit (m,k,i) );

for n, m, k being Nat

for b

( b

DigA (b

theorem Th19: :: RADIX_6:19

for n being Nat st n >= 1 holds

for m, k being Nat st m in Seg n & k >= 2 holds

SDDec (FSDMin (n,m,k)) = 1

for m, k being Nat st m in Seg n & k >= 2 holds

SDDec (FSDMin (n,m,k)) = 1

proof end;

:: deftheorem defines is_Zero_over RADIX_6:def 12 :

for n, m, k being Nat

for r being Tuple of m + 2,k -SD holds

( r is_Zero_over n iff for i being Nat st i > n holds

DigA (r,i) = 0 );

for n, m, k being Nat

for r being Tuple of m + 2,k -SD holds

( r is_Zero_over n iff for i being Nat st i > n holds

DigA (r,i) = 0 );

theorem :: RADIX_6:20

for m being Nat st m >= 1 holds

for n, k being Nat

for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 holds

SDDec (Mmask r) > 0

for n, k being Nat

for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 holds

SDDec (Mmask r) > 0

proof end;