Theorem cnre 8041

Description: Alias for ax-cnre 8009, 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 8009	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 7896   RRcr 7897   _ici 7900   + caddc 7901   x. cmul 7903

This theorem was proved from axioms:  ax-cnre 8009

This theorem is referenced by:  mulrid  8042  cnegexlem2  8221  cnegex  8223  apirr  8651  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  apti  8668  recexap  8699  creur  9005  creui  9006  cju  9007  cnref1o  9744  replim  11043  cjap  11090