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