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 ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2		ax-1cn	⊢ 1 ∈ ℂ
3	2 2	addcli	⊢ ( 1 + 1 ) ∈ ℂ
4	1 3	eqeltri	⊢ 2 ∈ ℂ