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

Theorem 0cnd 11149
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 11148 . 2 0 ∈ ℂ
21a1i 11 1 (𝜑 → 0 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 11050  0cc0 11052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-mulcl 11114  ax-i2m1 11120
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815
This theorem is referenced by:  addeq0  11579  mul0or  11796  diveq0  11824  eqneg  11876  un0addcl  12447  un0mulcl  12448  modsumfzodifsn  13850  muldivbinom2  14164  reusq0  15348  clim0c  15390  rlim0  15391  rlim0lt  15392  rlimneg  15532  isercolllem3  15552  sumrblem  15597  summolem2a  15601  sumz  15608  fsumcl  15619  expcnv  15750  ntrivcvgfvn0  15785  ef4p  15996  sadadd2lem2  16331  sadadd2lem  16340  modprm0  16678  iserodd  16708  prmrec  16795  4sqlem10  16820  4sqlem11  16828  frgpnabllem1  19652  fsumcn  24236  cnheibor  24321  evth2  24326  rrxmval  24772  mbfmulc2lem  25014  mbfpos  25018  dvcmulf  25312  dvmptc  25325  dvmptcmul  25331  dvmptfsum  25342  dveflem  25346  dvef  25347  rolle  25357  elply2  25560  plyf  25562  elplyr  25565  elplyd  25566  ply1term  25568  ply0  25572  plyeq0  25575  plyaddlem  25579  plymullem  25580  dgrlem  25593  coeidlem  25601  plyco  25605  coeeq2  25606  coe0  25620  plycj  25641  coecj  25642  plymul0or  25644  dvply1  25647  fta1lem  25670  elqaalem3  25684  tayl0  25724  dvtaylp  25732  taylthlem2  25736  radcnv0  25778  pserdvlem2  25790  pserdv  25791  ptolemy  25856  advlog  26012  advlogexp  26013  efopnlem2  26015  efopn  26016  logtayllem  26017  logtayl  26018  loglesqrt  26114  affineequiv  26176  quad2  26192  dcubic  26199  asinlem  26221  dvatan  26288  leibpilem2  26294  leibpi  26295  rlimcnp  26318  efrlim  26322  emcllem7  26354  dmgmaddn0  26375  lgamgulmlem2  26382  igamf  26403  igamcl  26404  sqff1o  26534  dchrelbasd  26590  dchrsum2  26619  sumdchr2  26621  addsq2reu  26791  addsqnreup  26794  dchrvmasumiflem2  26853  occllem  30248  nlelchi  31006  divnumden2  31717  fprodeq02  31722  ballotlemic  33109  ballotlem1c  33110  signsvfn  33197  circlemeth  33256  elmrsubrn  34117  climlec3  34309  bj-bary1lem  35784  tan2h  36073  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  lcmineqlem7  40495  lcmineqlem12  40500  aks4d1p1p7  40534  aks6d1c2p2  40552  sticksstones10  40566  sticksstones12a  40568  sn-addid2  40876  remul02  40877  remul01  40879  sn-it0e0  40887  sn-addid1  40892  sn-addid0  40896  sn-mul01  40897  sn-0tie0  40911  sn-mul02  40912  3cubeslem1  41010  pell14qrgt0  41185  expgrowth  42622  binomcxplemnotnn0  42643  ellimcabssub0  43865  0ellimcdiv  43897  clim0cf  43902  cosknegpi  44117  fprodsubrecnncnvlem  44155  fprodaddrecnncnvlem  44157  dvsinax  44161  dvasinbx  44168  dvnmptconst  44189  dvnxpaek  44190  itgiccshift  44228  itgperiod  44229  itgsbtaddcnst  44230  stirlinglem7  44328  dirkertrigeqlem2  44347  fourierdlem59  44413  fourierdlem62  44416  fourierdlem74  44428  fourierdlem75  44429  sqwvfoura  44476  fouriersw  44479  etransclem20  44502  etransclem21  44503  etransclem22  44504  etransclem25  44507  etransclem35  44517  sge0z  44623  ovnhoilem1  44849  vonsn  44939  0nodd  46111  fdivmptf  46634  nn0sumshdiglem2  46715  eenglngeehlnmlem2  46831  itsclc0yqsollem1  46855
  Copyright terms: Public domain W3C validator