I think this approach is the most logically "efficient". You can phrase it as defining ln(x) to be the integral of 1/t from 1 to x. Maybe not the most intuitive, though.

Interestingly, a similar approach gives the shortest proof that exp(x) and ln(x) are computable functions (since integration is a computable functional, thanks to interval arithmetic), and therefore that e = exp(1) is a computable real number.

Yeah, the hairiest part is probably the existence and uniqueness of the antiderivative, followed by the existence of an inverse for exp(1). In fact, I can't quite recall whether the book defined it as a Riemann integral or an antiderivative, but of course it had a statement of the FTC which would connect the two. (It was just a high-school textbook, so it tended to gloss over the finer points of existence and uniqueness.)