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

Theorem 0cn 9609
Description: 0 is a complex number. See also 0cnALT 9832. (Contributed by NM, 19-Feb-2005.)
Assertion
Ref Expression
0cn

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 9581 . 2
2 ax-icn 9572 . . . 4
3 mulcl 9597 . . . 4
42, 2, 3mp2an 672 . . 3
5 ax-1cn 9571 . . 3
6 addcl 9595 . . 3
74, 5, 6mp2an 672 . 2
81, 7eqeltrri 2542 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  (class class class)co 6296   cc 9511  0cc0 9513  1c1 9514   ci 9515   caddc 9516   cmul 9518
This theorem is referenced by:  0cnd  9610  c0ex  9611  1re  9616  00id  9776  mul02lem1  9777  mul02  9779  mul01  9780  addid1  9781  addid2  9784  negcl  9843  subid  9861  subid1  9862  neg0  9888  negid  9889  negsub  9890  subneg  9891  negneg  9892  negeq0  9896  negsubdi  9898  renegcli  9903  mulneg1  10018  msqge0  10099  ixi  10203  muleqadd  10218  div0  10260  ofsubge0  10560  0m0e0  10670  elznn0  10904  ser0  12159  0exp0e1  12171  0exp  12201  sq0  12259  sqeqor  12282  binom2  12283  bcval5  12396  s1co  12799  shftval3  12909  shftidt2  12914  cjne0  12996  sqrt0  13075  abs0  13118  abs00bd  13124  abs2dif  13165  clim0  13329  climz  13372  serclim0  13400  rlimneg  13469  sumrblem  13533  fsumcvg  13534  summolem2a  13537  sumss  13546  fsumss  13547  fsumcvg2  13549  fsumsplit  13562  sumsplit  13583  fsumrelem  13621  fsumrlim  13625  fsumo1  13626  ef0  13826  eftlub  13844  sin0  13884  tan0  13886  divalglem9  14059  sadadd2lem2  14100  sadadd3  14111  bezout  14180  pcmpt2  14412  prmreclem2  14435  4sqlem11  14473  ramcl  14547  odadd1  16854  cnaddablx  16874  cnaddabl  16875  frgpnabllem1  16877  cncrng  18439  cnfld0  18442  cnbl0  21281  cnblcld  21282  cnfldnm  21286  xrge0gsumle  21338  xrge0tsms  21339  cnheibor  21455  csscld  21689  clsocv  21690  cnflduss  21796  cnfldcusp  21797  rrxmvallem  21831  rrxmval  21832  mbfss  22053  mbfmulc2lem  22054  0plef  22079  0pledm  22080  itg1ge0  22093  itg1addlem4  22106  itg2splitlem  22155  itg2addlem  22165  ibl0  22193  iblcnlem  22195  iblss2  22212  itgss3  22221  dvconst  22320  dvcnp2  22323  dvrec  22358  dvexp3  22379  dveflem  22380  dvef  22381  dv11cn  22402  lhop1lem  22414  plyun0  22594  plyeq0lem  22607  coeeulem  22621  coeeu  22622  coef3  22629  dgrle  22640  0dgrb  22643  coefv0  22645  coemulc  22652  coe1termlem  22655  coe1term  22656  dgr0  22659  dgrmulc  22668  dgrcolem2  22671  vieta1lem2  22707  iaa  22721  aareccl  22722  aalioulem3  22730  taylthlem2  22769  psercn  22821  pserdvlem2  22823  abelthlem2  22827  abelthlem3  22828  abelthlem5  22830  abelthlem7  22833  abelth  22836  sin2kpi  22876  cos2kpi  22877  sinkpi  22912  efopn  23039  logtayl  23041  cxpval  23045  0cxp  23047  cxpexp  23049  cxpcl  23055  cxpge0  23064  mulcxplem  23065  mulcxp  23066  cxpmul2  23070  dvsqrt  23118  cxpcn3  23122  abscxpbnd  23127  efrlim  23299  ftalem2  23347  ftalem3  23348  ftalem4  23349  ftalem5  23350  ftalem7  23352  prmorcht  23452  muinv  23469  1sgm2ppw  23475  logfacbnd3  23498  logexprlim  23500  dchrelbas2  23512  dchrmulid2  23527  dchrfi  23530  dchrinv  23536  lgsdir2  23603  lgsdir  23605  dchrvmasumiflem1  23686  dchrvmasumiflem2  23687  rpvmasum2  23697  log2sumbnd  23729  selberg2lem  23735  logdivbnd  23741  ax5seglem8  24239  axlowdimlem6  24250  axlowdimlem13  24257  ex-co  25159  avril1  25171  cnaddablo  25352  cnid  25353  addinv  25354  vc0  25462  vcz  25463  vcoprne  25472  ipasslem8  25752  siilem2  25767  hvmul0  25941  hi01  26013  norm-iii  26057  h1de2ctlem  26473  pjmuli  26607  pjneli  26641  eigre  26754  eigorth  26757  elnlfn  26847  0cnfn  26899  0lnfn  26904  lnopunilem2  26930  xrge0tsmsd  27775  qqh0  27965  qqhcn  27972  eulerpartlemgs2  28319  sgnneg  28479  subfacp1lem6  28629  sinccvglem  29038  abs2sqle  29046  abs2sqlt  29047  0fallfac  29159  0risefac  29160  binomfallfac  29163  fsumcube  29822  tan2h  30047  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  ftc1anclem5  30094  dvcnsqrt  30101  cntotbnd  30292  flcidc  31123  dvconstbi  31239  expgrowth  31240  dvradcnv2  31252  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  negcncfg  31683  ioodvbdlimc1  31730  ioodvbdlimc2  31732  itgsinexplem1  31752  stoweidlem26  31808  stoweidlem36  31818  stoweidlem55  31837  stirlinglem8  31863  fourierdlem103  31992  sqwvfoura  32011  sqwvfourb  32012  sec0  33154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-i2m1 9581
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator