let n be non zero Nat; :: thesis: for i being Integer st i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i holds
Intval (2sComplement (n,i)) = i
let i be Integer; :: thesis: ( i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i implies Intval (2sComplement (n,i)) = i )
assume that
A1: i <= (2 to_power (n -' 1)) - 1 and
A2: - (2 to_power (n -' 1)) <= i ; :: thesis: Intval (2sComplement (n,i)) = i
A3: n >= 1 by NAT_1:14;

now :: thesis: Intval (2sComplement (n,i)) = i

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

suppose i >= 0 ; :: thesis: Intval (2sComplement (n,i)) = i

then reconsider i = i as Element of NAT by INT_1:3;
A4: 2sComplement (n,i) = n -BinarySequence |.i.| by Def2
.= n -BinarySequence i by ABSVALUE:def 1 ;
i + 1 <= ((2 to_power (n -' 1)) - 1) + 1 by A1, XREAL_1:6;
then A5: i < 2 to_power (n -' 1) by NAT_1:13;
n >= 1 by NAT_1:14;
then n - 1 >= 1 - 1 by XREAL_1:9;
then n -' 1 = n - 1 by XREAL_0:def 2;
then 2 to_power (n -' 1) < 2 to_power n by POWER:39, XREAL_1:146;
then i < 2 to_power n by A5, XXREAL_0:2;
then A6: Absval (n -BinarySequence i) = i by BINARI_3:35;
1 <= n by NAT_1:14;
then n in Seg n by FINSEQ_1:1;
then (n -BinarySequence i) /. n = IFEQ (((i div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by BINARI_3:def 1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A5, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def 8 ;
hence Intval (2sComplement (n,i)) = i by A4, A6, BINARI_2:def 3; :: thesis: verum

end;

suppose A7: i < 0 ; :: thesis: Intval (2sComplement (n,i)) = i

A8: 2 to_power n >= 2 to_power (n -' 1) by NAT_2:9, POWER:39;
then - (2 to_power n) <= - (2 to_power (n -' 1)) by XREAL_1:24;
then - (2 to_power n) <= i by A2, XXREAL_0:2;
then (- (2 to_power n)) - i <= i - i by XREAL_1:9;
then - ((2 to_power n) + i) <= 0 ;
then (2 to_power n) + i >= - 0 ;
then reconsider k = (2 to_power n) + i as Element of NAT by INT_1:3;
|.i.| = - i by A7, ABSVALUE:def 1;
then |.i.| <= - (- (2 to_power (n -' 1))) by A2, XREAL_1:24;
then MajP (n,|.i.|) = n by A8, Th24, XXREAL_0:2;
then A9: 2sComplement (n,i) = n -BinarySequence |.k.| by A7, Def2
.= n -BinarySequence k by ABSVALUE:def 1 ;
k < (2 to_power n) + 0 by A7, XREAL_1:8;
then k < (2 to_power 1) * (2 to_power (n -' 1)) by NAT_1:14, NAT_2:10;
then k < 2 * (2 to_power (n -' 1)) by POWER:25;
then A10: k < (2 to_power (n -' 1)) + (2 to_power (n -' 1)) ;
A11: (2 to_power n) + i < (2 to_power n) + 0 by A7, XREAL_1:6;
(2 to_power n) + (- (2 to_power (n -' 1))) = (2 to_power n) - (2 to_power (n -' 1))
.= ((2 to_power 1) * (2 to_power (n -' 1))) - (2 to_power (n -' 1)) by NAT_1:14, NAT_2:10
.= (2 * (2 to_power (n -' 1))) - (2 to_power (n -' 1)) by POWER:25
.= 2 to_power (n -' 1) ;
then A12: k >= 2 to_power (n -' 1) by A2, XREAL_1:6;
n in Seg n by A3, FINSEQ_1:1;
then (n -BinarySequence k) /. n = IFEQ (((k div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by BINARI_3:def 1
.= IFEQ ((1 mod 2),0,FALSE,TRUE) by A12, A10, NAT_2:20
.= IFEQ (1,0,FALSE,TRUE) by NAT_D:14
.= TRUE by FUNCOP_1:def 8 ;
then Intval (2sComplement (n,i)) = (Absval (n -BinarySequence k)) - (2 to_power n) by A9, BINARI_2:def 3
.= k - (2 to_power n) by A11, BINARI_3:35
.= 0 + i ;
hence Intval (2sComplement (n,i)) = i ; :: thesis: verum

end;

end;

end;

hence Intval (2sComplement (n,i)) = i ; :: thesis: verum