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

Theorem cnre 7931
Description: Alias for ax-cnre 7900, 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 7900 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 1353    e. wcel 2148   E.wrex 2456  (class class class)co 5868   CCcc 7787   RRcr 7788   _ici 7791    + caddc 7792    x. cmul 7794
This theorem was proved from axioms:  ax-cnre 7900
This theorem is referenced by:  mulid1  7932  cnegexlem2  8110  cnegex  8112  apirr  8539  apsym  8540  apcotr  8541  apadd1  8542  apneg  8545  mulext1  8546  apti  8556  recexap  8586  creur  8892  creui  8893  cju  8894  cnref1o  9626  replim  10839  cjap  10886
  Copyright terms: Public domain W3C validator