Metamath Proof Explorer


Table of Contents - 20.43.22.8. 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