Theorem cnre 8150

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200   E.wrex 2509  (class class class)co 6007   CCcc 8005   RRcr 8006   _ici 8009   + caddc 8010   x. cmul 8012

This theorem was proved from axioms:  ax-cnre 8118

This theorem is referenced by:  mulrid  8151  cnegexlem2  8330  cnegex  8332  apirr  8760  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  apti  8777  recexap  8808  creur  9114  creui  9115  cju  9116  cnref1o  9854  replim  11378  cjap  11425