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

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

Proof of Theorem 0cnd
StepHypRef Expression
1 0cn 10232 . 2 0 ∈ ℂ
21a1i 11 1 (𝜑 → 0 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  cc 10134  0cc0 10136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-mulcl 10198  ax-i2m1 10204
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767
This theorem is referenced by:  mul0or  10867  diveq0  10895  eqneg  10945  un0addcl  11526  un0mulcl  11527  modsumfzodifsn  12944  muldivbinom2  13247  repswcshw  13760  clim0c  14439  rlim0  14440  rlim0lt  14441  rlimneg  14578  isercolllem3  14598  sumrblem  14643  summolem2a  14647  sumz  14654  fsumcl  14665  expcnv  14796  ntrivcvgfvn0  14831  ef4p  15042  sadadd2lem2  15373  sadadd2lem  15382  modprm0  15710  iserodd  15740  prmrec  15826  4sqlem10  15851  4sqlem11  15859  frgpnabllem1  18476  fsumcn  22886  cnheibor  22967  evth2  22972  rrxmval  23400  mbfmulc2lem  23627  mbfpos  23631  dvcmulf  23921  dvmptc  23934  dvmptcmul  23940  dvmptfsum  23951  dveflem  23955  rolle  23966  elply2  24165  plyf  24167  elplyr  24170  elplyd  24171  ply1term  24173  ply0  24177  plyeq0  24180  plyaddlem  24184  plymullem  24185  dgrlem  24198  coeidlem  24206  plyco  24210  coeeq2  24211  coe0  24225  plycj  24246  coecj  24247  plymul0or  24249  dvply1  24252  fta1lem  24275  elqaalem3  24289  tayl0  24329  dvtaylp  24337  taylthlem2  24341  radcnv0  24383  pserdvlem2  24395  pserdv  24396  ptolemy  24462  advlog  24614  advlogexp  24615  efopnlem2  24617  efopn  24618  logtayllem  24619  logtayl  24620  loglesqrt  24713  affineequiv  24767  quad2  24780  dcubic  24787  asinlem  24809  dvatan  24876  leibpilem2  24882  leibpi  24883  rlimcnp  24906  efrlim  24910  emcllem7  24942  dmgmaddn0  24963  lgamgulmlem2  24970  igamf  24991  igamcl  24992  sqff1o  25122  dchrelbasd  25178  dchrsum2  25207  sumdchr2  25209  dchrvmasumiflem2  25405  occllem  28495  nlelchi  29253  addeq0  29843  divnumden2  29897  fprodeq02  29902  ballotlemic  30901  ballotlem1c  30902  signsvfn  30992  circlemeth  31051  elmrsubrn  31748  climlec3  31950  bj-bary1lem  33490  tan2h  33727  ftc1anclem5  33814  ftc1anclem6  33815  ftc1anclem7  33816  ftc1anclem8  33817  ftc1anc  33818  pell14qrgt0  37942  expgrowth  39053  binomcxplemnotnn0  39074  ellimcabssub0  40360  0ellimcdiv  40392  clim0cf  40397  cosknegpi  40591  fprodsubrecnncnvlem  40632  fprodaddrecnncnvlem  40634  dvsinax  40638  dvasinbx  40646  dvnmptconst  40667  dvnxpaek  40668  itgiccshift  40706  itgperiod  40707  itgsbtaddcnst  40708  stirlinglem7  40807  dirkertrigeqlem2  40826  fourierdlem59  40892  fourierdlem62  40895  fourierdlem74  40907  fourierdlem75  40908  sqwvfoura  40955  fouriersw  40958  etransclem20  40981  etransclem21  40982  etransclem22  40983  etransclem25  40986  etransclem35  40996  sge0z  41102  ovnhoilem1  41328  vonsn  41418  0nodd  42331  fdivmptf  42856  nn0sumshdiglem2  42937
  Copyright terms: Public domain W3C validator