let n be non zero 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 = |.((2 to_power (MajP (n,|.i.|))) + i).|;
set M = |.((2 to_power (MajP ((n + 1),|.i.|))) + i).|;
A5: ( i < 0 implies (|.((2 to_power (MajP ((n + 1),|.i.|))) + i).| div (2 to_power (j -' 1))) mod 2 = (|.((2 to_power (MajP (n,|.i.|))) + i).| div (2 to_power (j -' 1))) mod 2 )

proof

MajP ((n + 1),|.i.|) >= MajP (n,|.i.|) by Th22, NAT_1:11;
then consider m being Nat such that
A6: MajP ((n + 1),|.i.|) = (MajP (n,|.i.|)) + m by NAT_1:10;
reconsider m = m as Nat ;
set P = MajP (n,|.i.|);
assume A7: i < 0 ; :: thesis: (|.((2 to_power (MajP ((n + 1),|.i.|))) + i).| div (2 to_power (j -' 1))) mod 2 = (|.((2 to_power (MajP (n,|.i.|))) + i).| div (2 to_power (j -' 1))) mod 2
set Q = 2 to_power (MajP (n,|.i.|));
A8: ((2 to_power (MajP (n,|.i.|))) * (2 to_power m)) mod (2 to_power (MajP (n,|.i.|))) = 0 by NAT_D:13;
2 to_power (MajP ((n + 1),|.i.|)) >= |.i.| by Def1;
then 2 to_power (MajP ((n + 1),|.i.|)) >= - i by A7, ABSVALUE:def 1;
then (2 to_power (MajP ((n + 1),|.i.|))) + i >= (- i) + i by XREAL_1:6;
then |.((2 to_power (MajP ((n + 1),|.i.|))) + i).| = (2 to_power ((MajP (n,|.i.|)) + m)) + i by A6, ABSVALUE:def 1
.= ((2 to_power (MajP (n,|.i.|))) * (2 to_power m)) + i by POWER:27 ;
then A9: |.((2 to_power (MajP ((n + 1),|.i.|))) + i).| mod (2 to_power (MajP (n,|.i.|))) = ((((2 to_power (MajP (n,|.i.|))) * (2 to_power m)) mod (2 to_power (MajP (n,|.i.|)))) + (i mod (2 to_power (MajP (n,|.i.|))))) mod (2 to_power (MajP (n,|.i.|))) by NAT_D:66
.= (i mod (2 to_power (MajP (n,|.i.|)))) mod (2 to_power (MajP (n,|.i.|))) by A8 ;
A10: (2 to_power (MajP (n,|.i.|))) mod (2 to_power (MajP (n,|.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,|.i.|) >= n by Def1;
then A12: j -' 1 < MajP (n,|.i.|) by A11, XXREAL_0:2;
2 to_power (MajP (n,|.i.|)) >= |.i.| by Def1;
then 2 to_power (MajP (n,|.i.|)) >= - i by A7, ABSVALUE:def 1;
then (2 to_power (MajP (n,|.i.|))) + i >= (- i) + i by XREAL_1:6;
then |.((2 to_power (MajP (n,|.i.|))) + i).| = (2 to_power (MajP (n,|.i.|))) + i by ABSVALUE:def 1;
then |.((2 to_power (MajP (n,|.i.|))) + i).| mod (2 to_power (MajP (n,|.i.|))) = (((2 to_power (MajP (n,|.i.|))) mod (2 to_power (MajP (n,|.i.|)))) + (i mod (2 to_power (MajP (n,|.i.|))))) mod (2 to_power (MajP (n,|.i.|))) by NAT_D:66
.= (i mod (2 to_power (MajP (n,|.i.|)))) mod (2 to_power (MajP (n,|.i.|))) by A10 ;
hence (|.((2 to_power (MajP ((n + 1),|.i.|))) + i).| div (2 to_power (j -' 1))) mod 2 = (|.((2 to_power (MajP (n,|.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 |.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 |.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 |.((2 to_power (MajP (n,|.i.|))) + i).|) /. j by Def2
.= IFEQ (((|.((2 to_power (MajP (n,|.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 |.((2 to_power (MajP ((n + 1),|.i.|))) + i).|) /. j by A14, Def2
.= IFEQ (((|.((2 to_power (MajP ((n + 1),|.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;