Theorem cnre 10036

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

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   E.wrex 2913  (class class class)co 6650   CCcc 9934   RRcr 9935   _ici 9938   + caddc 9939   x. cmul 9941

This theorem was proved from axioms:  ax-cnre 10009

This theorem is referenced by:  mulid1  10037  1re  10039  mul02  10214  cnegex  10217  recex  10659  creur  11014  creui  11015  cju  11016  cnref1o  11827  replim  13856  ipasslem11  27695