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:1;
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:1;
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:6;
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:27 ;
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 NAT_D:66
.= (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:6;
then j -' 1 = j - 1 by XREAL_0:def 2;
then A11: j -' 1 < n by A2, XREAL_1:146, 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:6;
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 NAT_D:66
.= (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:3;
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;