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

Theorem cnre 7081
Description: Alias for ax-cnre 7053, 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 7053 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 1259    e. wcel 1409   E.wrex 2324  (class class class)co 5540   CCcc 6945   RRcr 6946   _ici 6949    + caddc 6950    x. cmul 6952
This theorem was proved from axioms:  ax-cnre 7053
This theorem is referenced by:  mulid1  7082  cnegexlem2  7250  cnegex  7252  apirr  7670  apsym  7671  apcotr  7672  apadd1  7673  apneg  7676  mulext1  7677  apti  7687  recexap  7708  creur  7987  creui  7988  cju  7989  cnref1o  8680  replim  9687  cjap  9734
  Copyright terms: Public domain W3C validator