Is there a lemma like "∃x. a^x = b" proved in Isabelle?

Question

Does anyone know where a lemma similar to

∃(x::real). a^x = (b::real)

might be found? I couldn't find something like that in the 'query', but it seems pretty handy.

Answer 1

You need a few more assumptions on a and b and you need to use the powr operator instead of ^, since ^ is only for the n-th power where n is a natural number. powr on the other hand is for any non-negative real number raised to the power of any other real number. (or similarly for complex numbers)

lemma 
  fixes a b :: real
  assumes "a > 0" "a ≠ 1" "b > 0"
  shows   "∃x. a powr x = b"
proof
  from assms show "a powr (log a b) = b" by simp
qed