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

Metamath Proof Explorer

Theorem cnre

Description: Alias for ax-cnre , for naming consistency. (Contributed by NM, 3-Jan-2013)

		Ref	Expression
	Assertion	cnre	$⊢ A \in ℂ \to \exists x \in ℝ \exists y \in ℝ A = x + i y$

Step	Hyp	Ref	Expression
1		ax-cnre	$⊢ A \in ℂ \to \exists x \in ℝ \exists y \in ℝ A = x + i y$