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 A1: ( i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i ) ; :: thesis: Intval (2sComplement n,i) = i
A2: 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;
A3: 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 A4: 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 A4, XXREAL_0:2;
then A5: 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 A4, 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 A3, A5, BINARI_2:def 3; :: thesis: verum

end;

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

then abs i = - i by ABSVALUE:def 1;
then A7: abs i <= - (- (2 to_power (n -' 1))) by A1, XREAL_1:26;
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 A1, 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;
MajP n,(abs i) = n by A7, A8, Th24, XXREAL_0:2;
then A9: 2sComplement n,i = n -BinarySequence (abs k) by A6, Def2
.= n -BinarySequence k by ABSVALUE:def 1 ;
A10: (2 to_power n) + i < (2 to_power n) + 0 by A6, 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 A11: k >= 2 to_power (n -' 1) by A1, XREAL_1:8;
k < (2 to_power n) + 0 by A6, 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 A12: k < (2 to_power (n -' 1)) + (2 to_power (n -' 1)) ;
n in Seg n by A2, 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 A11, A12, 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 A10, BINARI_3:36
.= 0 + i ;
hence Intval (2sComplement n,i) = i ; :: thesis: verum

end;

end;

end;

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