let n be non empty 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

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:16;
A4: 2sComplement n,i = n -BinarySequence (abs i) by Def2
.= n -BinarySequence i by ABSVALUE:def 1 ;
i + 1 <= ((2 to_power (n -' 1)) - 1) + 1 by A1, XREAL_1:8;
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:11;
then n -' 1 = n - 1 by XREAL_0:def 2;
then 2 to_power (n -' 1) < 2 to_power n by POWER:44, XREAL_1:148;
then i < 2 to_power n by A5, XXREAL_0:2;
then A6: Absval (n -BinarySequence i) = i by BINARI_3:36;
1 <= n by NAT_1:14;
then n in Seg n by FINSEQ_1:3;
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:11, POWER:44;
then - (2 to_power n) <= - (2 to_power (n -' 1)) by XREAL_1:26;
then - (2 to_power n) <= i by A2, XXREAL_0:2;
then (- (2 to_power n)) - i <= i - i by XREAL_1:11;
then - ((2 to_power n) + i) <= 0 ;
then (2 to_power n) + i >= - 0 by XREAL_1:26;
then reconsider k = (2 to_power n) + i as Element of NAT by INT_1:16;
abs i = - i by A7, ABSVALUE:def 1;
then abs i <= - (- (2 to_power (n -' 1))) by A2, XREAL_1:26;
then MajP n,(abs i) = n by A8, Th24, XXREAL_0:2;
then A9: 2sComplement n,i = n -BinarySequence (abs k) by A7, Def2
.= n -BinarySequence k by ABSVALUE:def 1 ;
k < (2 to_power n) + 0 by A7, XREAL_1:10;
then k < (2 to_power 1) * (2 to_power (n -' 1)) by NAT_1:14, NAT_2:12;
then k < 2 * (2 to_power (n -' 1)) by POWER:30;
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:8;
(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:12
.= (2 * (2 to_power (n -' 1))) - (2 to_power (n -' 1)) by POWER:30
.= 2 to_power (n -' 1) ;
then A12: k >= 2 to_power (n -' 1) by A2, XREAL_1:8;
n in Seg n by A3, FINSEQ_1:3;
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:22
.= 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:36
.= 0 + i ;
hence Intval (2sComplement n,i) = i ; :: thesis: verum

end;

end;

end;

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