For this entire argument I will be operating under the assumption that ¬Con(ZFC) is independent of ZFC.
ZFC+¬Con(ZFC) proves "there EXISTS a natural number x such that x is an encoding of a proof in ZFC of 0=1".
Now suppose there is actually a numeral n, i.e. a specific written term written using symbols, e.g. (+,*,1), such that
ZFC+¬Con(ZFC) proves that "n is an encoding of a proof in ZFC of 0=1". We can mechanically decode such a n and check if it is indeed a proof that that ZFC proves "0=1" or not.
There are two possibilities: (a) the check is successful and thus we have found proof of a contradiction in ZFC. But if ZFC is inconsistent, then it proves everything. In particular ZFC proves ¬Con(ZFC), which violates our assumption that ¬Con(ZFC) is independent of ZFC.
Alternatively (b) our check fails and n does not encode a proof in ZFC of 0=1. But that statement "n does not encode a proof in ZFC of 0=1" is a true Delta_0 statement, and we can prove by induction that ZFC proves every true Delta_0 statement. Thus we can prove that ZFC proves "n does not encode a proof 0=1", and hence ZFC+¬Con(ZFC) proves "n does not encode a proof 0=1". But now we have found a statement Q such that ZFC+¬Con(ZFC) proves both Q and also ¬Q. This means that ZFC+¬Con(ZFC) is inconsistent. But if ZFC+¬Con(ZFC) is inconsistent, by the deduction theorem, ZFC proves ¬¬Con(ZFC), or equivalently ZFC proves Con(ZFC). This contradicts our assumption that ¬Con(ZFC) is independent of ZFC (it also implies that ZFC is inconsistent).
Thus we are left with the conclusion that there is no such numeral n. However it is still the case that ZFC+¬Con(ZFC) proves "there EXISTS a natural number x such that x is an encoding of a proof in ZFC of 0=1", and the only way this can be the case is any such x is a "natural number" which has no numeral that denotes it.