MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0cn Unicode version

Theorem 0cn 8847
Description: 0 is a complex number. See also 0cnALT 9057. (Contributed by NM, 19-Feb-2005.)
Assertion
Ref Expression
0cn  |-  0  e.  CC

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 8821 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 8812 . . . 4  |-  _i  e.  CC
3 mulcl 8837 . . . 4  |-  ( ( _i  e.  CC  /\  _i  e.  CC )  -> 
( _i  x.  _i )  e.  CC )
42, 2, 3mp2an 653 . . 3  |-  ( _i  x.  _i )  e.  CC
5 ax-1cn 8811 . . 3  |-  1  e.  CC
6 addcl 8835 . . 3  |-  ( ( ( _i  x.  _i )  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  _i )  +  1 )  e.  CC )
74, 5, 6mp2an 653 . 2  |-  ( ( _i  x.  _i )  +  1 )  e.  CC
81, 7eqeltrri 2367 1  |-  0  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1696  (class class class)co 5874   CCcc 8751   0cc0 8753   1c1 8754   _ici 8755    + caddc 8756    x. cmul 8758
This theorem is referenced by:  c0ex  8848  1re  8853  00id  9003  mul02lem1  9004  mul02  9006  mul01  9007  addid1  9008  addid2  9011  negcl  9068  subid  9083  subid1  9084  neg0  9109  negid  9110  negsub  9111  subneg  9112  negneg  9113  negeq0  9117  negsubdi  9119  renegcli  9124  mulneg1  9232  msqge0  9311  ixi  9413  mul0or  9424  muleqadd  9428  diveq0  9450  div0  9468  eqneg  9496  ofsubge0  9761  un0addcl  10013  un0mulcl  10014  elznn0  10054  ser0  11114  0exp  11153  sq0  11211  sqeqor  11233  binom2  11234  discr  11254  faclbnd  11319  faclbnd3  11321  faclbnd4lem3  11324  facubnd  11329  bcval5  11346  revs1  11499  s1co  11504  shftval3  11587  shftidt2  11592  cjne0  11664  sqr0  11743  abs0  11786  abs00bd  11792  abs2dif  11832  clim0  11996  clim0c  11997  rlim0  11998  rlim0lt  11999  climz  12039  serclim0  12067  rlimneg  12136  isercolllem3  12156  sumrblem  12200  fsumcvg  12201  summolem2a  12204  zsum  12207  sumz  12211  sumss  12213  fsumss  12214  fsumcvg2  12216  fsumcl  12222  fsumsplit  12228  sumsplit  12247  fsumparts  12280  fsumrelem  12281  fsumrlim  12285  fsumo1  12286  binom  12304  arisum2  12335  expcnv  12338  ef0lem  12376  ef0  12388  eftlub  12405  ef4p  12409  sin0  12445  tan0  12447  divalglem9  12616  sadadd2lem2  12657  sadadd2lem  12666  sadadd3  12668  bezout  12737  phiprmpw  12860  iserodd  12904  pcmpt2  12957  prmreclem2  12980  prmreclem4  12982  prmrec  12985  4sqlem10  13010  4sqlem11  13018  ramcl  13092  odadd1  15156  cnaddablx  15174  cnaddabl  15175  frgpnabllem1  15177  cncrng  16411  cnfld0  16414  cnbl0  18299  cnblcld  18300  cnfldnm  18304  xrge0gsumle  18354  xrge0tsms  18355  fsumcn  18390  cnheibor  18469  evth2  18474  csscld  18692  clsocv  18693  ovolicc1  18891  mbfss  19017  mbfmulc2lem  19018  0plef  19043  0pledm  19044  itg1ge0  19057  itg1addlem4  19070  itg2splitlem  19119  itg2addlem  19129  ibl0  19157  iblcnlem  19159  itgrevallem1  19165  iblss2  19176  itgss3  19185  dvconst  19282  dvcnp2  19285  dvcmulf  19310  dvrec  19320  dvmptc  19323  dvmptcmul  19329  dvmptfsum  19338  dvexp3  19341  dveflem  19342  dvef  19343  rolle  19353  dv11cn  19364  lhop1lem  19376  elply2  19594  plyun0  19595  plyf  19596  elplyr  19599  elplyd  19600  ply1term  19602  ply0  19606  plyeq0lem  19608  plyeq0  19609  plyaddlem  19613  plymullem  19614  coeeulem  19622  coeeu  19623  dgrlem  19627  coef3  19630  coeidlem  19635  plyco  19639  coeeq2  19640  dgrle  19641  0dgrb  19644  coefv0  19645  coemulc  19652  coe0  19653  coe1termlem  19655  coe1term  19656  dgr0  19659  dgrmulc  19668  dgrcolem2  19671  plycj  19674  coecj  19675  plymul0or  19677  dvply1  19680  plydiveu  19694  fta1lem  19703  vieta1lem2  19707  elqaalem3  19717  iaa  19721  aareccl  19722  aalioulem3  19730  tayl0  19757  dvtaylp  19765  taylthlem2  19769  radcnv0  19808  psercn  19818  pserdvlem2  19820  pserdv  19821  abelthlem2  19824  abelthlem3  19825  abelthlem5  19827  abelthlem7  19830  abelth  19833  pilem2  19844  sin2kpi  19867  cos2kpi  19868  ptolemy  19880  sinkpi  19903  advlog  20017  advlogexp  20018  efopnlem2  20020  efopn  20021  logtayllem  20022  logtayl  20023  cxpval  20027  0cxp  20029  cxpexp  20031  cxpcl  20037  cxpge0  20046  mulcxplem  20047  mulcxp  20048  cxpmul2  20052  dvsqr  20100  cxpcn3  20104  abscxpbnd  20109  loglesqr  20114  affineequiv  20139  quad2  20151  dcubic  20158  asinlem  20180  dvatan  20247  leibpilem2  20253  leibpi  20254  efrlim  20280  emcllem7  20311  harmonicbnd3  20317  ftalem2  20327  ftalem3  20328  ftalem4  20329  ftalem5  20330  ftalem7  20332  prmorcht  20432  sqff1o  20436  musum  20447  muinv  20449  1sgm2ppw  20455  logfacbnd3  20478  logexprlim  20480  dchrelbas2  20492  dchrelbasd  20494  dchrmulid2  20507  dchrfi  20510  dchrinv  20516  dchrsum2  20523  sumdchr2  20525  bposlem1  20539  bposlem2  20540  lgsdir2  20583  lgsdir  20585  rplogsumlem2  20650  dchrvmasumiflem1  20666  dchrvmasumiflem2  20667  rpvmasum2  20677  log2sumbnd  20709  selberg2lem  20715  logdivbnd  20721  pntrsumo1  20730  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntleml  20776  ex-co  20841  avril1  20852  cnaddablo  21033  cnid  21034  addinv  21035  vc0  21141  vcz  21142  vcoprne  21151  ipasslem8  21431  siilem2  21446  hvmul0  21619  hi01  21691  norm-iii  21735  occllem  21898  h1de2ctlem  22150  pjmuli  22284  pjneli  22318  eigre  22431  eigorth  22434  elnlfn  22524  0cnfn  22576  0lnfn  22581  lnopeq0i  22603  lnopunilem2  22607  nlelchi  22657  addeq0  23059  ballotlemfval0  23070  ballotlem4  23073  ballotlemi1  23077  ballotlemic  23081  ballotlem1c  23082  xrge0tsmsd  23397  dmgmaddn0  23710  subfacp1lem6  23731  sinccvglem  24020  abs2sqle  24031  abs2sqlt  24032  ax5seglem8  24636  axlowdimlem6  24647  axlowdimlem13  24654  fsumcube  24867  ovoliunnfl  25001  itg2addnclem  25003  itgaddnclem2  25010  dvreacos  25027  zernpl  25756  valvze  25757  cntotbnd  26623  pell14qrgt0  27047  acongeq  27173  mpaaeu  27458  flcidc  27482  dvconstbi  27654  expgrowth  27655  itgsinexplem1  27851  stoweidlem26  27878  stoweidlem36  27888  stoweidlem44  27896  stoweidlem55  27907  stirlinglem7  27932  stirlinglem8  27933  sec0  28484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-mulcl 8815  ax-i2m1 8821
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator