Theorem nnsscn

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)

	Ref	Expression
Assertion	nnsscn	|- NN C_ CC

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	|- 1 e. CC
2		peano2cn	|- ( x e. CC -> ( x + 1 ) e. CC )
3	2	rgen	|- A. x e. CC ( x + 1 ) e. CC
4		peano5nni	|- ( ( 1 e. CC /\ A. x e. CC ( x + 1 ) e. CC ) -> NN C_ CC )
5	1 3 4	mp2an	|- NN C_ CC