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

Theorem cnre 7755
Description: Alias for ax-cnre 7724, 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 7724 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 1331    e. wcel 1480   E.wrex 2415  (class class class)co 5767   CCcc 7611   RRcr 7612   _ici 7615    + caddc 7616    x. cmul 7618
This theorem was proved from axioms:  ax-cnre 7724
This theorem is referenced by:  mulid1  7756  cnegexlem2  7931  cnegex  7933  apirr  8360  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  apti  8377  recexap  8407  creur  8710  creui  8711  cju  8712  cnref1o  9433  replim  10624  cjap  10671
  Copyright terms: Public domain W3C validator