let m be Nat; :: thesis: ( m >= 1 implies 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 )
assume m >= 1 ; :: thesis: 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
then A1: m + 2 >= 1 by Lm1;
let n, k be Nat; :: thesis: 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
let r be Tuple of m + 2,k -SD ; :: thesis: ( k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 implies SDDec (Mmask r) > 0 )
assume that
A2: k >= 2 and
A3: n in Seg (m + 2) and
A4: Mmask r is_Zero_over n and
A5: DigA ((Mmask r),n) > 0 ; :: thesis: SDDec (Mmask r) > 0
for i being Nat st i in Seg (m + 2) holds
DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
proof
let i be Nat; :: thesis: ( i in Seg (m + 2) implies DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) )
assume A6: i in Seg (m + 2) ; :: thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
now :: thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
per cases ( i > n or i <= n ) ;
suppose A7: i > n ; :: thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
DigA ((FSDMin ((m + 2),n,k)),i) = FSDMinDigit (n,k,i) by A6, Def11
.= 0 by A2, A7, Def10 ;
hence DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) by A4, A7; :: thesis: verum
end;
suppose A8: i <= n ; :: thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
now :: thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
per cases ( i = n or i < n ) by A8, XXREAL_0:1;
suppose A9: i = n ; :: thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
then A10: DigA ((Mmask r),i) >= 0 + 1 by A5, INT_1:7;
DigA ((FSDMin ((m + 2),n,k)),i) = FSDMinDigit (n,k,i) by A6, Def11
.= 1 by A2, A9, Def10 ;
hence DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) by A10; :: thesis: verum
end;
suppose A11: i < n ; :: thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
A12: DigA ((Mmask r),i) = (Mmask r) . i by A6, RADIX_1:def 3;
A13: (Mmask r) . i is Element of k -SD by A6, RADIX_1:15;
DigA ((FSDMin ((m + 2),n,k)),i) = FSDMinDigit (n,k,i) by A6, Def11
.= (- (Radix k)) + 1 by A2, A11, Def10 ;
hence DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) by A12, A13, RADIX_1:13; :: thesis: verum
end;
end;
end;
hence DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) ; :: thesis: verum
end;
end;
end;
hence DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) ; :: thesis: verum
end;
then SDDec (Mmask r) >= SDDec (FSDMin ((m + 2),n,k)) by A1, RADIX_5:13;
hence SDDec (Mmask r) > 0 by A2, A3, A1, Th19; :: thesis: verum