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

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

Proof of Theorem 0cnd
StepHypRef Expression
1 0cn 10611 . 2 0 ∈ ℂ
21a1i 11 1 (𝜑 → 0 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  cc 10513  0cc0 10515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-mulcl 10577  ax-i2m1 10583
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2813  df-clel 2891
This theorem is referenced by:  addeq0  11041  mul0or  11258  diveq0  11286  eqneg  11338  un0addcl  11909  un0mulcl  11910  modsumfzodifsn  13296  muldivbinom2  13608  reusq0  14802  clim0c  14844  rlim0  14845  rlim0lt  14846  rlimneg  14983  isercolllem3  15003  sumrblem  15048  summolem2a  15052  sumz  15059  fsumcl  15070  expcnv  15199  ntrivcvgfvn0  15235  ef4p  15446  sadadd2lem2  15777  sadadd2lem  15786  modprm0  16120  iserodd  16150  prmrec  16236  4sqlem10  16261  4sqlem11  16269  frgpnabllem1  18972  fsumcn  23454  cnheibor  23539  evth2  23544  rrxmval  23988  mbfmulc2lem  24230  mbfpos  24234  dvcmulf  24527  dvmptc  24540  dvmptcmul  24546  dvmptfsum  24557  dveflem  24561  dvef  24562  rolle  24572  elply2  24772  plyf  24774  elplyr  24777  elplyd  24778  ply1term  24780  ply0  24784  plyeq0  24787  plyaddlem  24791  plymullem  24792  dgrlem  24805  coeidlem  24813  plyco  24817  coeeq2  24818  coe0  24832  plycj  24853  coecj  24854  plymul0or  24856  dvply1  24859  fta1lem  24882  elqaalem3  24896  tayl0  24936  dvtaylp  24944  taylthlem2  24948  radcnv0  24990  pserdvlem2  25002  pserdv  25003  ptolemy  25068  advlog  25224  advlogexp  25225  efopnlem2  25227  efopn  25228  logtayllem  25229  logtayl  25230  loglesqrt  25326  affineequiv  25388  quad2  25404  dcubic  25411  asinlem  25433  dvatan  25500  leibpilem2  25506  leibpi  25507  rlimcnp  25530  efrlim  25534  emcllem7  25566  dmgmaddn0  25587  lgamgulmlem2  25594  igamf  25615  igamcl  25616  sqff1o  25746  dchrelbasd  25802  dchrsum2  25831  sumdchr2  25833  addsq2reu  26003  addsqnreup  26006  dchrvmasumiflem2  26065  occllem  29065  nlelchi  29823  divnumden2  30521  fprodeq02  30526  ballotlemic  31772  ballotlem1c  31773  signsvfn  31860  circlemeth  31919  elmrsubrn  32775  climlec3  32973  bj-bary1lem  34608  tan2h  34925  ftc1anclem5  35010  ftc1anclem6  35011  ftc1anclem7  35012  ftc1anclem8  35013  ftc1anc  35014  lcmineqlem7  39187  lcmineqlem12  39192  sn-addid2  39354  remul02  39355  remul01  39357  sn-it0e0  39364  sn-addid1  39369  sn-addid0  39372  sn-mul01  39373  3cubeslem1  39418  pell14qrgt0  39593  expgrowth  40822  binomcxplemnotnn0  40843  ellimcabssub0  42050  0ellimcdiv  42082  clim0cf  42087  cosknegpi  42302  fprodsubrecnncnvlem  42340  fprodaddrecnncnvlem  42342  dvsinax  42346  dvasinbx  42353  dvnmptconst  42374  dvnxpaek  42375  itgiccshift  42413  itgperiod  42414  itgsbtaddcnst  42415  stirlinglem7  42513  dirkertrigeqlem2  42532  fourierdlem59  42598  fourierdlem62  42601  fourierdlem74  42613  fourierdlem75  42614  sqwvfoura  42661  fouriersw  42664  etransclem20  42687  etransclem21  42688  etransclem22  42689  etransclem25  42692  etransclem35  42702  sge0z  42805  ovnhoilem1  43031  vonsn  43121  0nodd  44222  fdivmptf  44746  nn0sumshdiglem2  44827  eenglngeehlnmlem2  44912  itsclc0yqsollem1  44936
  Copyright terms: Public domain W3C validator