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

Theorem cnre 7484
Description: Alias for ax-cnre 7456, 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 7456 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 1289    e. wcel 1438   E.wrex 2360  (class class class)co 5652   CCcc 7348   RRcr 7349   _ici 7352    + caddc 7353    x. cmul 7355
This theorem was proved from axioms:  ax-cnre 7456
This theorem is referenced by:  mulid1  7485  cnegexlem2  7658  cnegex  7660  apirr  8082  apsym  8083  apcotr  8084  apadd1  8085  apneg  8088  mulext1  8089  apti  8099  recexap  8122  creur  8419  creui  8420  cju  8421  cnref1o  9133  replim  10293  cjap  10340
  Copyright terms: Public domain W3C validator