Hello, I would like to define things related to logarithms: \(\ln,e\). I want to then prove facts like \(\ln(e)=1\), that \(\ln\) is the inverse of \(x\mapsto e^x\) and that the derivative of \(\ln\) is \(x\mapsto 1/x\).

Definition For \(0 < x\) we define

\[\ln(x) := \lim_{n\to \infty} n(\sqrt[n]{x}-1).\]

I should prove that this that the sequence convergence, that it is continuous and that it is diffferentiable, but I don’t feel like doing this at the moment.