Metamath Proof Explorer


Table of Contents - 21.50.21.7. The binary logarithm

If the binary logarithm is used more often, a separate symbol/definition could be provided for it, e.g., log2 = . Then we can write "( log2 ` x )" (analogous to for the natural logarithm) instead of .

  1. fldivexpfllog2
  2. nnlog2ge0lt1
  3. logbpw2m1
  4. fllog2