Theorem cnre 8180

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2201   E.wrex 2510  (class class class)co 6023   CCcc 8035   RRcr 8036   _ici 8039   + caddc 8040   x. cmul 8042

This theorem was proved from axioms:  ax-cnre 8148

This theorem is referenced by:  mulrid  8181  cnegexlem2  8360  cnegex  8362  apirr  8790  apsym  8791  apcotr  8792  apadd1  8793  apneg  8796  mulext1  8797  apti  8807  recexap  8838  creur  9144  creui  9145  cju  9146  cnref1o  9890  replim  11442  cjap  11489