This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ℕ \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	$⊢ (1 \in ℂ \land \forall x \in ℂ x + 1 \in ℂ) \to ℕ \subseteq ℂ$
5	1 3 4	mp2an	$⊢ ℕ \subseteq ℂ$