If a contour $C$ is parameterized by $z(t): [a, b] \to \mathbb{C}$, then we define $$ \int_C f(z) \, dz= \int_a^b f(z(t)) \, z'(t) \, dt.$$
If the contour integral on the left side is equal to some number $w$ for all contours $C$ [in some domain? all of $\mathbb{C}$?] such that $z(a) = z_1$ and $z(b) = z_2$, then we write $$ \int_{z_1}^{z_2} f(z) \, dz = \int_C f(z) \, dz.$$
But of course, this integral on the right of the first equation (if a Riemann integral) is defined in terms of the limit of sups and infs and may not exist. So we have at least two "levels" of existence to verify before the notation even makes sense.
My question however is about how one formalizes the definitions above. In logic. How do we formally express a definition whose very sensibility is conditional on some property like this? And are there any negative consequences to the fact that existence seems to be ignored or hand-waved away so readily by most undergraduate textbooks? (And perhaps grad textbooks too?) Are there edge cases that we're glossing over?
I just feel lost in a sea of hand-wavy definitions. For what it's worth, I'm currently reading Churchill and Brown's not-so-high-level Complex Variables and Applications (it's required).