let n be non empty Nat; :: thesis: 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; :: thesis: ( h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) implies 2sComplement n,h = 2sComplement n,i )
assume A1:
( h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) )
; :: thesis: 2sComplement n,h = 2sComplement n,i
A2:
2sComplement n,h = n -BinarySequence (abs ((2 to_power (MajP n,(abs h))) + h))
by A1, Def2;
A3:
2sComplement n,i = n -BinarySequence (abs ((2 to_power (MajP n,(abs i))) + i))
by A1, Def2;
abs h = - h
by A1, ABSVALUE:def 1;
then
2 to_power (MajP n,(abs h)) >= - h
by Def1;
then
(2 to_power (MajP n,(abs h))) + h >= (- h) + h
by XREAL_1:8;
then reconsider H = (2 to_power (MajP n,(abs h))) + h as Element of NAT by INT_1:16;
abs i = - i
by A1, ABSVALUE:def 1;
then
2 to_power (MajP n,(abs i)) >= - i
by Def1;
then
(2 to_power (MajP n,(abs i))) + i >= (- i) + i
by XREAL_1:8;
then reconsider I = (2 to_power (MajP n,(abs i))) + i as Element of NAT by INT_1:16;
A4:
H mod (2 to_power n) = I mod (2 to_power n)
by A1, Lm4;
for j being Nat st j in Seg n holds
(n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j
proof
let j be
Nat;
:: thesis: ( j in Seg n implies (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j )
assume A5:
j in Seg n
;
:: thesis: (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j
A6:
( 1
<= j &
j <= n )
by A5, FINSEQ_1:3;
reconsider j =
j as
Nat ;
A7:
(
len (n -BinarySequence H) = n &
len (n -BinarySequence I) = n )
by FINSEQ_1:def 18;
j - 1
>= 1
- 1
by A6, XREAL_1:11;
then
j -' 1
= j - 1
by XREAL_0:def 2;
then A8:
j -' 1
< n
by A6, XREAL_1:148, XXREAL_0:2;
(
abs H = H &
abs I = I )
by ABSVALUE:def 1;
then (n -BinarySequence (abs H)) . j =
(n -BinarySequence H) /. j
by A6, A7, FINSEQ_4:24
.=
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 A4, A8, Lm3
.=
(n -BinarySequence I) /. j
by A5, BINARI_3:def 1
.=
(n -BinarySequence I) . j
by A6, A7, FINSEQ_4:24
;
hence
(n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j
by ABSVALUE:def 1;
:: thesis: verum
end;
hence
2sComplement n,h = 2sComplement n,i
by A2, A3, FINSEQ_2:139; :: thesis: verum