let n be Nat; :: thesis: ( n >= 1 implies for m, k being Nat st m in Seg n & k >= 2 holds
SDDec (FSDMin n,m,k) = 1 )
assume A1: n >= 1 ; :: thesis: for m, k being Nat st m in Seg n & k >= 2 holds
SDDec (FSDMin n,m,k) = 1
let m, k be Nat; :: thesis: ( m in Seg n & k >= 2 implies SDDec (FSDMin n,m,k) = 1 )
assume that
A2: m in Seg n and
A3: k >= 2 ; :: thesis: SDDec (FSDMin n,m,k) = 1
for i being Nat holds
( not i in Seg n or ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) )

proof

let i be Nat; :: thesis: ( not i in Seg n or ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) )
assume A4: i in Seg n ; :: thesis: ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) )
then A5: i >= 1 by FINSEQ_1:3;

now

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

suppose A6: i > m ; :: thesis: ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) )

A7: DigA (Fmin n,m,k),i = FminDigit m,k,i by A4, RADIX_5:def 6
.= 0 by A3, A6, RADIX_5:def 5 ;
A8: DigA (SDMin n,m,k),i = SDMinDigit m,k,i by A4, RADIX_5:def 2
.= 0 by A3, A6, RADIX_5:def 1 ;
DigA (FSDMin n,m,k),i = FSDMinDigit m,k,i by A4, Def11
.= 0 by A3, A6, Def10 ;
hence ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) ) by A8, A7; :: thesis: verum

end;

suppose A9: i <= m ; :: thesis: ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) )

now

per cases ( i = m or i < m ) by A9, XXREAL_0:1;

suppose A10: i = m ; :: thesis: ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) )

A11: DigA (Fmin n,m,k),i = FminDigit m,k,i by A4, RADIX_5:def 6
.= 1 by A3, A10, RADIX_5:def 5 ;
A12: DigA (SDMin n,m,k),i = SDMinDigit m,k,i by A4, RADIX_5:def 2
.= 0 by A3, A10, RADIX_5:def 1 ;
DigA (FSDMin n,m,k),i = FSDMinDigit m,k,i by A4, Def11
.= 1 by A3, A10, Def10 ;
hence ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) ) by A12, A11; :: thesis: verum

end;

suppose A13: i < m ; :: thesis: ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) )

A14: DigA (Fmin n,m,k),i = FminDigit m,k,i by A4, RADIX_5:def 6
.= 0 by A3, A13, RADIX_5:def 5 ;
A15: DigA (SDMin n,m,k),i = SDMinDigit m,k,i by A4, RADIX_5:def 2
.= (- (Radix k)) + 1 by A3, A5, A13, RADIX_5:def 1 ;
DigA (FSDMin n,m,k),i = FSDMinDigit m,k,i by A4, Def11
.= (- (Radix k)) + 1 by A3, A13, Def10 ;
hence ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) ) by A15, A14; :: thesis: verum

end;

end;

end;

hence ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( DigA (FSDMin n,m,k),i = DigA (Fmin n,m,k),i & DigA (SDMin n,m,k),i = 0 ) or ( DigA (FSDMin n,m,k),i = DigA (SDMin n,m,k),i & DigA (Fmin n,m,k),i = 0 ) ) ; :: thesis: verum

end;

then (SDDec (FSDMin n,m,k)) + (SDDec (DecSD 0 ,n,k)) = (SDDec (Fmin n,m,k)) + (SDDec (SDMin n,m,k)) by A1, A3, RADIX_5:15;
then (SDDec (FSDMin n,m,k)) + 0 = (SDDec (Fmin n,m,k)) + (SDDec (SDMin n,m,k)) by A1, RADIX_5:6
.= ((SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k))) + (SDDec (SDMin n,m,k)) by A1, A2, A3, RADIX_5:18
.= ((SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k))) + (SDDec (DecSD 1,n,k))
.= (SDDec (DecSD 0 ,n,k)) + (SDDec (DecSD 1,n,k)) by A1, A3, RADIX_5:17
.= 0 + (SDDec (DecSD 1,n,k)) by A1, RADIX_5:6 ;
hence SDDec (FSDMin n,m,k) = 1 by A1, A3, RADIX_5:9; :: thesis: verum