Theorem cnre 8039

Description: Alias for ax-cnre 8007, 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 8007	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 2167   E.wrex 2476  (class class class)co 5925   CCcc 7894   RRcr 7895   _ici 7898   + caddc 7899   x. cmul 7901

This theorem was proved from axioms:  ax-cnre 8007

This theorem is referenced by:  mulrid  8040  cnegexlem2  8219  cnegex  8221  apirr  8649  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  apti  8666  recexap  8697  creur  9003  creui  9004  cju  9005  cnref1o  9742  replim  11041  cjap  11088