Theorem cnre 8266

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203   E.wrex 2521  (class class class)co 6049   CCcc 8121   RRcr 8122   _ici 8125   + caddc 8126   x. cmul 8128

This theorem was proved from axioms:  ax-cnre 8234

This theorem is referenced by:  mulrid  8267  cnegexlem2  8445  cnegex  8447  apirr  8875  apsym  8876  apcotr  8877  apadd1  8878  apneg  8881  mulext1  8882  apti  8892  recexap  8923  creur  9229  creui  9230  cju  9231  cnref1o  9979  replim  11537  cjap  11584