let m be non zero Nat; for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))
let z be Tuple of m, BOOLEAN ; for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))
let d be Element of BOOLEAN ; Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))
per cases
( d = FALSE or d = TRUE )
by XBOOLEAN:def 3;
suppose A1:
d = FALSE
;
Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))then
(z ^ <*d*>) /. (m + 1) = FALSE
by BINARITH:2;
then A2:
Intval (z ^ <*d*>) =
Absval (z ^ <*d*>)
by Def3
.=
(Absval z) + (IFEQ (d,FALSE,0,(2 to_power m)))
by BINARITH:20
.=
(Absval z) + 0
by A1, FUNCOP_1:def 8
.=
Absval z
;
(Absval z) - (IFEQ (d,FALSE,0,(2 to_power m))) =
(Absval z) - 0
by A1, FUNCOP_1:def 8
.=
Absval z
;
hence
Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))
by A2;
verum end; end;