Description: The positive integers are a subset of the complex numbers. Remark: this
could also be proven from nnssre and ax-resscn at the cost of using
more axioms. (Contributed by NM, 2-Aug-2004) Reduce dependencies on
axioms. (Revised by Steven Nguyen, 4-Oct-2022)