Theorem 0cnd 11216

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11115  0cc0 11117

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-mulcl 11179  ax-i2m1 11185

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

This theorem is used by:  addeq0  11654  mul0or  11871  eqneg  11952  un0addcl  12554  un0mulcl  12555  modsumfzodifsn  14000  muldivbinom2  14319  reusq0  15542  clim0c  15584  rlim0  15585  rlim0lt  15586  rlimneg  15724  isercolllem3  15744  sumrblem  15787  summolem2a  15791  sumz  15798  fsumcl  15809  expcnv  15943  ntrivcvgfvn0  15978  ef4p  16193  sadadd2lem2  16532  sadadd2lem  16541  modprm0  16889  iserodd  16919  prmrec  17006  4sqlem10  17031  4sqlem11  17039  frgpnabllem1  19989  evlsvvval  22296  fsumcn  25082  cnheibor  25167  evth2  25172  rrxmval  25617  mbfmulc2lem  25859  mbfpos  25863  dvcnp2  26132  dvcmulf  26157  dvmptc  26170  dvmptcmul  26176  dvmptfsum  26187  dveflem  26191  dvef  26192  rolle  26202  elply2  26406  plyf  26408  elplyr  26411  elplyd  26412  ply1term  26414  ply0  26418  plyeq0  26421  plyaddlem  26425  plymullem  26426  dgrlem  26439  coeidlem  26447  plyco  26451  coeeq2  26452  coe0  26466  plycj  26487  coecj  26488  plycjOLD  26489  coecjOLD  26490  plymul0or  26492  dvply1  26498  fta1lem  26521  elqaalem3  26535  tayl0  26578  dvtaylp  26586  taylthlem2  26590  radcnv0  26632  pserdvlem2  26644  pserdv  26645  ptolemy  26714  advlog  26872  advlogexp  26873  efopnlem2  26875  efopn  26876  logtayllem  26877  logtayl  26878  loglesqrt  26979  affineequiv  27041  quad2  27057  dcubic  27064  asinlem  27086  dvatan  27153  leibpilem2  27159  leibpi  27160  rlimcnp  27183  efrlim  27187  emcllem7  27219  dmgmaddn0  27240  lgamgulmlem2  27247  igamf  27268  igamcl  27269  sqff1o  27399  dchrelbasd  27456  dchrsum2  27485  sumdchr2  27487  addsq2reu  27657  addsqnreup  27660  dchrvmasumiflem2  27719  occllem  31728  nlelchi  32486  divnumden2  33232  fprodeq02  33240  gsumind  33731  constrrtcc  34191  constrsslem  34197  constraddcl  34218  constrmulcl  34227  cos9thpiminplylem1  34238  cos9thpiminplylem3  34240  cos9thpinconstrlem1  34245  ballotlemic  34964  ballotlem1c  34965  signsvfn  35036  circlemeth  35094  elmrsubrn  36051  climlec3  36265  bj-bary1lem  38013  tan2h  38322  ftc1anclem5  38407  ftc1anclem6  38408  ftc1anclem7  38409  ftc1anclem8  38410  ftc1anc  38411  lcmineqlem7  42862  lcmineqlem12  42867  aks4d1p1p7  42901  aks6d1c2p2  42946  aks6d1c5lem1  42963  aks6d1c5lem2  42965  sticksstones10  42982  sticksstones12a  42984  sn-addlid  43225  remul02  43226  remul01  43228  sn-it0e0  43237  sn-addrid  43242  sn-addid0  43246  sn-mul01  43247  sn-0tie0  43285  sn-mul02  43286  3cubeslem1  43475  pell14qrgt0  43646  expgrowth  45105  binomcxplemnotnn0  45126  ellimcabssub0  46393  0ellimcdiv  46423  clim0cf  46428  cosknegpi  46643  fprodsubrecnncnvlem  46681  fprodaddrecnncnvlem  46683  dvsinax  46687  dvasinbx  46694  dvnmptconst  46715  dvnxpaek  46716  itgiccshift  46754  itgperiod  46755  itgsbtaddcnst  46756  stirlinglem7  46854  dirkertrigeqlem2  46873  fourierdlem59  46939  fourierdlem62  46942  fourierdlem74  46954  fourierdlem75  46955  sqwvfoura  47002  fouriersw  47005  etransclem20  47028  etransclem21  47029  etransclem22  47030  etransclem25  47033  etransclem35  47043  sge0z  47149  ovnhoilem1  47375  vonsn  47465  sqrtnnaa  47664  sqrtnzqaa  47665  lambert0  47684  0nodd  48994  fdivmptf  49380  nn0sumshdiglem2  49461  eenglngeehlnmlem2  49577  itsclc0yqsollem1  49601