Theorem cnre 7895

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136   E.wrex 2445  (class class class)co 5842   CCcc 7751   RRcr 7752   _ici 7755   + caddc 7756   x. cmul 7758

This theorem was proved from axioms:  ax-cnre 7864

This theorem is referenced by:  mulid1  7896  cnegexlem2  8074  cnegex  8076  apirr  8503  apsym  8504  apcotr  8505  apadd1  8506  apneg  8509  mulext1  8510  apti  8520  recexap  8550  creur  8854  creui  8855  cju  8856  cnref1o  9588  replim  10801  cjap  10848