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

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

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 8805 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 8796 . . . 4  |-  _i  e.  CC
3 mulcl 8821 . . . 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 8795 . . 3  |-  1  e.  CC
6 addcl 8819 . . 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 2354 1  |-  0  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1684  (class class class)co 5858   CCcc 8735   0cc0 8737   1c1 8738   _ici 8739    + caddc 8740    x. cmul 8742
This theorem is referenced by:  c0ex  8832  1re  8837  00id  8987  mul02lem1  8988  mul02  8990  mul01  8991  addid1  8992  addid2  8995  negcl  9052  subid  9067  subid1  9068  neg0  9093  negid  9094  negsub  9095  subneg  9096  negneg  9097  negeq0  9101  negsubdi  9103  renegcli  9108  mulneg1  9216  msqge0  9295  ixi  9397  mul0or  9408  muleqadd  9412  diveq0  9434  div0  9452  eqneg  9480  ofsubge0  9745  un0addcl  9997  un0mulcl  9998  elznn0  10038  ser0  11098  0exp  11137  sq0  11195  sqeqor  11217  binom2  11218  discr  11238  faclbnd  11303  faclbnd3  11305  faclbnd4lem3  11308  facubnd  11313  bcval5  11330  revs1  11483  s1co  11488  shftval3  11571  shftidt2  11576  cjne0  11648  sqr0  11727  abs0  11770  abs00bd  11776  abs2dif  11816  clim0  11980  clim0c  11981  rlim0  11982  rlim0lt  11983  climz  12023  serclim0  12051  rlimneg  12120  isercolllem3  12140  sumrblem  12184  fsumcvg  12185  summolem2a  12188  zsum  12191  sumz  12195  sumss  12197  fsumss  12198  fsumcvg2  12200  fsumcl  12206  fsumsplit  12212  sumsplit  12231  fsumparts  12264  fsumrelem  12265  fsumrlim  12269  fsumo1  12270  binom  12288  arisum2  12319  expcnv  12322  ef0lem  12360  ef0  12372  eftlub  12389  ef4p  12393  sin0  12429  tan0  12431  divalglem9  12600  sadadd2lem2  12641  sadadd2lem  12650  sadadd3  12652  bezout  12721  phiprmpw  12844  iserodd  12888  pcmpt2  12941  prmreclem2  12964  prmreclem4  12966  prmrec  12969  4sqlem10  12994  4sqlem11  13002  ramcl  13076  odadd1  15140  cnaddablx  15158  cnaddabl  15159  frgpnabllem1  15161  cncrng  16395  cnfld0  16398  cnbl0  18283  cnblcld  18284  cnfldnm  18288  xrge0gsumle  18338  xrge0tsms  18339  fsumcn  18374  cnheibor  18453  evth2  18458  csscld  18676  clsocv  18677  ovolicc1  18875  mbfss  19001  mbfmulc2lem  19002  0plef  19027  0pledm  19028  itg1ge0  19041  itg1addlem4  19054  itg2splitlem  19103  itg2addlem  19113  ibl0  19141  iblcnlem  19143  itgrevallem1  19149  iblss2  19160  itgss3  19169  dvconst  19266  dvcnp2  19269  dvcmulf  19294  dvrec  19304  dvmptc  19307  dvmptcmul  19313  dvmptfsum  19322  dvexp3  19325  dveflem  19326  dvef  19327  rolle  19337  dv11cn  19348  lhop1lem  19360  elply2  19578  plyun0  19579  plyf  19580  elplyr  19583  elplyd  19584  ply1term  19586  ply0  19590  plyeq0lem  19592  plyeq0  19593  plyaddlem  19597  plymullem  19598  coeeulem  19606  coeeu  19607  dgrlem  19611  coef3  19614  coeidlem  19619  plyco  19623  coeeq2  19624  dgrle  19625  0dgrb  19628  coefv0  19629  coemulc  19636  coe0  19637  coe1termlem  19639  coe1term  19640  dgr0  19643  dgrmulc  19652  dgrcolem2  19655  plycj  19658  coecj  19659  plymul0or  19661  dvply1  19664  plydiveu  19678  fta1lem  19687  vieta1lem2  19691  elqaalem3  19701  iaa  19705  aareccl  19706  aalioulem3  19714  tayl0  19741  dvtaylp  19749  taylthlem2  19753  radcnv0  19792  psercn  19802  pserdvlem2  19804  pserdv  19805  abelthlem2  19808  abelthlem3  19809  abelthlem5  19811  abelthlem7  19814  abelth  19817  pilem2  19828  sin2kpi  19851  cos2kpi  19852  ptolemy  19864  sinkpi  19887  advlog  20001  advlogexp  20002  efopnlem2  20004  efopn  20005  logtayllem  20006  logtayl  20007  cxpval  20011  0cxp  20013  cxpexp  20015  cxpcl  20021  cxpge0  20030  mulcxplem  20031  mulcxp  20032  cxpmul2  20036  dvsqr  20084  cxpcn3  20088  abscxpbnd  20093  loglesqr  20098  affineequiv  20123  quad2  20135  dcubic  20142  asinlem  20164  dvatan  20231  leibpilem2  20237  leibpi  20238  efrlim  20264  emcllem7  20295  harmonicbnd3  20301  ftalem2  20311  ftalem3  20312  ftalem4  20313  ftalem5  20314  ftalem7  20316  prmorcht  20416  sqff1o  20420  musum  20431  muinv  20433  1sgm2ppw  20439  logfacbnd3  20462  logexprlim  20464  dchrelbas2  20476  dchrelbasd  20478  dchrmulid2  20491  dchrfi  20494  dchrinv  20500  dchrsum2  20507  sumdchr2  20509  bposlem1  20523  bposlem2  20524  lgsdir2  20567  lgsdir  20569  rplogsumlem2  20634  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  rpvmasum2  20661  log2sumbnd  20693  selberg2lem  20699  logdivbnd  20705  pntrsumo1  20714  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntleml  20760  ex-co  20825  avril1  20836  cnaddablo  21017  cnid  21018  addinv  21019  vc0  21125  vcz  21126  vcoprne  21135  ipasslem8  21415  siilem2  21430  hvmul0  21603  hi01  21675  norm-iii  21719  occllem  21882  h1de2ctlem  22134  pjmuli  22268  pjneli  22302  eigre  22415  eigorth  22418  elnlfn  22508  0cnfn  22560  0lnfn  22565  lnopeq0i  22587  lnopunilem2  22591  nlelchi  22641  addeq0  23043  ballotlemfval0  23054  ballotlem4  23057  ballotlemi1  23061  ballotlemic  23065  ballotlem1c  23066  xrge0tsmsd  23382  dmgmaddn0  23695  subfacp1lem6  23716  sinccvglem  24005  abs2sqle  24016  abs2sqlt  24017  ax5seglem8  24564  axlowdimlem6  24575  axlowdimlem13  24582  fsumcube  24795  dvreacos  24924  zernpl  25653  valvze  25654  cntotbnd  26520  pell14qrgt0  26944  acongeq  27070  mpaaeu  27355  flcidc  27379  dvconstbi  27551  expgrowth  27552  itgsinexplem1  27748  stoweidlem26  27775  stoweidlem36  27785  stoweidlem44  27793  stoweidlem55  27804  stirlinglem7  27829  stirlinglem8  27830  sec0  28230
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-i2m1 8805
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator