Theorem cnre 8015

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

Assertion

Ref	Expression
cnre	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Distinct variable group:   x, A, y

Proof of Theorem cnre

Step	Hyp	Ref	Expression
1		ax-cnre 7983	1 |- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164   E.wrex 2473  (class class class)co 5918   CCcc 7870   RRcr 7871   _ici 7874   + caddc 7875   x. cmul 7877

This theorem was proved from axioms:  ax-cnre 7983

This theorem is referenced by:  mulrid  8016  cnegexlem2  8195  cnegex  8197  apirr  8624  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  apti  8641  recexap  8672  creur  8978  creui  8979  cju  8980  cnref1o  9716  replim  11003  cjap  11050