Theorem cnre 8323

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209   E.wrex 2529  (class class class)co 6085   CCcc 8178   RRcr 8179   _ici 8182   + caddc 8183   x. cmul 8185

This proof depends on axioms:  ax-cnre 8291

This theorem is used by:  mulrid  8324  cnegexlem2  8504  cnegex  8506  apirr  8936  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  apti  8953  recexap  8984  creur  9292  creui  9293  cju  9294  cnref1o  10062  replim  11640  cjap  11688