let n be non zero Nat; for k being Nat st 2 to_power n <= k & k < 2 to_power (n + 1) holds
((n + 1) -BinarySequence k) . (n + 1) = TRUE
let k be Nat; ( 2 to_power n <= k & k < 2 to_power (n + 1) implies ((n + 1) -BinarySequence k) . (n + 1) = TRUE )
assume that
A1:
2 to_power n <= k
and
A2:
k < 2 to_power (n + 1)
; ((n + 1) -BinarySequence k) . (n + 1) = TRUE
k < (2 to_power n) * (2 to_power 1)
by A2, POWER:27;
then
k < 2 * (2 to_power n)
by POWER:25;
then A3:
k < (2 to_power n) + (2 to_power n)
;
(n + 1) -' 1 =
(n + 1) - 1
by NAT_D:37
.=
n
;
then A4: (k div (2 to_power ((n + 1) -' 1))) mod 2 =
1 mod 2
by A1, A3, NAT_2:20
.=
1
by NAT_D:24
;
A5:
n + 1 in Seg (n + 1)
by FINSEQ_1:4;
then
n + 1 in Seg (len ((n + 1) -BinarySequence k))
by CARD_1:def 7;
then
n + 1 in dom ((n + 1) -BinarySequence k)
by FINSEQ_1:def 3;
hence ((n + 1) -BinarySequence k) . (n + 1) =
((n + 1) -BinarySequence k) /. (n + 1)
by PARTFUN1:def 6
.=
IFEQ (((k div (2 to_power ((n + 1) -' 1))) mod 2),0,FALSE,TRUE)
by A5, Def1
.=
TRUE
by A4, FUNCOP_1:def 8
;
verum