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 e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cc	|- CC
2	0 1	wcel	|- A e. CC
3		vx	|- x
4		cr	|- RR
5		vy	|- y
6	3	cv	|- x
7		caddc	|- +
8		ci	|- _i
9		cmul	|- x.
10	5	cv	|- y
11	8 10 9	co	|- ( _i x. y )
12	6 11 7	co	|- ( x + ( _i x. y ) )
13	0 12	wceq	|- A = ( x + ( _i x. y ) )
14	13 5 4	wrex	|- E. y e. RR A = ( x + ( _i x. y ) )
15	14 3 4	wrex	|- E. x e. RR E. y e. RR A = ( x + ( _i x. y ) )
16	2 15	wi	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )