let n be non zero Nat; for h, i being Integer st h >= 0 & i >= 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement (n,h) = 2sComplement (n,i)
let h, i be Integer; ( h >= 0 & i >= 0 & h mod (2 to_power n) = i mod (2 to_power n) implies 2sComplement (n,h) = 2sComplement (n,i) )
assume that
A1:
( h >= 0 & i >= 0 )
and
A2:
h mod (2 to_power n) = i mod (2 to_power n)
; 2sComplement (n,h) = 2sComplement (n,i)
A3:
for j being Nat st j in Seg n holds
(n -BinarySequence |.h.|) . j = (n -BinarySequence |.i.|) . j
proof
A4:
(
|.h.| = h &
|.i.| = i )
by A1, ABSVALUE:def 1;
let j be
Nat;
( j in Seg n implies (n -BinarySequence |.h.|) . j = (n -BinarySequence |.i.|) . j )
assume A5:
j in Seg n
;
(n -BinarySequence |.h.|) . j = (n -BinarySequence |.i.|) . j
reconsider j =
j as
Nat ;
A6:
j <= n
by A5, FINSEQ_1:1;
A7:
1
<= j
by A5, FINSEQ_1:1;
then
j - 1
>= 1
- 1
by XREAL_1:9;
then
j -' 1
= j - 1
by XREAL_0:def 2;
then A8:
j -' 1
< n
by A6, XREAL_1:146, XXREAL_0:2;
len (n -BinarySequence |.i.|) = n
by CARD_1:def 7;
then A9:
(n -BinarySequence |.i.|) . j =
(n -BinarySequence |.i.|) /. j
by A7, A6, FINSEQ_4:15
.=
IFEQ (
((|.i.| div (2 to_power (j -' 1))) mod 2),
0,
FALSE,
TRUE)
by A5, BINARI_3:def 1
;
len (n -BinarySequence |.h.|) = n
by CARD_1:def 7;
then (n -BinarySequence |.h.|) . j =
(n -BinarySequence |.h.|) /. j
by A7, A6, FINSEQ_4:15
.=
IFEQ (
((|.h.| div (2 to_power (j -' 1))) mod 2),
0,
FALSE,
TRUE)
by A5, BINARI_3:def 1
.=
IFEQ (
((|.i.| div (2 to_power (j -' 1))) mod 2),
0,
FALSE,
TRUE)
by A2, A8, A4, Lm3
;
hence
(n -BinarySequence |.h.|) . j = (n -BinarySequence |.i.|) . j
by A9;
verum
end;
( 2sComplement (n,h) = n -BinarySequence |.h.| & 2sComplement (n,i) = n -BinarySequence |.i.| )
by A1, Def2;
hence
2sComplement (n,h) = 2sComplement (n,i)
by A3, FINSEQ_2:119; verum