MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnre Structured version   Visualization version   GIF version

Theorem cnre 11207
Description: Alias for ax-cnre 11179, for naming consistency. (Contributed by NM, 3-Jan-2013.)
Assertion
Ref Expression
cnre (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)))
Distinct variable group:   ๐‘ฅ,๐ด,๐‘ฆ

Proof of Theorem cnre
StepHypRef Expression
1 ax-cnre 11179 1 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1541   โˆˆ wcel 2106  โˆƒwrex 3070  (class class class)co 7405  โ„‚cc 11104  โ„cr 11105  ici 11108   + caddc 11109   ยท cmul 11111
This theorem was proved from axioms:  ax-cnre 11179
This theorem is referenced by:  mulrid  11208  1re  11210  0re  11212  mul02  11388  cnegex  11391  0cnALT  11444  recex  11842  creur  12202  creui  12203  cju  12204  cnref1o  12965  replim  15059  ipasslem11  30080  sn-addlid  41273  sn-it0e0  41284  sn-negex12  41285  sn-mullid  41304  sn-0tie0  41308  sn-mul02  41309
  Copyright terms: Public domain W3C validator