Theorem 0cnd 11226

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

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

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 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-i2m1 11195

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  11664  mul0or  11881  eqneg  11962  un0addcl  12564  un0mulcl  12565  modsumfzodifsn  14011  muldivbinom2  14330  reusq0  15555  clim0c  15597  rlim0  15598  rlim0lt  15599  rlimneg  15737  isercolllem3  15757  sumrblem  15800  summolem2a  15804  sumz  15811  fsumcl  15822  expcnv  15956  ntrivcvgfvn0  15991  ef4p  16204  sadadd2lem2  16543  sadadd2lem  16552  modprm0  16900  iserodd  16930  prmrec  17017  4sqlem10  17042  4sqlem11  17050  frgpnabllem1  20003  evlsvvval  22312  fsumcn  25101  cnheibor  25186  evth2  25191  rrxmval  25636  mbfmulc2lem  25878  mbfpos  25882  dvcnp2  26150  dvcmulf  26175  dvmptc  26188  dvmptcmul  26194  dvmptfsum  26205  dveflem  26209  dvef  26210  rolle  26220  elply2  26424  plyf  26426  elplyr  26429  elplyd  26430  ply1term  26432  ply0  26436  plyeq0  26440  plyaddlem  26444  plymullem  26445  dgrlem  26458  coeidlem  26466  plyco  26470  coeeq2  26471  coe0  26485  plycj  26506  coecj  26507  plycjOLD  26508  coecjOLD  26509  plymul0or  26511  dvply1  26517  fta1lem  26540  elqaalem3  26556  tayl0  26601  dvtaylp  26609  taylthlem2  26613  radcnv0  26655  pserdvlem2  26667  pserdv  26668  ptolemy  26737  advlog  26894  advlogexp  26895  efopnlem2  26897  efopn  26898  logtayllem  26899  logtayl  26900  loglesqrt  27001  affineequiv  27063  quad2  27079  dcubic  27086  asinlem  27108  dvatan  27175  leibpilem2  27181  leibpi  27182  rlimcnp  27205  efrlim  27209  emcllem7  27241  dmgmaddn0  27262  lgamgulmlem2  27269  igamf  27290  igamcl  27291  sqff1o  27421  dchrelbasd  27478  dchrsum2  27507  sumdchr2  27509  addsq2reu  27679  addsqnreup  27682  dchrvmasumiflem2  27741  occllem  31787  nlelchi  32545  divnumden2  33289  fprodeq02  33297  gsumind  33788  constrrtcc  34248  constrsslem  34254  constraddcl  34275  constrmulcl  34284  cos9thpiminplylem1  34295  cos9thpiminplylem3  34297  cos9thpinconstrlem1  34302  ballotlemic  35021  ballotlem1c  35022  signsvfn  35093  circlemeth  35151  elmrsubrn  36102  climlec3  36316  bj-bary1lem  38065  tan2h  38369  ftc1anclem5  38449  ftc1anclem6  38450  ftc1anclem7  38451  ftc1anclem8  38452  ftc1anc  38453  lcmineqlem7  42904  lcmineqlem12  42909  aks4d1p1p7  42943  aks6d1c2p2  42988  aks6d1c5lem1  43005  aks6d1c5lem2  43007  sticksstones10  43024  sticksstones12a  43026  sn-addlid  43282  remul02  43283  remul01  43285  sn-it0e0  43294  sn-addrid  43299  sn-addid0  43303  sn-mul01  43304  sn-0tie0  43342  sn-mul02  43343  3cubeslem1  43532  pell14qrgt0  43703  expgrowth  45162  binomcxplemnotnn0  45183  ellimcabssub0  46450  0ellimcdiv  46480  clim0cf  46485  cosknegpi  46700  fprodsubrecnncnvlem  46738  fprodaddrecnncnvlem  46740  dvsinax  46744  dvasinbx  46751  dvnmptconst  46772  dvnxpaek  46773  itgiccshift  46811  itgperiod  46812  itgsbtaddcnst  46813  stirlinglem7  46911  dirkertrigeqlem2  46930  fourierdlem59  46996  fourierdlem62  46999  fourierdlem74  47011  fourierdlem75  47012  sqwvfoura  47059  fouriersw  47062  etransclem20  47085  etransclem21  47086  etransclem22  47087  etransclem25  47090  etransclem35  47100  sge0z  47206  ovnhoilem1  47432  vonsn  47522  sqrtnnaa  47734  sqrtnzqaa  47735  lambert0  47758  0nodd  49088  fdivmptf  49474  nn0sumshdiglem2  49555  eenglngeehlnmlem2  49671  itsclc0yqsollem1  49695