:: deftheorem defines is_expressible_by IDEA_1:def 3 :
for n, i being Nat holds
( i is_expressible_by n iff i < 2 to_power n );