[proofplan] Since $\det A \neq 0$, the matrix $A$ is invertible, so $Ax = b$ has a unique solution. We compute $x_j$ by expanding $\det A_j$ along column $j$. Substituting $b = Ax$ into column $j$ converts the determinant into a sum over the columns of $A$: the $j$-th column reproduces $\det A$ via cofactor expansion, while every other column produces a cross-expansion (entries from one column paired with cofactors of column $j$), which vanishes by the cofactor expansion across different columns. [/proofplan] [step:Establish existence and uniqueness of the solution] Since $\det A \neq 0$, the [Determinant Invertibility Criterion](/theorems/396) guarantees that $A$ is invertible. Therefore the system $Ax = b$ has the unique solution $x = A^{-1} b$. [/step] [step:Express $\det A_j$ by substituting $b = Ax$ into column $j$] Let $a_1, \ldots, a_n \in F^n$ denote the columns of $A$, so that $b = Ax = \sum_{\ell=1}^{n} x_\ell\, a_\ell$. The matrix $A_j$ is obtained from $A$ by replacing column $j$ with $b$: \begin{align*} A_j &= \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; b \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr]. \end{align*} Substituting $b = \sum_{\ell=1}^{n} x_\ell\, a_\ell$ and using the multilinearity of the determinant in column $j$ (by the [Properties of the Determinant](/theorems/917)): \begin{align*} \det A_j &= \det \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; \textstyle\sum_{\ell=1}^{n} x_\ell\, a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr] \\ &= \sum_{\ell=1}^{n} x_\ell \det \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr]. \end{align*} [guided] Let $a_1, \ldots, a_n \in F^n$ denote the columns of $A$. Since $Ax = b$, the vector $b$ is a linear combination of the columns: $b = \sum_{\ell=1}^{n} x_\ell\, a_\ell$. The matrix $A_j$ is formed by replacing column $j$ of $A$ with $b$: \begin{align*} A_j &= \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; b \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr]. \end{align*} The determinant is multilinear in its columns: it is linear in each column when the other columns are held fixed. This is part of the [Properties of the Determinant](/theorems/917). Applying linearity in column $j$: \begin{align*} \det A_j &= \det \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; \textstyle\sum_{\ell=1}^{n} x_\ell\, a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr] \\ &= \sum_{\ell=1}^{n} x_\ell \det \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr]. \end{align*} Each summand places column $a_\ell$ in the $j$-th position while keeping all other columns of $A$ in place. The next step is to evaluate these determinants. [/guided] [/step] [step:Identify the only surviving term via the cofactor expansion across different columns] For each $\ell$ in the sum, the matrix $[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,]$ has $a_\ell$ in column $j$ and $a_\ell$ in column $\ell$ (the original position). When $\ell \neq j$, columns $\ell$ and $j$ are identical, so by the [Properties of the Determinant](/theorems/917) the determinant is zero. When $\ell = j$, column $j$ is restored to $a_j$, and the matrix is $A$ itself. Therefore: \begin{align*} \det A_j &= \sum_{\ell=1}^{n} x_\ell \det \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr] = x_j \det A. \end{align*} [guided] We now evaluate each term in the sum \begin{align*} \det A_j &= \sum_{\ell=1}^{n} x_\ell \det \bigl[\, a_1 \;\; \cdots \;\; a_{j-1} \;\; a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,\bigr]. \end{align*} Consider the matrix $B_\ell := [\, a_1 \;\; \cdots \;\; a_{j-1} \;\; a_\ell \;\; a_{j+1} \;\; \cdots \;\; a_n \,]$. This matrix has $a_\ell$ in position $j$, while all other columns remain as in $A$. **Case $\ell = j$:** The matrix $B_j$ has $a_j$ in position $j$ — it is simply $A$ itself. So $\det B_j = \det A$. **Case $\ell \neq j$:** The matrix $B_\ell$ has $a_\ell$ in both column $\ell$ (its original position, which was not modified) and column $j$ (where we placed it). Since two columns of $B_\ell$ are identical, the [Properties of the Determinant](/theorems/917) give $\det B_\ell = 0$. Alternatively, one can see this vanishing through cofactors: expanding $\det B_\ell$ along column $j$ gives $\sum_{i=1}^{n} (a_\ell)_i\, C_{ij}(B_\ell)$. Since columns other than $j$ are unchanged, the cofactors of column $j$ in $B_\ell$ equal those in $A$: $C_{ij}(B_\ell) = C_{ij}(A)$. So the sum becomes $\sum_{i=1}^{n} A_{i\ell}\, C_{ij}(A)$, which is exactly a [Cofactor Expansion Across Different Rows](/theorems/3304) (column version) with $\ell \neq j$, and hence vanishes. Either way, only the $\ell = j$ term survives: \begin{align*} \det A_j &= x_j \det A + \sum_{\ell \neq j} x_\ell \cdot 0 = x_j \det A. \end{align*} [/guided] [/step] [step:Divide by $\det A$ to obtain Cramer's formula] Since $\det A \neq 0$, we divide both sides of $\det A_j = x_j \det A$ by $\det A$: \begin{align*} x_j &= \frac{\det A_j}{\det A}, \quad j = 1, \ldots, n. \end{align*} This holds for each $j = 1, \ldots, n$, completing the proof of Cramer's Rule. [/step]