I would appreciate to have my proof verified
Show $e^{a-b}=\frac{e^a}{e^b}$ for every $a,b \in \mathbb{C}$.
As is already known that $e^{a+b}=e^{a}e^{b}$ for every $a,b \in \mathbb{C}$, then for every $a,b \in \mathbb{C}$
$$e^a=e^z(1)=e^ae^0=e^ae^{b-b}=e^ae^be^{-b}=e^ae^{-b}e^b=e^{a-b}e^{b}.$$
Then; $e^{a-b}=\frac{e^a}{e^b}$.
I was wondering if there is something wrong with my proof? Also is there any ways to make it more formal? Alternate proofs of this statement are also apreciated. Thanks!
Here's a way that I like, given by Michael Taylor in a few of his texts: define $e^z=\sum\limits_{k=1}^\infty\frac{z^k}{k!}.$ Clearly, one gets $\frac{d}{dt} e^{at}=ae^{at},$ where $t\in\mathbb{R}$ and $z\in\mathbb{R}.$ In fact, this is the only such solution to the ODE $f'(t)=af(t),$ $f(0)=1.$ Indeed, $$\frac{d}{dt}\left(e^{-at}f(t)\right)=0$$ by the product rule, and so $e^{-at}f(t)$ is constant in $t$. Evaluation at $t=1$ yields that $e^{-at}f(t)=1$ for all $t$, and since $e^{at}$ solves the above ODE, we have $$e^{-at}e^{at}=1,$$ or $$e^{-at}=\frac{1}{e^{at}}$$ for any $t\in\mathbb{R}$ and $a\in\mathbb{C}.$ Multplying both sides by $e^{at}$ gives that $f(t)=e^{at}$ for any real $t$. Now, fix $a,b\in\mathbb{C}.$ Differentiating $e^{-at}e^{-bt}e^{(a+b)t}$ in $t$ yields $0$ identically, so this is also constant in $t$. Evaluating at $t=0$ gives $$e^{-at}e^{-bt}e^{(a+b)t}=1$$ for any $t\in\mathbb{R},$ or $$e^{(a+b)t}=e^{at}e^{bt}.$$ Evaluating at $t=1$ gives $$e^{a+b}=e^ae^b.$$ In particular, taking $b\mapsto -b$ gives your result. I like this approach since it generalizes nicely to e.g. commuting elements in a Banach algebra, using holomorphic functional calculus.