> And Euler's formula comes from finding such a function and then defining it to be exp(z).
That's certainly one way, but you can also define exp via its power series (which is easily proven to be convergent everywhere). Then, all the properties of exp, as well as Euler's formula, are actual theorems, not just definitions.
It doesn’t matter which definition you pick. I e.g. had it defined axiomatically when I studied, i.e. we were given a list of properties which identify exp unambiguously and then we were given a proof of its existence. The fact that those properties were part of the definition doesn’t take away from their profoundness. The function could still just not exist. Same thing with defining by formulas. The map is not the territory.
That's certainly one way, but you can also define exp via its power series (which is easily proven to be convergent everywhere). Then, all the properties of exp, as well as Euler's formula, are actual theorems, not just definitions.