Theorem 0cnd 11224

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 11223	. 2 ⊢ 0 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11123  0cc0 11125

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-mulcl 11187  ax-i2m1 11193

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

This theorem is used by:  addeq0  11662  mul0or  11879  eqneg  11960  un0addcl  12562  un0mulcl  12563  modsumfzodifsn  14009  muldivbinom2  14328  reusq0  15553  clim0c  15595  rlim0  15596  rlim0lt  15597  rlimneg  15735  isercolllem3  15755  sumrblem  15798  summolem2a  15802  sumz  15809  fsumcl  15820  expcnv  15954  ntrivcvgfvn0  15989  ef4p  16202  sadadd2lem2  16541  sadadd2lem  16550  modprm0  16898  iserodd  16928  prmrec  17015  4sqlem10  17040  4sqlem11  17048  frgpnabllem1  20001  evlsvvval  22310  fsumcn  25099  cnheibor  25184  evth2  25189  rrxmval  25634  mbfmulc2lem  25876  mbfpos  25880  dvcnp2  26148  dvcmulf  26173  dvmptc  26186  dvmptcmul  26192  dvmptfsum  26203  dveflem  26207  dvef  26208  rolle  26218  elply2  26422  plyf  26424  elplyr  26427  elplyd  26428  ply1term  26430  ply0  26434  plyeq0  26438  plyaddlem  26442  plymullem  26443  dgrlem  26456  coeidlem  26464  plyco  26468  coeeq2  26469  coe0  26483  plycj  26504  coecj  26505  plycjOLD  26506  coecjOLD  26507  plymul0or  26509  dvply1  26515  fta1lem  26538  elqaalem3  26554  tayl0  26599  dvtaylp  26607  taylthlem2  26611  radcnv0  26653  pserdvlem2  26665  pserdv  26666  ptolemy  26735  advlog  26892  advlogexp  26893  efopnlem2  26895  efopn  26896  logtayllem  26897  logtayl  26898  loglesqrt  26999  affineequiv  27061  quad2  27077  dcubic  27084  asinlem  27106  dvatan  27173  leibpilem2  27179  leibpi  27180  rlimcnp  27203  efrlim  27207  emcllem7  27239  dmgmaddn0  27260  lgamgulmlem2  27267  igamf  27288  igamcl  27289  sqff1o  27419  dchrelbasd  27476  dchrsum2  27505  sumdchr2  27507  addsq2reu  27677  addsqnreup  27680  dchrvmasumiflem2  27739  occllem  31785  nlelchi  32543  divnumden2  33287  fprodeq02  33295  gsumind  33786  constrrtcc  34246  constrsslem  34252  constraddcl  34273  constrmulcl  34282  cos9thpiminplylem1  34293  cos9thpiminplylem3  34295  cos9thpinconstrlem1  34300  ballotlemic  35019  ballotlem1c  35020  signsvfn  35091  circlemeth  35149  elmrsubrn  36100  climlec3  36314  bj-bary1lem  38063  tan2h  38367  ftc1anclem5  38447  ftc1anclem6  38448  ftc1anclem7  38449  ftc1anclem8  38450  ftc1anc  38451  lcmineqlem7  42902  lcmineqlem12  42907  aks4d1p1p7  42941  aks6d1c2p2  42986  aks6d1c5lem1  43003  aks6d1c5lem2  43005  sticksstones10  43022  sticksstones12a  43024  sn-addlid  43280  remul02  43281  remul01  43283  sn-it0e0  43292  sn-addrid  43297  sn-addid0  43301  sn-mul01  43302  sn-0tie0  43340  sn-mul02  43341  3cubeslem1  43530  pell14qrgt0  43701  expgrowth  45160  binomcxplemnotnn0  45181  ellimcabssub0  46448  0ellimcdiv  46478  clim0cf  46483  cosknegpi  46698  fprodsubrecnncnvlem  46736  fprodaddrecnncnvlem  46738  dvsinax  46742  dvasinbx  46749  dvnmptconst  46770  dvnxpaek  46771  itgiccshift  46809  itgperiod  46810  itgsbtaddcnst  46811  stirlinglem7  46909  dirkertrigeqlem2  46928  fourierdlem59  46994  fourierdlem62  46997  fourierdlem74  47009  fourierdlem75  47010  sqwvfoura  47057  fouriersw  47060  etransclem20  47083  etransclem21  47084  etransclem22  47085  etransclem25  47088  etransclem35  47098  sge0z  47204  ovnhoilem1  47430  vonsn  47520  sqrtnnaa  47732  sqrtnzqaa  47733  lambert0  47756  0nodd  49086  fdivmptf  49472  nn0sumshdiglem2  49553  eenglngeehlnmlem2  49669  itsclc0yqsollem1  49693