let m, k, f be 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 )
let r be Tuple of m + 2,k -SD ; ( m >= 1 & k >= 2 & f needs_digits_of m,k implies ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f ) )
assume that
A1:
m >= 1
and
A2:
k >= 2
and
A3:
f needs_digits_of m,k
; ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )
SDDec (Fmin ((m + 2),m,k)) <= f
by A1, A2, A3, Th7;
then A4:
(SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k))) <= (SDDec (Mmin r)) + f
by XREAL_1:7;
SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))
by A1, A2, Th13;
then A5:
SDDec (M0 r) < (SDDec (Mmin r)) + f
by A4, XXREAL_0:2;
(Radix k) |^ (m -' 1) > 0
by NEWTON:83, RADIX_2:6;
then
f > 0
by A3;
hence
ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )
by A5, Th8; verum