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 h)
by A1, Def2;
A3:
2sComplement n,i = n -BinarySequence (abs i)
by A1, Def2;
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 A4:
j in Seg n
;
:: thesis: (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j
reconsider j =
j as
Nat ;
A5:
( 1
<= j &
j <= n )
by A4, FINSEQ_1:3;
then
j - 1
>= 1
- 1
by XREAL_1:11;
then
j -' 1
= j - 1
by XREAL_0:def 2;
then A6:
j -' 1
< n
by A5, XREAL_1:148, XXREAL_0:2;
A7:
(
abs h = h &
abs i = i & 2
to_power n > 0 )
by A1, ABSVALUE:def 1, POWER:39;
A8:
(
len (n -BinarySequence (abs h)) = n &
len (n -BinarySequence (abs i)) = n )
by FINSEQ_1:def 18;
then A9:
(n -BinarySequence (abs h)) . j =
(n -BinarySequence (abs h)) /. j
by A5, FINSEQ_4:24
.=
IFEQ (((abs h) div (2 to_power (j -' 1))) mod 2),
0 ,
FALSE ,
TRUE
by A4, BINARI_3:def 1
.=
IFEQ (((abs i) div (2 to_power (j -' 1))) mod 2),
0 ,
FALSE ,
TRUE
by A1, A6, A7, Lm3
;
(n -BinarySequence (abs i)) . j =
(n -BinarySequence (abs i)) /. j
by A5, A8, FINSEQ_4:24
.=
IFEQ (((abs i) div (2 to_power (j -' 1))) mod 2),
0 ,
FALSE ,
TRUE
by A4, BINARI_3:def 1
;
hence
(n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j
by A9;
:: thesis: verum
end;
hence
2sComplement n,h = 2sComplement n,i
by A2, A3, FINSEQ_2:139; :: thesis: verum