let x be Integer; :: thesis: for k being Nat st 2 <= k holds
SDSub_Add_Carry x,k in k -SD_Sub_S
let k be Nat; :: thesis: ( 2 <= k implies SDSub_Add_Carry x,k in k -SD_Sub_S )
A1: SDSub_Add_Carry x,k <= 1 by Th13;
assume k >= 2 ; :: thesis: SDSub_Add_Carry x,k in k -SD_Sub_S
then k > 1 by XXREAL_0:2;
then k - 1 > 1 - 1 by XREAL_1:16;
then A2: k -' 1 > 0 by XREAL_0:def 2;
then 2 to_power (k -' 1) > 1 by POWER:40;
then A3: - (Radix (k -' 1)) <= - 1 by XREAL_1:26;
- 1 <= SDSub_Add_Carry x,k by Th13;
then A4: SDSub_Add_Carry x,k >= - (Radix (k -' 1)) by A3, XXREAL_0:2;
(Radix (k -' 1)) - 1 >= 1 by A2, INT_1:79, POWER:40;
then A5: SDSub_Add_Carry x,k <= (Radix (k -' 1)) - 1 by A1, XXREAL_0:2;
SDSub_Add_Carry x,k is Element of INT by INT_1:def 2;
hence SDSub_Add_Carry x,k in k -SD_Sub_S by A5, A4; :: thesis: verum