let n be Nat; :: thesis: ( 0 < n implies LenBSeq n = [\(log (2,n))/] + 1 )

assume 0 < n ; :: thesis: LenBSeq n = [\(log (2,n))/] + 1

then consider x being Nat such that

LCX: ( 2 to_power x <= n & n < 2 to_power (x + 1) & LenBSeq n = x + 1 ) by BINARI_6:def 1;

log (2,(2 to_power x)) = x by POWER:def 3;

then LT1: x <= log (2,n) by LCX, ASYMPT_2:7;

log (2,(2 to_power (x + 1))) = x + 1 by POWER:def 3;

then log (2,n) < x + 1 by LCX, POWER:57;

then (log (2,n)) - 1 < (x + 1) - 1 by XREAL_1:14;

hence LenBSeq n = [\(log (2,n))/] + 1 by LCX, LT1, INT_1:def 6; :: thesis: verum

assume 0 < n ; :: thesis: LenBSeq n = [\(log (2,n))/] + 1

then consider x being Nat such that

LCX: ( 2 to_power x <= n & n < 2 to_power (x + 1) & LenBSeq n = x + 1 ) by BINARI_6:def 1;

log (2,(2 to_power x)) = x by POWER:def 3;

then LT1: x <= log (2,n) by LCX, ASYMPT_2:7;

log (2,(2 to_power (x + 1))) = x + 1 by POWER:def 3;

then log (2,n) < x + 1 by LCX, POWER:57;

then (log (2,n)) - 1 < (x + 1) - 1 by XREAL_1:14;

hence LenBSeq n = [\(log (2,n))/] + 1 by LCX, LT1, INT_1:def 6; :: thesis: verum