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 A1: ( 1 <= j & j <= n ) ; :: thesis: (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j
A2: j in Seg n by A1, FINSEQ_1:3;
n <= n + 1 by NAT_1:11;
then j <= n + 1 by A1, XXREAL_0:2;
then A3: j in Seg (n + 1) by A1, FINSEQ_1:3;
set M = abs ((2 to_power (MajP (n + 1),(abs i))) + i);
set N = abs ((2 to_power (MajP n,(abs i))) + i);
A4: ( 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

assume A5: 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
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);
set Q = 2 to_power (MajP n,(abs i));
2 to_power (MajP (n + 1),(abs i)) >= abs i by Def1;
then 2 to_power (MajP (n + 1),(abs i)) >= - i by A5, ABSVALUE:def 1;
then (2 to_power (MajP (n + 1),(abs i))) + i >= (- i) + i by XREAL_1:8;
then A7: 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 ;
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;
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 A7, 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;
2 to_power (MajP n,(abs i)) >= abs i by Def1;
then 2 to_power (MajP n,(abs i)) >= - i by A5, 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 A11: (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 ;
A12: MajP n,(abs i) >= n by Def1;
A13: j + (- 1) >= 1 + (- 1) by A1, XREAL_1:8;
j -' 1 = j - 1 by A13, XREAL_0:def 2;
then j -' 1 < n by A1, XREAL_1:148, XXREAL_0:2;
then j -' 1 < MajP n,(abs i) by A12, XXREAL_0:2;
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, A11, 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;
A15: (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 A3, BINARI_3:def 1 ;
(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 A2, BINARI_3:def 1 ;
hence (2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j by A15; :: thesis: verum

end;

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

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

end;

end;