Any consistent, recursively axiomatized theory (for example ZFC + $\neg$Con(ZFC)) can be interpreted in true arithmetic, i.e., the first-order theory consisting of all sentences true in the standard model of arithmetic (equivalently, all sentences provable in PA + $\omega$-rule). The proof is essentially the usual Henkin proof of the completeness theorem. By paying attention to the quantifier complexity of the steps in that proof, one gets that such a theory has an arithmetically definable (in fact $\Delta^0_2$) model, and that amounts to an interpretation in true arithmetic.
Your argument for the contrary conclusion confuses "$\neg$Con(ZFC) is true" (which is not the case) with "the interpretation of $\neg$Con(ZFC) is true in the Henkin model constructed above" (which is true because it's a Henkin model for the theory ZFC + $\neg$Con(ZFC)).
After writing this answer, I realized that spaceisdarkgreen already explained this in the comment thread above; if they leave an answer, I'll delete this one.
Yes, there's an issue here. What we really have is the following:
"In $\mathsf{ZFC}$ (or indeed much less$^1$), we can prove that the following are equivalent:
$\mathsf{ZFC}\not\vdash Con(\mathsf{ZFC})\rightarrow Con(\mathsf{ZFC+I})$.
$\mathsf{ZFC}\not\vdash \neg Con(\mathsf{ZFC})$.
Note that the latter is intermediate between $Con(\mathsf{ZFC})$ and $\Sigma_1$-$Sound(\mathsf{ZFC})$ (the latter of which in turn is a very weak fragment of arithmetical soundness).
The $\neg 2\rightarrow \neg 1$ direction is exactly what you've observed: if $\mathsf{ZFC}\vdash \neg Con(\mathsf{ZFC})$, then $\mathsf{ZFC}\vdash Con(\mathsf{ZFC})\rightarrow\varphi$ for every sentence $\varphi$.
Now we want to show $\neg1\rightarrow\neg 2$. This basically parallels Jech's argument. There are three steps, each of which is provable in $\mathsf{ZFC}$ (or indeed much less):
Monotonicity. Suppose $\mathsf{ZFC}\vdash Con(\mathsf{ZFC})\rightarrow Con(\mathsf{ZFC+I})$. Then a fortiori we have $\mathsf{ZFC+I}\vdash Con(\mathsf{ZFC})\rightarrow Con(\mathsf{ZFC+I})$, and so $\mathsf{ZFC+I}\vdash Con(\mathsf{ZFC+I})$.
Godel's second incompleteness theorem. From this and the previous bulletpoint we get $\neg Con(\mathsf{ZFC+I})$.
- Note - addressing one of your comments - that no additional assumption here is necessary: "if $\mathsf{ZFC+I}$ is consistent then GSIT applies and so $\mathsf{ZFC+I}$ is inconsistent" is already a deduction of $\neg Con(\mathsf{ZFC+I})$.
$\Sigma_1$-completeness. The previous bulletpoint implies $\mathsf{ZFC}\vdash\neg Con(\mathsf{ZFC+I})$. But now combining this with our original hypothesis $\neg 1$, we get $$\mathsf{ZFC}\vdash \neg Con(\mathsf{ZFC+I})\wedge[Con(\mathsf{ZFC})\rightarrow Con(\mathsf{ZFC+I})],$$ which in turn yields $$\mathsf{ZFC}\vdash\neg Con(\mathsf{ZFC})$$ as desired.
$^1$Mathematical limbo - how low can we go?
As the argument above shows, we really just need our metatheory to prove three things:
Monotonicity of $\vdash$.
Godel's second incompleteness theorem.
The $\Sigma_1$-completeness of $\mathsf{ZFC}$.
The first is basically trivial (e.g. even Robinson arithmetic does that), while this fascinating paper of Visser mentions $\mathsf{EA}$ as an upper bound for the third ($\mathsf{EA}$ is incredibly weak, as that same paper demonstrates). Meanwhile, I believe - but don't have a source for the claim - that $\mathsf{EA}$ also proves GSIT, which would make $\mathsf{EA}$ in fact a sufficient metatheory!
However, going all the way down to $\mathsf{EA}$ - if we even can - is really just showing off. For almost all purposes it's enough to observe that $I\Sigma_1$ (a weak fragment of $\mathsf{PA}$) is enough. $I\Sigma_1$ has a number of nice properties which in my opinion do make it a better stopping point than the more-famous $\mathsf{PA}$: basically, it's the weakest "natural" theory capable of "naturally" developing basic computability theory (for example, the provably total functions of $I\Sigma_1$ are exactly the primitive recursive functions). It's also finitely axiomatizable, which is sometimes quite useful. And finally, it's the first-order part of $\mathsf{RCA_0}$, meaning that a reduction to $I\Sigma_1$ fits quite nicely in the program of reverse mathematics.
Best Answer
It is quite possible that $\sf ZFC$ proves $\lnot\operatorname{Con}\sf (ZFC)$ without $\sf ZFC$ being actually inconsistent.
We know that if $\sf ZFC$ is consistent, then $\sf ZFC+\lnot\operatorname{Con}(ZFC)$ is consistent. So we can look at the following theory: $$\sf ZFC+\operatorname{Con}(ZFC+\lnot\operatorname{Con}(ZFC))+\lnot\operatorname{Con}(ZFC+\operatorname{Con}(ZFC))$$ which is just a bit stronger than $\sf ZFC$, about the same as $\sf ZFC+\operatorname{Con}(ZFC)$.
Take a universe in which this theory holds. Then $\sf ZFC$ is consistent, but there is no model of $\sf ZFC$ in which $\operatorname{Con}\sf (ZFC)$ is true. Therefore $\sf ZFC$ proves, in that universe, $\lnot\operatorname{Con}\sf (ZFC)$.
The point here is that we very much depend on the meta-theory, but there is no problem with a consistent theory proving its own inconsistency.
The key issue here, which is what bothers you, is that while it is true that a real proof translates to an arithmetic sequence coding that proof, therefore $T\vdash\varphi$ translates to the arithmetic statement corresponding to this proof; but in the other direction, if we have non-standard integers, these will encode proofs that are not "real proofs" from the [meta-]meta-theory perspective, so they are not representing "reality".
So, it's true that if there is an actual proof from $\sf ZFC$ that $0=1$, then $\lnot\operatorname{Con}\sf (ZFC)$ is true. But by assuming $\sf\operatorname{Con}(ZFC+\lnot\operatorname{Con}(ZFC))$, one is essentially assuming the existence of non-standard integers which code that proof of inconsistency, which will not correspond to an actual proof (as that would contradict the fact that a theory containing $\sf ZFC$ was assumed to be consistent in the first place!).