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 A1: 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
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 A2: ( k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA (Mmask r),n > 0 ) ; :: thesis: SDDec (Mmask r) > 0
A3: m + 2 >= 1 by A1, Lm1;
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 A4: i in Seg (m + 2) ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

now

per cases ( i > n or i <= n ) ;

suppose A5: 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 A4, Def11
.= 0 by A2, A5, Def10 ;
hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i by A2, A5, Def12; :: thesis: verum

end;

suppose A6: i <= n ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

now

per cases ( i = n or i < n ) by A6, XXREAL_0:1;

suppose A7: i = n ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

then A8: DigA (Mmask r),i >= 0 + 1 by A2, INT_1:20;
DigA (FSDMin (m + 2),n,k),i = FSDMinDigit n,k,i by A4, Def11
.= 1 by A2, A7, Def10 ;
hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i by A8; :: thesis: verum

end;

suppose A9: i < n ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

A10: DigA (Mmask r),i = (Mmask r) . i by A4, RADIX_1:def 3;
A11: (Mmask r) . i is Element of k -SD by A4, RADIX_1:18;
DigA (FSDMin (m + 2),n,k),i = FSDMinDigit n,k,i by A4, Def11
.= (- (Radix k)) + 1 by A2, A9, Def10 ;
hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i by A10, A11, RADIX_1:15; :: 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 A3, RADIX_5:13;
hence SDDec (Mmask r) > 0 by A2, A3, Th19; :: thesis: verum