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

Theorem cnre 11159
Description: Alias for ax-cnre 11131, 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 11131 1 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1542   โˆˆ wcel 2107  โˆƒwrex 3074  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  ici 11060   + caddc 11061   ยท cmul 11063
This theorem was proved from axioms:  ax-cnre 11131
This theorem is referenced by:  mulid1  11160  1re  11162  0re  11164  mul02  11340  cnegex  11343  0cnALT  11396  recex  11794  creur  12154  creui  12155  cju  12156  cnref1o  12917  replim  15008  ipasslem11  29824  sn-addid2  40902  sn-it0e0  40913  sn-negex12  40914  sn-mulid2  40933  sn-0tie0  40937  sn-mul02  40938
  Copyright terms: Public domain W3C validator