let m, k, f be Nat; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum