ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnre Unicode version

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
StepHypRef Expression
1 ax-cnre 7517 1  |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator