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

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

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 9060 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 9051 . . . 4  |-  _i  e.  CC
3 mulcl 9076 . . . 4  |-  ( ( _i  e.  CC  /\  _i  e.  CC )  -> 
( _i  x.  _i )  e.  CC )
42, 2, 3mp2an 655 . . 3  |-  ( _i  x.  _i )  e.  CC
5 ax-1cn 9050 . . 3  |-  1  e.  CC
6 addcl 9074 . . 3  |-  ( ( ( _i  x.  _i )  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  _i )  +  1 )  e.  CC )
74, 5, 6mp2an 655 . 2  |-  ( ( _i  x.  _i )  +  1 )  e.  CC
81, 7eqeltrri 2509 1  |-  0  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1726  (class class class)co 6083   CCcc 8990   0cc0 8992   1c1 8993   _ici 8994    + caddc 8995    x. cmul 8997
This theorem is referenced by:  c0ex  9087  1re  9092  00id  9243  mul02lem1  9244  mul02  9246  mul01  9247  addid1  9248  addid2  9251  negcl  9308  subid  9323  subid1  9324  neg0  9349  negid  9350  negsub  9351  subneg  9352  negneg  9353  negeq0  9357  negsubdi  9359  renegcli  9364  mulneg1  9472  msqge0  9551  ixi  9653  mul0or  9664  muleqadd  9668  diveq0  9690  div0  9708  eqneg  9736  ofsubge0  10001  un0addcl  10255  un0mulcl  10256  elznn0  10298  ser0  11377  0exp  11417  sq0  11475  sqeqor  11497  binom2  11498  discr  11518  faclbnd  11583  faclbnd3  11585  faclbnd4lem3  11588  facubnd  11593  bcval5  11611  revs1  11799  s1co  11804  shftval3  11893  shftidt2  11898  cjne0  11970  sqr0  12049  abs0  12092  abs00bd  12098  abs2dif  12138  clim0  12302  clim0c  12303  rlim0  12304  rlim0lt  12305  climz  12345  serclim0  12373  rlimneg  12442  isercolllem3  12462  sumrblem  12507  fsumcvg  12508  summolem2a  12511  zsum  12514  sumz  12518  sumss  12520  fsumss  12521  fsumcvg2  12523  fsumcl  12529  fsumsplit  12535  sumsplit  12554  fsumparts  12587  fsumrelem  12588  fsumrlim  12592  fsumo1  12593  binom  12611  arisum2  12642  expcnv  12645  ef0lem  12683  ef0  12695  eftlub  12712  ef4p  12716  sin0  12752  tan0  12754  divalglem9  12923  sadadd2lem2  12964  sadadd2lem  12973  sadadd3  12975  bezout  13044  phiprmpw  13167  iserodd  13211  pcmpt2  13264  prmreclem2  13287  prmreclem4  13289  prmrec  13292  4sqlem10  13317  4sqlem11  13325  ramcl  13399  odadd1  15465  cnaddablx  15483  cnaddabl  15484  frgpnabllem1  15486  cncrng  16724  cnfld0  16727  cnbl0  18810  cnblcld  18811  cnfldnm  18815  xrge0gsumle  18866  xrge0tsms  18867  fsumcn  18902  cnheibor  18982  evth2  18987  csscld  19205  clsocv  19206  cnflduss  19312  cnfldcusp  19313  ovolicc1  19414  mbfss  19540  mbfmulc2lem  19541  0plef  19566  0pledm  19567  itg1ge0  19580  itg1addlem4  19593  itg2splitlem  19642  itg2addlem  19652  ibl0  19680  iblcnlem  19682  itgrevallem1  19688  iblss2  19699  itgss3  19708  dvconst  19805  dvcnp2  19808  dvcmulf  19833  dvrec  19843  dvmptc  19846  dvmptcmul  19852  dvmptfsum  19861  dvexp3  19864  dveflem  19865  dvef  19866  rolle  19876  dv11cn  19887  lhop1lem  19899  elply2  20117  plyun0  20118  plyf  20119  elplyr  20122  elplyd  20123  ply1term  20125  ply0  20129  plyeq0lem  20131  plyeq0  20132  plyaddlem  20136  plymullem  20137  coeeulem  20145  coeeu  20146  dgrlem  20150  coef3  20153  coeidlem  20158  plyco  20162  coeeq2  20163  dgrle  20164  0dgrb  20167  coefv0  20168  coemulc  20175  coe0  20176  coe1termlem  20178  coe1term  20179  dgr0  20182  dgrmulc  20191  dgrcolem2  20194  plycj  20197  coecj  20198  plymul0or  20200  dvply1  20203  plydiveu  20217  fta1lem  20226  vieta1lem2  20230  elqaalem3  20240  iaa  20244  aareccl  20245  aalioulem3  20253  tayl0  20280  dvtaylp  20288  taylthlem2  20292  radcnv0  20334  psercn  20344  pserdvlem2  20346  pserdv  20347  abelthlem2  20350  abelthlem3  20351  abelthlem5  20353  abelthlem7  20356  abelth  20359  pilem2  20370  sin2kpi  20393  cos2kpi  20394  ptolemy  20406  sinkpi  20429  advlog  20547  advlogexp  20548  efopnlem2  20550  efopn  20551  logtayllem  20552  logtayl  20553  cxpval  20557  0cxp  20559  cxpexp  20561  cxpcl  20567  cxpge0  20576  mulcxplem  20577  mulcxp  20578  cxpmul2  20582  dvsqr  20630  cxpcn3  20634  abscxpbnd  20639  loglesqr  20644  affineequiv  20669  quad2  20681  dcubic  20688  asinlem  20710  dvatan  20777  leibpilem2  20783  leibpi  20784  efrlim  20810  emcllem7  20842  harmonicbnd3  20848  ftalem2  20858  ftalem3  20859  ftalem4  20860  ftalem5  20861  ftalem7  20863  prmorcht  20963  sqff1o  20967  musum  20978  muinv  20980  1sgm2ppw  20986  logfacbnd3  21009  logexprlim  21011  dchrelbas2  21023  dchrelbasd  21025  dchrmulid2  21038  dchrfi  21041  dchrinv  21047  dchrsum2  21054  sumdchr2  21056  bposlem1  21070  bposlem2  21071  lgsdir2  21114  lgsdir  21116  rplogsumlem2  21181  dchrvmasumiflem1  21197  dchrvmasumiflem2  21198  rpvmasum2  21208  log2sumbnd  21240  selberg2lem  21246  logdivbnd  21252  pntrsumo1  21261  pntrlog2bndlem4  21276  pntrlog2bndlem5  21277  pntleml  21307  ex-co  21748  avril1  21759  cnaddablo  21940  cnid  21941  addinv  21942  vc0  22050  vcz  22051  vcoprne  22060  ipasslem8  22340  siilem2  22355  hvmul0  22528  hi01  22600  norm-iii  22644  occllem  22807  h1de2ctlem  23059  pjmuli  23193  pjneli  23227  eigre  23340  eigorth  23343  elnlfn  23433  0cnfn  23485  0lnfn  23490  lnopeq0i  23512  lnopunilem2  23516  nlelchi  23566  addeq0  24116  divnumden2  24163  xrge0tsmsd  24225  qqh0  24370  qqhcn  24377  ballotlemfval0  24755  ballotlem4  24758  ballotlemi1  24762  ballotlemic  24766  ballotlem1c  24767  dmgmaddn0  24809  lgamgulmlem2  24816  igamf  24837  igamcl  24838  subfacp1lem6  24873  sinccvglem  25111  abs2sqle  25122  abs2sqlt  25123  climlec3  25216  ntrivcvgfvn0  25229  0fallfac  25355  0risefac  25356  binomfallfac  25359  ax5seglem8  25877  axlowdimlem6  25888  axlowdimlem13  25895  fsumcube  26108  mblfinlem2  26246  ovoliunnfl  26250  voliunnfl  26252  itg2addnclem  26258  itg2addnclem3  26260  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  dvreacos  26293  cntotbnd  26507  pell14qrgt0  26924  acongeq  27050  mpaaeu  27334  flcidc  27358  dvconstbi  27530  expgrowth  27531  itgsinexplem1  27726  stoweidlem26  27753  stoweidlem36  27763  stoweidlem55  27782  stirlinglem7  27807  stirlinglem8  27808  swrdccat3a  28239  modprm0  28250  sec0  28565
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-mulcl 9054  ax-i2m1 9060
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator