Metamath Proof Explorer


Theorem nn0cni

Description: A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022)

Ref Expression
Hypothesis nn0rei.1 A 0
Assertion nn0cni A

Proof

Step Hyp Ref Expression
1 nn0rei.1 A 0
2 nn0sscn 0
3 2 1 sselii A