Theorem cnre 8017

Description: Alias for ax-cnre 7985, 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 7985	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 2164   E.wrex 2473  (class class class)co 5919   CCcc 7872   RRcr 7873   _ici 7876   + caddc 7877   x. cmul 7879

This theorem was proved from axioms:  ax-cnre 7985

This theorem is referenced by:  mulrid  8018  cnegexlem2  8197  cnegex  8199  apirr  8626  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  apti  8643  recexap  8674  creur  8980  creui  8981  cju  8982  cnref1o  9719  replim  11006  cjap  11053