Theorem cnre 8142

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200   E.wrex 2509  (class class class)co 6001   CCcc 7997   RRcr 7998   _ici 8001   + caddc 8002   x. cmul 8004

This theorem was proved from axioms:  ax-cnre 8110

This theorem is referenced by:  mulrid  8143  cnegexlem2  8322  cnegex  8324  apirr  8752  apsym  8753  apcotr  8754  apadd1  8755  apneg  8758  mulext1  8759  apti  8769  recexap  8800  creur  9106  creui  9107  cju  9108  cnref1o  9846  replim  11370  cjap  11417