Existence and uniqueness of solutions to a system of non-linear equations

In general this is undecidable. The tools you mention (implicit function theorem and Jacobians) are quite useful locally, especially for the case $m=n$ when the Jacobian is nonzero at most points, but unless you have good control on the behaviour of $F(x)$ as $x$ gets large it may be impossible to tell whether there is a solution somewhere "out there". For example, suppose you have a system of polynomial equations in variables $x_j$. Include the equations $\sin(\pi x_j) = 0$ and you force the variables in a solution to be integers. But there is no algorithm to decide whether a system of polynomials has integer solutions (Hilbert's 10th problem).

In the case of a polynomial system, tools of algebraic geometry (Grobner bases, characteristic sets, etc) can be used.