Proof of A Square Real Matrix Is Invertible if and only if Its Determinant Is Nonzero

Each result cited is universally quantified over the data in its own statement. We work in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices.

A product formula. Let $A$ be invertible. By Inverse Matrix and Invertible Real Square Matrix §invertible, $A$ has exactly one inverse, denoted $A^{-1}\in\mathcal{M}_{n}(\mathbb{R})$, and $AA^{-1}=I_{n}$ by Inverse Matrix and Invertible Real Square Matrix §inverse. Hence, by The Determinant is Multiplicative §multiplicative with $A^{-1}$ in place of $B$, and by Rules for the Determinant: Rows, Scalar Multiples and the Transpose §identity,

$$\det A\cdot\det(A^{-1})=\det(AA^{-1})=\det I_{n}=1.\tag{1}$$

Clause invertible, only if. Let $A$ be invertible. If $\det A=0$, then (1) gives $1=0\cdot\det(A^{-1})=0$, which is false, since $0\neq1$ in the field $\mathbb{R}$ (Fields §field). Hence $\det A\neq0$.

Clause invertible, if. Let $\det A\neq0$, and suppose that $A$ is not invertible. Conditions Criteria for Invertibility of a Square Real Matrix §trivial-kernel and Criteria for Invertibility of a Square Real Matrix §invertible are equivalent by that theorem, and the latter fails, so the former fails: there is $x\in\mathbb{R}^{n}$ with $Ax=0$, the origin, and $x\neq0$. The transpose $A^{\top}$ lies in $\mathcal{M}_{n}(\mathbb{R})$ and $(A^{\top})_{ij}=A_{ji}$ for all $i,j\in[n]$, by Transpose of a Real Matrix §transpose. The origin is the constant map with value $0$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin, so all its components are $0$. Hence, for every $j\in[n]$, by Matrix-Vector Product §product,

$$\sum_{i=1}^{n}x_{i}(A^{\top})_{ij}=\sum_{i=1}^{n}A_{ji}x_{i}=(Ax)_{j}=0.$$

By Rules for the Determinant: Rows, Scalar Multiples and the Transpose §dependent-rows applied to $A^{\top}$ in place of $A$, $\det(A^{\top})=0$, and then $\det A=\det(A^{\top})=0$ by Rules for the Determinant: Rows, Scalar Multiples and the Transpose §transpose. This contradicts $\det A\neq0$; so $A$ is invertible.

Clause inverse. Let $A$ be invertible; then $\det A\neq0$ by clause invertible. By (1), $\det(A^{-1})$ is an element $z\in\mathbb{R}$ with $\det A\cdot z=1$; the only such $z$ is the reciprocal of $\det A$, by Negatives, Differences, Reciprocals and Quotients §reciprocal. Hence $\det(A^{-1})=(\det A)^{-1}=1/\det A$.