Theorem cnre 8103

Description: Alias for ax-cnre 8071, 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 8071	1 |- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178   E.wrex 2487  (class class class)co 5967   CCcc 7958   RRcr 7959   _ici 7962   + caddc 7963   x. cmul 7965

This theorem was proved from axioms:  ax-cnre 8071

This theorem is referenced by:  mulrid  8104  cnegexlem2  8283  cnegex  8285  apirr  8713  apsym  8714  apcotr  8715  apadd1  8716  apneg  8719  mulext1  8720  apti  8730  recexap  8761  creur  9067  creui  9068  cju  9069  cnref1o  9807  replim  11285  cjap  11332