Metamath Proof Explorer

Table of Contents - 14.3.5. Logarithms to an arbitrary base

Define "log using an arbitrary base" function and then prove some of its properties. Note that is generalized to an arbitrary base and arbitrary parameter in , but it doesn't accept infinities as arguments, unlike .

Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log".

There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): where is the base and is the argument of the logarithm function. An alternative would be to support the notational form ; that looks a little more like traditional notation. Such a function for a fixed base can be obtained in Metamath (without the need for a new definition) by the curry function: , see logbmpt, logbf and logbfval.

  1. clogb
  2. df-logb
  3. logbval
  4. logbcl
  5. logbid1
  6. logb1
  7. elogb
  8. logbchbase
  9. relogbval
  10. relogbcl
  11. relogbzcl
  12. relogbreexp
  13. relogbzexp
  14. relogbmul
  15. relogbmulexp
  16. relogbdiv
  17. relogbexp
  18. nnlogbexp
  19. logbrec
  20. logbleb
  21. logblt
  22. relogbcxp
  23. cxplogb
  24. relogbcxpb
  25. logbmpt
  26. logbf
  27. logbfval
  28. relogbf
  29. logblog
  30. logbgt0b
  31. logbgcd1irr
  32. 2logb9irr
  33. logbprmirr
  34. 2logb3irr
  35. 2logb9irrALT
  36. sqrt2cxp2logb9e3
  37. 2irrexpqALT