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

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

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 9063 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 9054 . . . 4  |-  _i  e.  CC
3 mulcl 9079 . . . 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 9053 . . 3  |-  1  e.  CC
6 addcl 9077 . . 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 6084   CCcc 8993   0cc0 8995   1c1 8996   _ici 8997    + caddc 8998    x. cmul 9000
This theorem is referenced by:  c0ex  9090  1re  9095  00id  9246  mul02lem1  9247  mul02  9249  mul01  9250  addid1  9251  addid2  9254  negcl  9311  subid  9326  subid1  9327  neg0  9352  negid  9353  negsub  9354  subneg  9355  negneg  9356  negeq0  9360  negsubdi  9362  renegcli  9367  mulneg1  9475  msqge0  9554  ixi  9656  mul0or  9667  muleqadd  9671  diveq0  9693  div0  9711  eqneg  9739  ofsubge0  10004  un0addcl  10258  un0mulcl  10259  elznn0  10301  ser0  11380  0exp  11420  sq0  11478  sqeqor  11500  binom2  11501  discr  11521  faclbnd  11586  faclbnd3  11588  faclbnd4lem3  11591  facubnd  11596  bcval5  11614  revs1  11802  s1co  11807  shftval3  11896  shftidt2  11901  cjne0  11973  sqr0  12052  abs0  12095  abs00bd  12101  abs2dif  12141  clim0  12305  clim0c  12306  rlim0  12307  rlim0lt  12308  climz  12348  serclim0  12376  rlimneg  12445  isercolllem3  12465  sumrblem  12510  fsumcvg  12511  summolem2a  12514  zsum  12517  sumz  12521  sumss  12523  fsumss  12524  fsumcvg2  12526  fsumcl  12532  fsumsplit  12538  sumsplit  12557  fsumparts  12590  fsumrelem  12591  fsumrlim  12595  fsumo1  12596  binom  12614  arisum2  12645  expcnv  12648  ef0lem  12686  ef0  12698  eftlub  12715  ef4p  12719  sin0  12755  tan0  12757  divalglem9  12926  sadadd2lem2  12967  sadadd2lem  12976  sadadd3  12978  bezout  13047  phiprmpw  13170  iserodd  13214  pcmpt2  13267  prmreclem2  13290  prmreclem4  13292  prmrec  13295  4sqlem10  13320  4sqlem11  13328  ramcl  13402  odadd1  15468  cnaddablx  15486  cnaddabl  15487  frgpnabllem1  15489  cncrng  16727  cnfld0  16730  cnbl0  18813  cnblcld  18814  cnfldnm  18818  xrge0gsumle  18869  xrge0tsms  18870  fsumcn  18905  cnheibor  18985  evth2  18990  csscld  19208  clsocv  19209  cnflduss  19315  cnfldcusp  19316  ovolicc1  19417  mbfss  19541  mbfmulc2lem  19542  0plef  19567  0pledm  19568  itg1ge0  19581  itg1addlem4  19594  itg2splitlem  19643  itg2addlem  19653  ibl0  19681  iblcnlem  19683  itgrevallem1  19689  iblss2  19700  itgss3  19709  dvconst  19808  dvcnp2  19811  dvcmulf  19836  dvrec  19846  dvmptc  19849  dvmptcmul  19855  dvmptfsum  19864  dvexp3  19867  dveflem  19868  dvef  19869  rolle  19879  dv11cn  19890  lhop1lem  19902  elply2  20120  plyun0  20121  plyf  20122  elplyr  20125  elplyd  20126  ply1term  20128  ply0  20132  plyeq0lem  20134  plyeq0  20135  plyaddlem  20139  plymullem  20140  coeeulem  20148  coeeu  20149  dgrlem  20153  coef3  20156  coeidlem  20161  plyco  20165  coeeq2  20166  dgrle  20167  0dgrb  20170  coefv0  20171  coemulc  20178  coe0  20179  coe1termlem  20181  coe1term  20182  dgr0  20185  dgrmulc  20194  dgrcolem2  20197  plycj  20200  coecj  20201  plymul0or  20203  dvply1  20206  plydiveu  20220  fta1lem  20229  vieta1lem2  20233  elqaalem3  20243  iaa  20247  aareccl  20248  aalioulem3  20256  tayl0  20283  dvtaylp  20291  taylthlem2  20295  radcnv0  20337  psercn  20347  pserdvlem2  20349  pserdv  20350  abelthlem2  20353  abelthlem3  20354  abelthlem5  20356  abelthlem7  20359  abelth  20362  pilem2  20373  sin2kpi  20396  cos2kpi  20397  ptolemy  20409  sinkpi  20432  advlog  20550  advlogexp  20551  efopnlem2  20553  efopn  20554  logtayllem  20555  logtayl  20556  cxpval  20560  0cxp  20562  cxpexp  20564  cxpcl  20570  cxpge0  20579  mulcxplem  20580  mulcxp  20581  cxpmul2  20585  dvsqr  20633  cxpcn3  20637  abscxpbnd  20642  loglesqr  20647  affineequiv  20672  quad2  20684  dcubic  20691  asinlem  20713  dvatan  20780  leibpilem2  20786  leibpi  20787  efrlim  20813  emcllem7  20845  harmonicbnd3  20851  ftalem2  20861  ftalem3  20862  ftalem4  20863  ftalem5  20864  ftalem7  20866  prmorcht  20966  sqff1o  20970  musum  20981  muinv  20983  1sgm2ppw  20989  logfacbnd3  21012  logexprlim  21014  dchrelbas2  21026  dchrelbasd  21028  dchrmulid2  21041  dchrfi  21044  dchrinv  21050  dchrsum2  21057  sumdchr2  21059  bposlem1  21073  bposlem2  21074  lgsdir2  21117  lgsdir  21119  rplogsumlem2  21184  dchrvmasumiflem1  21200  dchrvmasumiflem2  21201  rpvmasum2  21211  log2sumbnd  21243  selberg2lem  21249  logdivbnd  21255  pntrsumo1  21264  pntrlog2bndlem4  21279  pntrlog2bndlem5  21280  pntleml  21310  ex-co  21751  avril1  21762  cnaddablo  21943  cnid  21944  addinv  21945  vc0  22053  vcz  22054  vcoprne  22063  ipasslem8  22343  siilem2  22358  hvmul0  22531  hi01  22603  norm-iii  22647  occllem  22810  h1de2ctlem  23062  pjmuli  23196  pjneli  23230  eigre  23343  eigorth  23346  elnlfn  23436  0cnfn  23488  0lnfn  23493  lnopeq0i  23515  lnopunilem2  23519  nlelchi  23569  addeq0  24119  divnumden2  24166  xrge0tsmsd  24228  qqh0  24373  qqhcn  24380  ballotlemfval0  24758  ballotlem4  24761  ballotlemi1  24765  ballotlemic  24769  ballotlem1c  24770  dmgmaddn0  24812  lgamgulmlem2  24819  igamf  24840  igamcl  24841  subfacp1lem6  24876  sinccvglem  25114  abs2sqle  25125  abs2sqlt  25126  climlec3  25219  ntrivcvgfvn0  25232  0fallfac  25358  0risefac  25359  binomfallfac  25362  ax5seglem8  25880  axlowdimlem6  25891  axlowdimlem13  25898  fsumcube  26111  tan2h  26252  mblfinlem2  26256  ovoliunnfl  26260  voliunnfl  26262  itg2addnclem  26270  itg2addnclem3  26272  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  dvreacos  26305  cntotbnd  26519  pell14qrgt0  26936  acongeq  27062  mpaaeu  27346  flcidc  27370  dvconstbi  27542  expgrowth  27543  itgsinexplem1  27738  stoweidlem26  27765  stoweidlem36  27775  stoweidlem55  27794  stirlinglem7  27819  stirlinglem8  27820  swrdccat3a  28251  modprm0  28262  sec0  28577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-mulcl 9057  ax-i2m1 9063
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