let n be non empty Nat; :: thesis: for i being Integer
for j being Nat st 1 <= j & j <= n holds
(2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j
let i be Integer; :: thesis: for j being Nat st 1 <= j & j <= n holds
(2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j
let j be Nat; :: thesis: ( 1 <= j & j <= n implies (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j )
assume that
A1: 1 <= j and
A2: j <= n ; :: thesis: (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j
A3: j in Seg n by A1, A2, FINSEQ_1:3;
n <= n + 1 by NAT_1:11;
then j <= n + 1 by A2, XXREAL_0:2;
then A4: j in Seg (n + 1) by A1, FINSEQ_1:3;
set N = abs ((2 to_power (MajP n,(abs i))) + i);
set M = abs ((2 to_power (MajP (n + 1),(abs i))) + i);
A5: ( i < 0 implies ((abs ((2 to_power (MajP (n + 1),(abs i))) + i)) div (2 to_power (j -' 1))) mod 2 = ((abs ((2 to_power (MajP n,(abs i))) + i)) div (2 to_power (j -' 1))) mod 2 )

proof

MajP (n + 1),(abs i) >= MajP n,(abs i) by Th22, NAT_1:11;
then consider m being Nat such that
A6: MajP (n + 1),(abs i) = (MajP n,(abs i)) + m by NAT_1:10;
reconsider m = m as Nat ;
set P = MajP n,(abs i);
assume A7: i < 0 ; :: thesis: ((abs ((2 to_power (MajP (n + 1),(abs i))) + i)) div (2 to_power (j -' 1))) mod 2 = ((abs ((2 to_power (MajP n,(abs i))) + i)) div (2 to_power (j -' 1))) mod 2
set Q = 2 to_power (MajP n,(abs i));
A8: ((2 to_power (MajP n,(abs i))) * (2 to_power m)) mod (2 to_power (MajP n,(abs i))) = 0 by NAT_D:13;
2 to_power (MajP (n + 1),(abs i)) >= abs i by Def1;
then 2 to_power (MajP (n + 1),(abs i)) >= - i by A7, ABSVALUE:def 1;
then (2 to_power (MajP (n + 1),(abs i))) + i >= (- i) + i by XREAL_1:8;
then abs ((2 to_power (MajP (n + 1),(abs i))) + i) = (2 to_power ((MajP n,(abs i)) + m)) + i by A6, ABSVALUE:def 1
.= ((2 to_power (MajP n,(abs i))) * (2 to_power m)) + i by POWER:32 ;
then A9: (abs ((2 to_power (MajP (n + 1),(abs i))) + i)) mod (2 to_power (MajP n,(abs i))) = ((((2 to_power (MajP n,(abs i))) * (2 to_power m)) mod (2 to_power (MajP n,(abs i)))) + (i mod (2 to_power (MajP n,(abs i))))) mod (2 to_power (MajP n,(abs i))) by INT_3:14
.= (i mod (2 to_power (MajP n,(abs i)))) mod (2 to_power (MajP n,(abs i))) by A8 ;
A10: (2 to_power (MajP n,(abs i))) mod (2 to_power (MajP n,(abs i))) = 0 by NAT_D:25;
j + (- 1) >= 1 + (- 1) by A1, XREAL_1:8;
then j -' 1 = j - 1 by XREAL_0:def 2;
then A11: j -' 1 < n by A2, XREAL_1:148, XXREAL_0:2;
MajP n,(abs i) >= n by Def1;
then A12: j -' 1 < MajP n,(abs i) by A11, XXREAL_0:2;
2 to_power (MajP n,(abs i)) >= abs i by Def1;
then 2 to_power (MajP n,(abs i)) >= - i by A7, ABSVALUE:def 1;
then (2 to_power (MajP n,(abs i))) + i >= (- i) + i by XREAL_1:8;
then abs ((2 to_power (MajP n,(abs i))) + i) = (2 to_power (MajP n,(abs i))) + i by ABSVALUE:def 1;
then (abs ((2 to_power (MajP n,(abs i))) + i)) mod (2 to_power (MajP n,(abs i))) = (((2 to_power (MajP n,(abs i))) mod (2 to_power (MajP n,(abs i)))) + (i mod (2 to_power (MajP n,(abs i))))) mod (2 to_power (MajP n,(abs i))) by INT_3:14
.= (i mod (2 to_power (MajP n,(abs i)))) mod (2 to_power (MajP n,(abs i))) by A10 ;
hence ((abs ((2 to_power (MajP (n + 1),(abs i))) + i)) div (2 to_power (j -' 1))) mod 2 = ((abs ((2 to_power (MajP n,(abs i))) + i)) div (2 to_power (j -' 1))) mod 2 by A9, A12, Lm3; :: thesis: verum

end;

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

suppose i >= 0 ; :: thesis: (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j

then reconsider i = i as Element of NAT by INT_1:16;
A13: (2sComplement n,i) /. j = (n -BinarySequence (abs i)) /. j by Def2
.= (n -BinarySequence i) /. j by ABSVALUE:def 1
.= IFEQ ((i div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A3, BINARI_3:def 1 ;
(2sComplement (n + 1),i) /. j = ((n + 1) -BinarySequence (abs i)) /. j by Def2
.= ((n + 1) -BinarySequence i) /. j by ABSVALUE:def 1
.= IFEQ ((i div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A4, BINARI_3:def 1 ;
hence (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j by A13; :: thesis: verum

end;

suppose A14: i < 0 ; :: thesis: (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j

then A15: (2sComplement n,i) /. j = (n -BinarySequence (abs ((2 to_power (MajP n,(abs i))) + i))) /. j by Def2
.= IFEQ (((abs ((2 to_power (MajP n,(abs i))) + i)) div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A3, BINARI_3:def 1 ;
(2sComplement (n + 1),i) /. j = ((n + 1) -BinarySequence (abs ((2 to_power (MajP (n + 1),(abs i))) + i))) /. j by A14, Def2
.= IFEQ (((abs ((2 to_power (MajP (n + 1),(abs i))) + i)) div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A4, BINARI_3:def 1 ;
hence (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j by A5, A14, A15; :: thesis: verum

end;

end;