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	$$⊢\mathbb{N}\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		peano2cn	$$⊢x\in ℂ\to x+1\in ℂ$$
3	2	rgen	$$⊢\forall x\in ℂx+1\in ℂ$$
4		peano5nni	$$⊢\left(1\in ℂ\wedge \forall x\in ℂx+1\in ℂ\right)\to \mathbb{N}\subseteq ℂ$$
5	1 3 4	mp2an	$$⊢\mathbb{N}\subseteq ℂ$$