Oh, I feel silly—of course it’s enough. Real closedness is equivalent to intermediate value theorem for polynomials, so if you have “first-order completeness” you can just do the usual proof of intermediate value theorem, just for polynomials. (Because after all the topology on R can be described in terms of its order structure, which allows you to state and use continuity and such as first-order statements.)
Oh, I feel silly—of course it’s enough. Real closedness is equivalent to intermediate value theorem for polynomials, so if you have “first-order completeness” you can just do the usual proof of intermediate value theorem, just for polynomials. (Because after all the topology on R can be described in terms of its order structure, which allows you to state and use continuity and such as first-order statements.)