Theorem cnre 7762

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480   E.wrex 2417  (class class class)co 5774   CCcc 7618   RRcr 7619   _ici 7622   + caddc 7623   x. cmul 7625

This theorem was proved from axioms:  ax-cnre 7731

This theorem is referenced by:  mulid1  7763  cnegexlem2  7938  cnegex  7940  apirr  8367  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  apti  8384  recexap  8414  creur  8717  creui  8718  cju  8719  cnref1o  9440  replim  10631  cjap  10678