Theorem cnre 7994

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2160   E.wrex 2469  (class class class)co 5904   CCcc 7849   RRcr 7850   _ici 7853   + caddc 7854   x. cmul 7856

This theorem was proved from axioms:  ax-cnre 7962

This theorem is referenced by:  mulrid  7995  cnegexlem2  8174  cnegex  8176  apirr  8603  apsym  8604  apcotr  8605  apadd1  8606  apneg  8609  mulext1  8610  apti  8620  recexap  8651  creur  8957  creui  8958  cju  8959  cnref1o  9692  replim  10915  cjap  10962