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

Theorem 0cnd 10235
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 10234 . 2 0 ∈ ℂ
21a1i 11 1 (𝜑 → 0 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  cc 10136  0cc0 10138
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 10196  ax-icn 10197  ax-addcl 10198  ax-mulcl 10200  ax-i2m1 10206
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  10869  diveq0  10897  eqneg  10947  un0addcl  11528  un0mulcl  11529  modsumfzodifsn  12951  muldivbinom2  13254  repswcshw  13767  clim0c  14446  rlim0  14447  rlim0lt  14448  rlimneg  14585  isercolllem3  14605  sumrblem  14650  summolem2a  14654  sumz  14661  fsumcl  14672  expcnv  14803  ntrivcvgfvn0  14838  ef4p  15049  sadadd2lem2  15380  sadadd2lem  15389  modprm0  15717  iserodd  15747  prmrec  15833  4sqlem10  15858  4sqlem11  15866  frgpnabllem1  18483  fsumcn  22893  cnheibor  22974  evth2  22979  rrxmval  23407  mbfmulc2lem  23634  mbfpos  23638  dvcmulf  23928  dvmptc  23941  dvmptcmul  23947  dvmptfsum  23958  dveflem  23962  rolle  23973  elply2  24172  plyf  24174  elplyr  24177  elplyd  24178  ply1term  24180  ply0  24184  plyeq0  24187  plyaddlem  24191  plymullem  24192  dgrlem  24205  coeidlem  24213  plyco  24217  coeeq2  24218  coe0  24232  plycj  24253  coecj  24254  plymul0or  24256  dvply1  24259  fta1lem  24282  elqaalem3  24296  tayl0  24336  dvtaylp  24344  taylthlem2  24348  radcnv0  24390  pserdvlem2  24402  pserdv  24403  ptolemy  24469  advlog  24621  advlogexp  24622  efopnlem2  24624  efopn  24625  logtayllem  24626  logtayl  24627  loglesqrt  24720  affineequiv  24774  quad2  24787  dcubic  24794  asinlem  24816  dvatan  24883  leibpilem2  24889  leibpi  24890  rlimcnp  24913  efrlim  24917  emcllem7  24949  dmgmaddn0  24970  lgamgulmlem2  24977  igamf  24998  igamcl  24999  sqff1o  25129  dchrelbasd  25185  dchrsum2  25214  sumdchr2  25216  dchrvmasumiflem2  25412  occllem  28502  nlelchi  29260  addeq0  29850  divnumden2  29904  fprodeq02  29909  ballotlemic  30908  ballotlem1c  30909  signsvfn  30999  circlemeth  31058  elmrsubrn  31755  climlec3  31957  bj-bary1lem  33497  tan2h  33734  ftc1anclem5  33821  ftc1anclem6  33822  ftc1anclem7  33823  ftc1anclem8  33824  ftc1anc  33825  pell14qrgt0  37949  expgrowth  39060  binomcxplemnotnn0  39081  ellimcabssub0  40367  0ellimcdiv  40399  clim0cf  40404  cosknegpi  40598  fprodsubrecnncnvlem  40639  fprodaddrecnncnvlem  40641  dvsinax  40645  dvasinbx  40653  dvnmptconst  40674  dvnxpaek  40675  itgiccshift  40713  itgperiod  40714  itgsbtaddcnst  40715  stirlinglem7  40814  dirkertrigeqlem2  40833  fourierdlem59  40899  fourierdlem62  40902  fourierdlem74  40914  fourierdlem75  40915  sqwvfoura  40962  fouriersw  40965  etransclem20  40988  etransclem21  40989  etransclem22  40990  etransclem25  40993  etransclem35  41003  sge0z  41109  ovnhoilem1  41335  vonsn  41425  0nodd  42338  fdivmptf  42863  nn0sumshdiglem2  42944
  Copyright terms: Public domain W3C validator