Here's a precise question. Does Wiles' proof of FLT run just fine in the set theory that logicians would perhaps call "Zermelo + choice" -- i.e. drop the axiom schema of replacement but assume the axiom of choice to make analysis work sensibly? [Wiles' proof needs some cyclic base change, which involves a lot of functional analysis, and one would imagine that one needs enough AC to make this stuff go through, but my question is not about AC. I am also aware that there are theorems in logic of the form "if a statement has some properties and it is provable in ZFC then it's provable in certain other systems", but my question is not about the truth or provability of FLT in Z+AC, it's about whether Wiles' proof works].

My understanding of some justifications for including replacement: without it you can't construct the ordinal $\omega+\omega$, or the cardinal $\aleph_\omega$. But I am not sure a number theorist would need such things. If you really need something with order-type $\omega+\omega$ you could just use $\{0,1\}\times\omega$ with some lexicographic ordering, and $\aleph_\omega$ itself is not something I've ever seen in a number theory paper.

Of course Wiles' proof uses a lot of commutative algebra, directly or indirectly, and I do remember a proof in Matsumura's commutative algebra book that uses induction over ordinals, but if I remember correctly the induction was only needed in situations where some module was massively infinitely-generated over some ring.

Maybe Wiles' proof of FLT is asking too much -- what about something less technical, like Gross-Zagier or some other random thing? I'm sure people realise what I'm trying to ask -- take a "standard" result in "standard" number theory -- does one need Replacement? I'm not interested in statements about things that logicians might have constructed (for example Goodstein sequences) that they may perhaps argue are "number theoretic" -- I know something about these things and they are interesting, but this question is not about them. I want to focus on standard well-known theorems in mainstream number theory from the last 50 years or whatever. Perhaps another reason to shy away from FLT is that on the face of it it uses some category theory and there was a certain amount of fuss in the 1990s about whether the proof actually was a ZFC proof [conclusion: it was, although it undoubtedly used references which talked about subtle constructions in very large categories so some rewriting would be necessary to stuff it in.]

The reason I ask is that I have it in my head (perhaps I read it in a paper by Adrian Mathias) that Bourbaki don't assume replacement in their treatise, and I remember at the time thinking "oh wow that's crazy, what an omission" but now having actually used Bourbaki as a reference for various facts in e.g. representation theory and analysis, and having begun to comprehend just how far they get and how much further they could have got, I am now wondering how important replacement is outside logic and neighboring areas.