This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic K(En) (modal logic K with global counting operators), where number constraints are coded in binary. Hitherto the tight complexity bounds (namely ExpTime-completeness) have been established only for this logic with number restrictions coded in unary. The upper bound is established by showing that K(En) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(En).