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

Theorem 0cnd 9980
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 9979 . 2 0 ∈ ℂ
21a1i 11 1 (𝜑 → 0 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cc 9881  0cc0 9883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-mulcl 9945  ax-i2m1 9951
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617
This theorem is referenced by:  mul0or  10614  diveq0  10642  eqneg  10692  un0addcl  11273  un0mulcl  11274  modsumfzodifsn  12686  muldivbinom2  12990  repswcshw  13498  clim0c  14175  rlim0  14176  rlim0lt  14177  rlimneg  14314  isercolllem3  14334  sumrblem  14378  summolem2a  14382  sumz  14389  fsumcl  14400  expcnv  14524  ntrivcvgfvn0  14559  ef4p  14771  sadadd2lem2  15099  sadadd2lem  15108  modprm0  15437  iserodd  15467  prmrec  15553  4sqlem10  15578  4sqlem11  15586  frgpnabllem1  18200  fsumcn  22586  cnheibor  22667  evth2  22672  rrxmval  23101  mbfmulc2lem  23327  mbfpos  23331  dvcmulf  23621  dvmptc  23634  dvmptcmul  23640  dvmptfsum  23649  dveflem  23653  rolle  23664  elply2  23863  plyf  23865  elplyr  23868  elplyd  23869  ply1term  23871  ply0  23875  plyeq0  23878  plyaddlem  23882  plymullem  23883  dgrlem  23896  coeidlem  23904  plyco  23908  coeeq2  23909  coe0  23923  plycj  23944  coecj  23945  plymul0or  23947  dvply1  23950  fta1lem  23973  elqaalem3  23987  tayl0  24027  dvtaylp  24035  taylthlem2  24039  radcnv0  24081  pserdvlem2  24093  pserdv  24094  ptolemy  24159  advlog  24307  advlogexp  24308  efopnlem2  24310  efopn  24311  logtayllem  24312  logtayl  24313  loglesqrt  24406  affineequiv  24460  quad2  24473  dcubic  24480  asinlem  24502  dvatan  24569  leibpilem2  24575  leibpi  24576  rlimcnp  24599  efrlim  24603  emcllem7  24635  dmgmaddn0  24656  lgamgulmlem2  24663  igamf  24684  igamcl  24685  sqff1o  24815  dchrelbasd  24871  dchrsum2  24900  sumdchr2  24902  dchrvmasumiflem2  25098  occllem  28023  nlelchi  28781  addeq0  29365  divnumden2  29417  ballotlemic  30361  ballotlem1c  30362  signsvfn  30451  elmrsubrn  31146  climlec3  31348  bj-bary1lem  32814  tan2h  33054  ftc1anclem5  33142  ftc1anclem6  33143  ftc1anclem7  33144  ftc1anclem8  33145  ftc1anc  33146  pell14qrgt0  36924  expgrowth  38037  binomcxplemnotnn0  38058  ellimcabssub0  39271  0ellimcdiv  39303  clim0cf  39308  cosknegpi  39401  fprodsubrecnncnvlem  39442  fprodaddrecnncnvlem  39444  dvsinax  39449  dvasinbx  39458  dvnmptconst  39479  dvnxpaek  39480  itgiccshift  39519  itgperiod  39520  itgsbtaddcnst  39521  stirlinglem7  39620  dirkertrigeqlem2  39639  fourierdlem59  39705  fourierdlem62  39708  fourierdlem74  39720  fourierdlem75  39721  sqwvfoura  39768  fouriersw  39771  etransclem20  39794  etransclem21  39795  etransclem22  39796  etransclem25  39799  etransclem35  39809  sge0z  39915  ovnhoilem1  40138  vonsn  40228  0nodd  41114  fdivmptf  41643  nn0sumshdiglem2  41724
  Copyright terms: Public domain W3C validator