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

Metamath Proof Explorer

Theorem 2cn

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022)

		Ref	Expression
	Assertion	2cn	$⊢ 2 \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		df-2	$⊢ 2 = 1 + 1$
2		ax-1cn	$⊢ 1 \in ℂ$
3	2 2	addcli	$⊢ 1 + 1 \in ℂ$
4	1 3	eqeltri	$⊢ 2 \in ℂ$