Does this proof contain circular logic? I am trying to prove that $e^x$ is a solution to $f'(x)=f(x)$, and there is a point at which I am concerned that there might be circular logic.
Here's what I've got so far:
$$f'(x)=f(x)$$
$$\frac{f'(x)}{f(x)}=1$$
$$\int\frac{f'(x)}{f(x)}dx=x+c_0$$
Letting $y=f(x)$ gives
$$\int\frac{dy}{y}=x+c_0$$
Which gives $$\ln|y|=x+c_0$$
$$f(x)=c_1e^x$$
QED
The bit I'm concerned about is $\int\frac{dy}{y}=\ln|y|$.
Is there any proof of $$\int\frac{dx}{x}=\ln|x|$$ 
which doesn't use $\frac{d}{dx}e^x=e^x$?
Edit: If it wasn't clear, I am asking if there is a way that one can prove that $$\int\frac{dx}{x}=\ln|x|$$
without relying on the fact that $\frac{d}{dx}e^x=e^x$?
 A: Assuming the question you are asking is indeed that which you are trying to solve, to show that $e^x$ is a solution to $f' = f$ all you have to do is show that $\frac{d}{dx}e^x = e^x$. Which can be fairly easily done by looking at the series definition of $e^x$ term by term and differentiating.
If you're interested in investigating whether or not $ke^x$ is the only solution to $f' = f$ (which it is), then other steps are necessary.
A: Here's a way to remove the circularity.
Define $g(x) = \int_1^x dt/t$. Then
$$
g(xy) = \int_1^{xy}\frac{dt}{t} = \int_1^x\frac{dt}{t} + \int_x^{xy}\frac{dt}{t} = \int_1^x\frac{dt}{t} + \int_1^y\frac{du}{u} = g(x)+g(y)
$$
where $t = xu$ is used for the substitution. This property is unique to logarithm functions, and its base will be the number $e$ such that $g(e) = 1$. So $g(x) = \log_e(x)$, and $g^{-1}(x) = e^x$.
A: The usual proof of this is by setting $g(x)=f(x)e^{-x}$ and prove $g'=0$.
See for instance: Proof that $C\exp(x)$ is the only set of functions for which $f(x) = f'(x)$
Nevertheless your reasoning is correct, but solving the ODE this way lacks of rigour (dividing by $f(x)$ without discussing the annulation). Instead it should be used as a hint to find that solutions looks like $Ce^x$ then by CL theorem you claim their maximality and uniqueness.
See for instance LinAlgMan's answer here: https://math.stackexchange.com/a/409974/399263
A: Let's suppose we know nothing about exponential and logarithm. Now we're given the Cauchy problem
\begin{cases}
f'(x)=f(x)\\[6px]
f(0)=1
\end{cases}
Let's suppose a solution exists defined over $\mathbb{R}$. For $y\in\mathbb{R}$, define $f_y(x)=f(x+y)$. Then, differentiating with respect to $x$, $f'_y(x)=f(x+y)=f_y'(x)$ and $f_y(0)=f(y)$. If $f(y)\ne0$, we obtain that $g(x)=f_y(x)/f(y)$ is a solution of the same Cauchy problem, so we conclude that $g=f$, so that $f(x+y)=f(x)f(y)$ (at least, when $f(y)\ne0$).
Consider $Z=\{x\in\mathbb{R}:x>0, f(x)=0\}$ and assume it is not empty. Then, if $z=\inf Z$, we have by continuity that $f(z)=0$. Now $z>0$, because $f(0)=1$, so $f(z/2)\ne0$. But we have just proved that $f(z)=f(z/2+z/2)=f(z/2)^2\ne0$: a contradiction. Similarly, $f$ cannot have a negative zero. Thus $f$ is everywhere positive and strictly increasing.
In particular $f(1)>1$ and from $f(n)=f(1)^n$ we deduce that
$$
\lim_{x\to\infty}f(x)=\infty
$$
From $f(0)=f(x)f(-x)$, we get therefore that $\lim_{x\to-\infty}f(x)=0$.
The inverse function $l$ of $f$ is thus defined over $(0,\infty)$. For every $x\in(0,\infty)$, we have $f(l(x))=x$, so by differentiating,
$$
1=f'(l(x))l'(x)=f(l(x))l'(x)
$$
and so $l'(x)=1/x$. By the fundamental theorem of calculus, since $l(1)=0$,
$$
l(x)=\int_1^x\frac{1}{t}\,dt
$$
Since
$$
l(xy)=\int_1^{xy}\frac{1}{t}\,dt=\int_1^x\frac{1}{t}\,dt+\int_x^{xy}\frac{1}{t}\,dt
$$
In the second integral we can do the substitution $t=xu$, getting
$$
l(xy)=\int_1^x\frac{1}{t}\,dt+\int_1^{y}\frac{1}{u}\,du=l(x)+l(y)
$$
Now we can drop our assumption about the existence of $f$, because we can consider the function
$$
\log x=\int_1^x\frac{1}{t}\,dt
$$
which satisfies $\log(xy)=\log x+\log y$, is increasing and has
$$
\lim_{x\to0}\log x=-\infty,\qquad\lim_{x\to\infty}\log x=\infty
$$
by considering that $\log(2^n)=n\log2$ and $\log2>0$.
The inverse function $\exp$ of $\log$ is therefore a solution of our Cauchy problem.
Now it's not difficult to show that every solution of the differential equation $f'(x)=f(x)$ is of the form $f(x)=c\exp x$. Indeed, if $f$ is such a solution, then
$$
h(x)=f(x)\exp(-x)
$$
is constant, as
$$
h'(x)=f'(x)\exp(-x)-f(x)\exp(-x)=0
$$
Thus $c=f(0)$.
Can we say that $\exp x=e^x$? This is not really difficult. Note that $\log'1=1$, so
$$
1=\lim_{n\to\infty}\frac{\log(1+1/n)-\log1}{1/n}
$$
From the main property of $\log$, we get that, for integer $n$
$$
\log(x^n)=n\log x
$$
Thus we have
$$
1=\lim_{n\to\infty}\log\left(\left(1+\frac{1}{n}\right)^n\right)
$$
and, by continuity,
$$
\exp1=\lim_{n\to\infty}\left(1+\frac{1}{n}\right)^n=e
$$
For positive integer $n$, we have $\exp n=\exp(1+1+\dots+1)=(\exp 1)^n=e^n$. For negative $n$, $1=\exp(n-n)=\exp(n)\exp(-n)$, so also in this case $\exp n=e^n$.
If $p$ is an integer and $q$ is a positive integer, we have
$$
e^p=\exp p=\exp(q(p/q))=(\exp(p/q))^q
$$
and so $\exp(p/q)=e^{p/q}$. Since the functions $x\mapsto\exp x$ and $x\mapsto e^x$ coincide over the rationals, they are the same.

Actually, the functions $\exp$ and $\log$ allow to prove the existence of $q$-th roots. Let's work under the assumption we don't know them, so we don't know the existence of the functions of type $a^x$ (for $a>0$) for lack of tools.
If $a>0$, we note that $a^n=\exp(n\log a)$, so we can define $a^x=\exp(x\log a)$. By the very definition, it follows that
$$
(a^{1/n})^n=(\exp(\tfrac{1}{n}\log a))^n=\exp(n\tfrac{1}{n}\log a)=\exp\log a=a
$$
so $a^{1/n}$ is the (unique) positive real number whose $n$-th power is $a$.
By defining
$$
e=\exp1=\lim_{n\to\infty}\left(1+\frac{1}{n}\right)^n
$$
we have that $e^x=\exp x$ by definition, but also that, for a rational $p/q$ and any positive $a$,
$$
(a^{p/q})^q=a^p
$$
so our definition of the general exponential function is what we expect it to be.
A: This is one way to define the logarithmic functions.
$$\ln x= \int _1 ^x \frac{dt}{t},  \text { for  x > 0 }  $$
So with this convenience, your proof is OK.
