let n be non zero Nat; for z being Tuple of n, BOOLEAN st z = 0* n holds
('not' z) + (Bin1 n) = z
let z be Tuple of n, BOOLEAN ; ( z = 0* n implies ('not' z) + (Bin1 n) = z )
assume A1:
z = 0* n
; ('not' z) + (Bin1 n) = z
then A2:
add_ovfl (('not' z),(Bin1 n)) = TRUE
by Th23;
Absval (('not' z) + (Bin1 n)) =
((Absval (('not' z) + (Bin1 n))) + (2 to_power n)) - (2 to_power n)
.=
((Absval (('not' z) + (Bin1 n))) + (IFEQ ((add_ovfl (('not' z),(Bin1 n))),FALSE,0,(2 to_power n)))) - (2 to_power n)
by A2, FUNCOP_1:def 8
.=
((Absval ('not' z)) + (Absval (Bin1 n))) - (2 to_power n)
by BINARITH:21
.=
((((- (Absval z)) + (2 to_power n)) - 1) + (Absval (Bin1 n))) - (2 to_power n)
by BINARI_2:13
.=
((((- (Absval z)) + (2 to_power n)) - 1) + 1) - (2 to_power n)
by Th11
.=
- 0
by A1, Th6
.=
Absval z
by A1, Th6
;
hence
('not' z) + (Bin1 n) = z
by Th2; verum