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 Th12;

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

then A2: k -' 1 > 0 by XREAL_0:def 2;

then 2 to_power (k -' 1) > 1 by POWER:35;

then A3: - (Radix (k -' 1)) <= - 1 by XREAL_1:24;

- 1 <= SDSub_Add_Carry (x,k) by Th12;

then A4: SDSub_Add_Carry (x,k) >= - (Radix (k -' 1)) by A3, XXREAL_0:2;

(Radix (k -' 1)) - 1 >= 1 by A2, INT_1:52, POWER:35;

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

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 Th12;

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

then A2: k -' 1 > 0 by XREAL_0:def 2;

then 2 to_power (k -' 1) > 1 by POWER:35;

then A3: - (Radix (k -' 1)) <= - 1 by XREAL_1:24;

- 1 <= SDSub_Add_Carry (x,k) by Th12;

then A4: SDSub_Add_Carry (x,k) >= - (Radix (k -' 1)) by A3, XXREAL_0:2;

(Radix (k -' 1)) - 1 >= 1 by A2, INT_1:52, POWER:35;

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