Theorem cnre 8158

Description: Alias for ax-cnre 8126, 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 8126	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 6010   CCcc 8013   RRcr 8014   _ici 8017   + caddc 8018   x. cmul 8020

This theorem was proved from axioms:  ax-cnre 8126

This theorem is referenced by:  mulrid  8159  cnegexlem2  8338  cnegex  8340  apirr  8768  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  apti  8785  recexap  8816  creur  9122  creui  9123  cju  9124  cnref1o  9863  replim  11391  cjap  11438