Theorem cnre 7545

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

Syntax hints:   -> wi 4   = wceq 1290   e. wcel 1439   E.wrex 2361  (class class class)co 5666   CCcc 7409   RRcr 7410   _ici 7413   + caddc 7414   x. cmul 7416

This theorem was proved from axioms:  ax-cnre 7517

This theorem is referenced by:  mulid1  7546  cnegexlem2  7719  cnegex  7721  apirr  8143  apsym  8144  apcotr  8145  apadd1  8146  apneg  8149  mulext1  8150  apti  8160  recexap  8183  creur  8480  creui  8481  cju  8482  cnref1o  9194  replim  10354  cjap  10401