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

Theorem 0cnd 9610
Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
0cnd

Proof of Theorem 0cnd
StepHypRef Expression
1 0cn 9609 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511  0cc0 9513
This theorem is referenced by:  mul0or  10214  diveq0  10242  eqneg  10289  un0addcl  10854  un0mulcl  10855  repswcshw  12780  clim0c  13330  rlim0  13331  rlim0lt  13332  rlimneg  13469  isercolllem3  13489  sumrblem  13533  summolem2a  13537  sumz  13544  fsumcl  13555  expcnv  13675  ntrivcvgfvn0  13708  ef4p  13848  sadadd2lem2  14100  sadadd2lem  14109  modprm0  14330  iserodd  14359  prmrec  14440  4sqlem10  14465  4sqlem11  14473  frgpnabllem1  16877  fsumcn  21374  cnheibor  21455  evth2  21460  rrxmval  21832  mbfmulc2lem  22054  mbfpos  22058  dvcmulf  22348  dvmptc  22361  dvmptcmul  22367  dvmptfsum  22376  dveflem  22380  rolle  22391  elply2  22593  plyf  22595  elplyr  22598  elplyd  22599  ply1term  22601  ply0  22605  plyeq0  22608  plyaddlem  22612  plymullem  22613  dgrlem  22626  coeidlem  22634  plyco  22638  coeeq2  22639  coe0  22653  plycj  22674  coecj  22675  plymul0or  22677  dvply1  22680  fta1lem  22703  elqaalem3  22717  tayl0  22757  dvtaylp  22765  taylthlem2  22769  radcnv0  22811  pserdvlem2  22823  pserdv  22824  ptolemy  22889  advlog  23035  advlogexp  23036  efopnlem2  23038  efopn  23039  logtayllem  23040  logtayl  23041  loglesqrt  23132  affineequiv  23157  quad2  23170  dcubic  23177  asinlem  23199  dvatan  23266  leibpilem2  23272  leibpi  23273  rlimcnp  23295  efrlim  23299  emcllem7  23331  sqff1o  23456  dchrelbasd  23514  dchrsum2  23543  sumdchr2  23545  dchrvmasumiflem2  23687  occllem  26221  nlelchi  26980  addeq0  27558  divnumden2  27609  ballotlemic  28445  ballotlem1c  28446  signsvfn  28539  dmgmaddn0  28565  lgamgulmlem2  28572  igamf  28593  igamcl  28594  elmrsubrn  28880  climlec3  29120  tan2h  30047  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  pell14qrgt0  30795  expgrowth  31240  binomcxplemnotnn0  31261  ellimcabssub0  31623  0ellimcdiv  31655  clim0cf  31660  cosknegpi  31669  dvsinax  31708  dvasinbx  31717  dvnmptconst  31738  dvnxpaek  31739  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stirlinglem7  31862  dirkertrigeqlem2  31881  fourierdlem59  31948  fourierdlem62  31951  fourierdlem74  31963  fourierdlem75  31964  sqwvfoura  32011  fouriersw  32014  etransclem20  32037  etransclem21  32038  etransclem22  32039  etransclem25  32042  etransclem35  32052  0nodd  32498  bj-bary1lem  34679
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