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

Metamath Proof Explorer

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 ) ) )