It's true that it depends on the definitions of real/complex numbers. Many other things turn out to be provable from ZFC. A discussion about this, from the view

It's true that it depends on the definitions of real/complex numbers. Many other things turn out to be provable from ZFC. A discussion about this, from the viewpoint of Metamath, is here: http://us.metamath.org/mpeuni/mmcomplex.html http://us.metamath.org/mpeuni/mmcomplex.html