Theorem cnre 8070

Description: Alias for ax-cnre 8038, 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 8038	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 2176   E.wrex 2485  (class class class)co 5946   CCcc 7925   RRcr 7926   _ici 7929   + caddc 7930   x. cmul 7932

This theorem was proved from axioms:  ax-cnre 8038

This theorem is referenced by:  mulrid  8071  cnegexlem2  8250  cnegex  8252  apirr  8680  apsym  8681  apcotr  8682  apadd1  8683  apneg  8686  mulext1  8687  apti  8697  recexap  8728  creur  9034  creui  9035  cju  9036  cnref1o  9774  replim  11203  cjap  11250