We need a couple of technical results for starters. Some books would call these minor, but essential, results “lemmas.” We'll just call 'em theorems. See Proof Technique LC for more on the distinction.
The first of these technical results is interesting in that the hypothesis says something about a product of two square matrices and the conclusion then says the same thing about each individual matrix in the product. This result has an analogy in the algebra of complex numbers: suppose $\alpha,\,\beta\in\complexes$, then $\alpha\beta\neq 0$ if and only if $\alpha\neq 0$ and $\beta\neq 0$. We can view this result as suggesting that the term “nonsingular” for matrices is like the term “nonzero” for scalars. Consider too that we know singular matrices, as coefficient matrices for systems of equations, will sometimes lead to systems with no solutions, or systems with infinitely many solutions (Theorem NMUS). What do linear equations with zero look like? Consider $0x=5$, which has no solution, and $0x=0$, which has infinitely many solutions. In the algebra of scalars, zero is exceptional (meaning different, not better), and in the algebra of matrices, singular matrices are also the exception. While there is only one zero scalar, and there are infinitely many singular matrices, we will see that singular matrices are a distinct minority.
Suppose that $A$ and $B$ are square matrices of size $n$. The product $AB$ is nonsingular if and only if $A$ and $B$ are both nonsingular.
This is a powerful result in the “forward” direction, because it allows us to begin with a hypothesis that something complicated (the matrix product $AB$) has the property of being nonsingular, and we can then conclude that the simpler constituents ($A$ and $B$ individually) then also have the property of being nonsingular. If we had thought that the matrix product was an artificial construction, results like this would make us begin to think twice.
The contrapositive of this entire result is equally interesting. It says that $A$ or $B$ (or both) is a singular matrix if and only if the product $AB$ is singular. (See Proof Technique CP.)
Suppose $A$ and $B$ are square matrices of size $n$ such that $AB=I_n$. Then $BA=I_n$.
So Theorem OSIS tells us that if $A$ is nonsingular, then the matrix $B$ guaranteed by Theorem CINM will be both a “right-inverse” and a “left-inverse” for $A$, so $A$ is invertible and $\inverse{A}=B$.
So if you have a nonsingular matrix, $A$, you can use the procedure described in Theorem CINM to find an inverse for $A$. If $A$ is singular, then the procedure in Theorem CINM will fail as the first $n$ columns of $M$ will not row-reduce to the identity matrix. However, we can say a bit more. When $A$ is singular, then $A$ does not have an inverse (which is very different from saying that the procedure in Theorem CINM fails to find an inverse). This may feel like we are splitting hairs, but it is important that we do not make unfounded assumptions. These observations motivate the next theorem.
Suppose that $A$ is a square matrix. Then $A$ is nonsingular if and only if $A$ is invertible.
So for a square matrix, the properties of having an inverse and of having a trivial null space are one and the same. Cannot have one without the other.
Suppose that $A$ is a square matrix of size $n$. The following are equivalent.
In the case that $A$ is a nonsingular coefficient matrix of a system of equations, the inverse allows us to very quickly compute the unique solution, for any vector of constants.
Suppose that $A$ is nonsingular. Then the unique solution to $\linearsystem{A}{\vect{b}}$ is $\inverse{A}\vect{b}$.