let n be non zero Nat; for i being Integer st i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i holds
Intval (2sComplement (n,i)) = i
let i be Integer; ( i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i implies Intval (2sComplement (n,i)) = i )
assume that
A1:
i <= (2 to_power (n -' 1)) - 1
and
A2:
- (2 to_power (n -' 1)) <= i
; Intval (2sComplement (n,i)) = i
A3:
n >= 1
by NAT_1:14;
now Intval (2sComplement (n,i)) = iper cases
( i >= 0 or i < 0 )
;
suppose
i >= 0
;
Intval (2sComplement (n,i)) = ithen reconsider i =
i as
Element of
NAT by INT_1:3;
A4:
2sComplement (
n,
i) =
n -BinarySequence |.i.|
by Def2
.=
n -BinarySequence i
by ABSVALUE:def 1
;
i + 1
<= ((2 to_power (n -' 1)) - 1) + 1
by A1, XREAL_1:6;
then A5:
i < 2
to_power (n -' 1)
by NAT_1:13;
n >= 1
by NAT_1:14;
then
n - 1
>= 1
- 1
by XREAL_1:9;
then
n -' 1
= n - 1
by XREAL_0:def 2;
then
2
to_power (n -' 1) < 2
to_power n
by POWER:39, XREAL_1:146;
then
i < 2
to_power n
by A5, XXREAL_0:2;
then A6:
Absval (n -BinarySequence i) = i
by BINARI_3:35;
1
<= n
by NAT_1:14;
then
n in Seg n
by FINSEQ_1:1;
then (n -BinarySequence i) /. n =
IFEQ (
((i div (2 to_power (n -' 1))) mod 2),
0,
FALSE,
TRUE)
by BINARI_3:def 1
.=
IFEQ (
(0 mod 2),
0,
FALSE,
TRUE)
by A5, NAT_D:27
.=
IFEQ (
0,
0,
FALSE,
TRUE)
by NAT_D:26
.=
FALSE
by FUNCOP_1:def 8
;
hence
Intval (2sComplement (n,i)) = i
by A4, A6, BINARI_2:def 3;
verum end; suppose A7:
i < 0
;
Intval (2sComplement (n,i)) = iA8:
2
to_power n >= 2
to_power (n -' 1)
by NAT_2:9, POWER:39;
then
- (2 to_power n) <= - (2 to_power (n -' 1))
by XREAL_1:24;
then
- (2 to_power n) <= i
by A2, XXREAL_0:2;
then
(- (2 to_power n)) - i <= i - i
by XREAL_1:9;
then
- ((2 to_power n) + i) <= 0
;
then
(2 to_power n) + i >= - 0
;
then reconsider k =
(2 to_power n) + i as
Element of
NAT by INT_1:3;
|.i.| = - i
by A7, ABSVALUE:def 1;
then
|.i.| <= - (- (2 to_power (n -' 1)))
by A2, XREAL_1:24;
then
MajP (
n,
|.i.|)
= n
by A8, Th24, XXREAL_0:2;
then A9:
2sComplement (
n,
i) =
n -BinarySequence |.k.|
by A7, Def2
.=
n -BinarySequence k
by ABSVALUE:def 1
;
k < (2 to_power n) + 0
by A7, XREAL_1:8;
then
k < (2 to_power 1) * (2 to_power (n -' 1))
by NAT_1:14, NAT_2:10;
then
k < 2
* (2 to_power (n -' 1))
by POWER:25;
then A10:
k < (2 to_power (n -' 1)) + (2 to_power (n -' 1))
;
A11:
(2 to_power n) + i < (2 to_power n) + 0
by A7, XREAL_1:6;
(2 to_power n) + (- (2 to_power (n -' 1))) =
(2 to_power n) - (2 to_power (n -' 1))
.=
((2 to_power 1) * (2 to_power (n -' 1))) - (2 to_power (n -' 1))
by NAT_1:14, NAT_2:10
.=
(2 * (2 to_power (n -' 1))) - (2 to_power (n -' 1))
by POWER:25
.=
2
to_power (n -' 1)
;
then A12:
k >= 2
to_power (n -' 1)
by A2, XREAL_1:6;
n in Seg n
by A3, FINSEQ_1:1;
then (n -BinarySequence k) /. n =
IFEQ (
((k div (2 to_power (n -' 1))) mod 2),
0,
FALSE,
TRUE)
by BINARI_3:def 1
.=
IFEQ (
(1 mod 2),
0,
FALSE,
TRUE)
by A12, A10, NAT_2:20
.=
IFEQ (1,
0,
FALSE,
TRUE)
by NAT_D:14
.=
TRUE
by FUNCOP_1:def 8
;
then Intval (2sComplement (n,i)) =
(Absval (n -BinarySequence k)) - (2 to_power n)
by A9, BINARI_2:def 3
.=
k - (2 to_power n)
by A11, BINARI_3:35
.=
0 + i
;
hence
Intval (2sComplement (n,i)) = i
;
verum end;
hence
Intval (2sComplement (n,i)) = i
; verum