This is a comment I left on a blog but the comment box had no preview button and my comment came out kinda mangled, so I'm posting it here.
First of all, it's a long time since I proved anything so I may be wrong. Secondly, the markup is probably going to be terrible, there seems to be no preview button and I can't find wordpress's help section for markup. Finally, apologies if this is straying too far from the original idea of proof automation but I think this answers the question of whether this is true for Complex also. I can't really claim that this proof is discoverable by pattern matching as it's not really an epsilon-delta proof. That said, if I haven't made a mistake, the problem becomes "easy" if you consider a compactification of R and maybe looking at compactifications is a reasonable strategy for theorem provers.
Anyway, I think you can capture all of the fiddly parts and the proof-by-contradiction inside the Heine-Borel Theorem instead of using the Baire Category Theorem, which seems to be a bit more heavy-weight.
The essence is to show that for any δ > 0, there is a single Nδ such that |f(nX)| < δ for X ∈ [0,1] and n > Nδ. The conclusion follows from the fact that any Real > Nδ is something in [0,1] times an integer at least as big as N and therefore |f| will be < δ for this Real too.
Let X ∈ Real. We are given that f(nX) -> 0 as n -> ∞. More formally, ∀ δ > 0, ∀ X ∈ Real, ∃ Nδ,X ∈ Natural such that |f(nX)| < δ ∀ n > Nδ,X. Since f(X) is continuous there is an open set, Oδ,X containing X such that |f(Nδ,X y)| < δ ∀ y ∈ Oδ,X (it is the inverse image of (-δ, δ)).
For a fixed δ, {Oδ,X: X ∈ [0,1]} gives us an open cover of [0,1] and Heine-Borel tells us that there is a finite subcover. This means we have a finite set of Oδ,X, each with an Nδ,X and we can take the maximum Nδ,X and call it Nδ. This is a Natural such that |f(nX)| < δ ∀ X ∈ [0,1], ∀ n > Nδ.
Now let X ∈ Real, X > Nδ. Let N = [X]+1, where [] is the greatest integer function and let θ = X/N. Note that θ ∈ [0,1] and N > Nδ. So |f(Nθ)| < δ. That is, |f(X)| < δ.
So all you need is the compactness of [0,1] and the fact that you can generate all of Real+ from [0,1] and multiplication by Natural. So it seems that is true for Complex or RealN etc. where you take x -> ∞ to mean |x| -> ∞ and you use [-1,1] instead of [0,1].
If Real itself was compact you could skip the scaling step entirely. I think rephrasing the question in terms of Real ∪ {-∞, ∞} makes it almost trivial but I must admit I'm going beyond what I can remember from my student days, I expect someone will tell me that rephrasing it like that causes something else to break.
I think it would be reasonable for a theorem prover to start by choosing a δ to aim for and use continuity to construct the cover of Real from the inverse images of (-δ, -δ). It would get stuck then and I don't know whether there is a reasonable automated bridge to the solution from there.
