When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?
If the formula is satisfiable you cannot construct an interpolant. If the formula is unsatisfiable, you know that the final states are not reachable in at most $k$ steps. You do not know about reachability of final states in $k+1$ or more steps. 

If the formula you suggest is unsatisfiable, you can replace the sub-formula $I$ of $A$ with the interpolant and check for satisfiability. If this new formula is unsatisfiable, you know that the error state is not reachable in $k+1$ steps. Something significant just happened. We were able to determine that the final states are not reachable in $k+1$ steps using only $k$ unwindings. 

Interpolant computation can repeat until the formula is unsatisfiable, in which case you are stuck, or until a new interpolant implies the disjunction of the old interpolants. The second case is another advantage of interpolants. We use them to detect fixed points. Detecting a fixed point with just the bounded model checking formula is not easy.

A one-line intuition I once heard was: interpolation is a poor person's quantifier-elimination.