Theorem 0cnd 11338

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

Step	Hyp	Ref	Expression
1		0cn 11337	. 2 ⊢ 0 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11237  0cc0 11239

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-i2m1 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  addeq0  11778  mul0or  11996  eqneg  12077  un0addcl  12679  un0mulcl  12680  modsumfzodifsn  14127  muldivbinom2  14448  reusq0  15676  clim0c  15718  rlim0  15719  rlim0lt  15720  rlimneg  15858  isercolllem3  15878  sumrblem  15921  summolem2a  15925  sumz  15932  fsumcl  15943  expcnv  16077  ntrivcvgfvn0  16112  ef4p  16325  sadadd2lem2  16664  sadadd2lem  16673  modprm0  17027  iserodd  17057  prmrec  17144  4sqlem10  17169  4sqlem11  17177  frgpnabllem1  20138  evlsvvval  22457  fsumcn  25246  cnheibor  25331  evth2  25336  rrxmval  25781  mbfmulc2lem  26023  mbfpos  26027  dvcnp2  26295  dvcmulf  26320  dvmptc  26333  dvmptcmul  26339  dvmptfsum  26350  dveflem  26354  dvef  26355  rolle  26365  elply2  26569  plyf  26571  elplyr  26574  elplyd  26575  ply1term  26577  ply0  26581  plyeq0  26585  plyaddlem  26589  plymullem  26590  dgrlem  26603  coeidlem  26611  plyco  26615  coeeq2  26616  coe0  26630  plycj  26651  coecj  26652  plymul0or  26654  dvply1  26660  fta1lem  26683  elqaalem3  26701  tayl0  26746  dvtaylp  26754  taylthlem2  26758  radcnv0  26800  pserdvlem2  26812  pserdv  26813  ptolemy  26882  advlog  27039  advlogexp  27040  efopnlem2  27042  efopn  27043  logtayllem  27044  logtayl  27045  loglesqrt  27146  affineequiv  27208  quad2  27224  dcubic  27231  asinlem  27253  dvatan  27320  leibpilem2  27326  leibpi  27327  rlimcnp  27350  efrlim  27354  emcllem7  27386  dmgmaddn0  27407  lgamgulmlem2  27414  igamf  27435  igamcl  27436  sqff1o  27566  dchrelbasd  27623  dchrsum2  27652  sumdchr2  27654  addsq2reu  27824  addsqnreup  27827  dchrvmasumiflem2  27886  occllem  31962  nlelchi  32720  divnumden2  33503  fprodeq02  33511  gsumind  34010  constrrtcc  34478  constrsslem  34484  constraddcl  34505  constrmulcl  34514  cos9thpiminplylem1  34525  cos9thpiminplylem3  34527  cos9thpinconstrlem1  34532  ballotlemic  35250  ballotlem1c  35251  signsvfn  35322  circlemeth  35380  elmrsubrn  36493  climlec3  36714  bj-bary1lem  38499  tan2h  38803  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anclem8  38886  ftc1anc  38887  lcmineqlem7  43351  lcmineqlem12  43356  aks4d1p1p7  43390  aks6d1c2p2  43435  aks6d1c5lem1  43452  aks6d1c5lem2  43454  sticksstones10  43471  sticksstones12a  43473  sn-addlid  43721  remul02  43722  remul01  43724  sn-it0e0  43733  sn-addrid  43738  sn-addid0  43742  sn-mul01  43743  sn-0tie0  43781  sn-mul02  43782  3cubeslem1  43960  pell14qrgt0  44132  expgrowth  45580  binomcxplemnotnn0  45601  ellimcabssub0  46902  0ellimcdiv  46932  clim0cf  46937  cosknegpi  47152  fprodsubrecnncnvlem  47190  fprodaddrecnncnvlem  47192  dvsinax  47196  dvasinbx  47203  dvnmptconst  47224  dvnxpaek  47225  itgiccshift  47263  itgperiod  47264  itgsbtaddcnst  47265  stirlinglem7  47363  dirkertrigeqlem2  47382  fourierdlem59  47448  fourierdlem62  47451  fourierdlem74  47463  fourierdlem75  47464  sqwvfoura  47511  fouriersw  47514  etransclem20  47537  etransclem21  47538  etransclem22  47539  etransclem25  47542  etransclem35  47552  sge0z  47658  ovnhoilem1  47884  vonsn  47974  sqrtnnaa  48186  sqrtnzqaa  48187  lambert0  48210  0nodd  49540  fdivmptf  49984  nn0sumshdiglem2  50065  eenglngeehlnmlem2  50182  itsclc0yqsollem1  50205