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:1;

now :: 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 ) )

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 :: 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 ) )

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