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

Metamath Proof Explorer

Theorem 8cn

Description: The number 8 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022)

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

Proof

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