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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$ and let $A\in\mathcal{M}_{n}(\mathbb{R})$ be a square real matrix, with the determinant $\det$, invertible matrices and their inverses $A^{-1}$, and reciprocals and quotients as in Commutative Rings, Fields and Ordered Fields: Standard Notation §fields.

¶ $A$ is invertible if and only if $\det A\neq0$.

¶ If $A$ is invertible, then $\det(A^{-1})=1/\det A$, where $\det A\neq0$ by clause invertible.