Axiom ax-cnre

Description: A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of Gleason p. 130. Axiom 17 of 22 for real and complex numbers, justified by Theorem axcnre . For naming consistency, use cnre for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999)

	Ref	Expression
Assertion	ax-cnre	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cc	$$classℂ$$
2	0 1	wcel	$$wffA\in ℂ$$
3		vx	$$setvarx$$
4		cr	$$classℝ$$
5		vy	$$setvary$$
6	3	cv	$$setvarx$$
7		caddc	$$class+$$
8		ci	$$class\mathrm{i}$$
9		cmul	$$class\times$$
10	5	cv	$$setvary$$
11	8 10 9	co	$$class\mathrm{i}y$$
12	6 11 7	co	$$class\left(x+\mathrm{i}y\right)$$
13	0 12	wceq	$$wffA=x+\mathrm{i}y$$
14	13 5 4	wrex	$$wff\exists y\in ℝA=x+\mathrm{i}y$$
15	14 3 4	wrex	$$wff\exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$
16	2 15	wi	$$wff\left(A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\right)$$