let f, m, k be Nat; :: thesis: ( m >= 1 & k >= 2 & f needs_digits_of m,k implies f >= SDDec (Fmin ((m + 2),m,k)) )
assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k ; :: thesis: f >= SDDec (Fmin ((m + 2),m,k))
for i being Nat st i in Seg m holds
DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
proof
let i be Nat; :: thesis: ( i in Seg m implies DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) )
assume A4: i in Seg m ; :: thesis: DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
then A5: i <= m by FINSEQ_1:1;
now :: thesis: DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
per cases ( i = m or i < m ) by A5, XXREAL_0:1;
suppose A6: i = m ; :: thesis: DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
then DigA ((DecSD (f,m,k)),i) > 0 by A1, A3, Th6;
then A7: DigA ((DecSD (f,m,k)),i) >= 0 + 1 by INT_1:7;
DigA ((Fmin (m,m,k)),i) = FminDigit (m,k,i) by A4, RADIX_5:def 6
.= 1 by A2, A6, RADIX_5:def 5 ;
hence DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) by A7; :: thesis: verum
end;
suppose A8: i < m ; :: thesis: DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
DigA ((Fmin (m,m,k)),i) = FminDigit (m,k,i) by A4, RADIX_5:def 6
.= 0 by A2, A8, RADIX_5:def 5 ;
hence DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) by A4, Th5; :: thesis: verum
end;
end;
end;
hence DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) ; :: thesis: verum
end;
then SDDec (DecSD (f,m,k)) >= SDDec (Fmin (m,m,k)) by A1, RADIX_5:13;
then A9: SDDec (DecSD (f,m,k)) >= SDDec (Fmin ((m + 2),m,k)) by A1, A2, Th1;
f < (Radix k) |^ m by A3;
then f is_represented_by m,k by RADIX_1:def 12;
hence f >= SDDec (Fmin ((m + 2),m,k)) by A1, A9, RADIX_1:22; :: thesis: verum