Theorem 0cnd 11194

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11093  0cc0 11095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-i2m1 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  addeq0  11632  mul0or  11849  eqneg  11930  un0addcl  12532  un0mulcl  12533  modsumfzodifsn  13976  muldivbinom2  14295  reusq0  15512  clim0c  15554  rlim0  15555  rlim0lt  15556  rlimneg  15694  isercolllem3  15714  sumrblem  15758  summolem2a  15762  sumz  15769  fsumcl  15780  expcnv  15914  ntrivcvgfvn0  15949  ef4p  16164  sadadd2lem2  16503  sadadd2lem  16512  modprm0  16860  iserodd  16890  prmrec  16977  4sqlem10  17002  4sqlem11  17010  frgpnabllem1  19938  evlsvvval  22244  fsumcn  25029  cnheibor  25114  evth2  25119  rrxmval  25564  mbfmulc2lem  25806  mbfpos  25810  dvcnp2  26079  dvcmulf  26104  dvmptc  26117  dvmptcmul  26123  dvmptfsum  26134  dveflem  26138  dvef  26139  rolle  26149  elply2  26353  plyf  26355  elplyr  26358  elplyd  26359  ply1term  26361  ply0  26365  plyeq0  26368  plyaddlem  26372  plymullem  26373  dgrlem  26386  coeidlem  26394  plyco  26398  coeeq2  26399  coe0  26413  plycj  26434  coecj  26435  plycjOLD  26436  coecjOLD  26437  plymul0or  26439  dvply1  26445  fta1lem  26468  elqaalem3  26482  tayl0  26525  dvtaylp  26533  taylthlem2  26537  radcnv0  26579  pserdvlem2  26591  pserdv  26592  ptolemy  26661  advlog  26819  advlogexp  26820  efopnlem2  26822  efopn  26823  logtayllem  26824  logtayl  26825  loglesqrt  26926  affineequiv  26988  quad2  27004  dcubic  27011  asinlem  27033  dvatan  27100  leibpilem2  27106  leibpi  27107  rlimcnp  27130  efrlim  27134  emcllem7  27166  dmgmaddn0  27187  lgamgulmlem2  27194  igamf  27215  igamcl  27216  sqff1o  27346  dchrelbasd  27403  dchrsum2  27432  sumdchr2  27434  addsq2reu  27604  addsqnreup  27607  dchrvmasumiflem2  27666  occllem  31655  nlelchi  32413  divnumden2  33160  fprodeq02  33168  gsumind  33665  constrrtcc  34125  constrsslem  34131  constraddcl  34152  constrmulcl  34161  cos9thpiminplylem1  34172  cos9thpiminplylem3  34174  cos9thpinconstrlem1  34179  ballotlemic  34897  ballotlem1c  34898  signsvfn  34969  circlemeth  35027  elmrsubrn  36012  climlec3  36226  bj-bary1lem  37974  tan2h  38283  ftc1anclem5  38368  ftc1anclem6  38369  ftc1anclem7  38370  ftc1anclem8  38371  ftc1anc  38372  lcmineqlem7  42822  lcmineqlem12  42827  aks4d1p1p7  42861  aks6d1c2p2  42906  aks6d1c5lem1  42923  aks6d1c5lem2  42925  sticksstones10  42942  sticksstones12a  42944  sn-addlid  43185  remul02  43186  remul01  43188  sn-it0e0  43197  sn-addrid  43202  sn-addid0  43206  sn-mul01  43207  sn-0tie0  43245  sn-mul02  43246  3cubeslem1  43435  pell14qrgt0  43606  expgrowth  45065  binomcxplemnotnn0  45086  ellimcabssub0  46353  0ellimcdiv  46383  clim0cf  46388  cosknegpi  46603  fprodsubrecnncnvlem  46641  fprodaddrecnncnvlem  46643  dvsinax  46647  dvasinbx  46654  dvnmptconst  46675  dvnxpaek  46676  itgiccshift  46714  itgperiod  46715  itgsbtaddcnst  46716  stirlinglem7  46814  dirkertrigeqlem2  46833  fourierdlem59  46899  fourierdlem62  46902  fourierdlem74  46914  fourierdlem75  46915  sqwvfoura  46962  fouriersw  46965  etransclem20  46988  etransclem21  46989  etransclem22  46990  etransclem25  46993  etransclem35  47003  sge0z  47109  ovnhoilem1  47335  vonsn  47425  sqrtnnaa  47624  sqrtnzqaa  47625  lambert0  47644  0nodd  48955  fdivmptf  49341  nn0sumshdiglem2  49422  eenglngeehlnmlem2  49538  itsclc0yqsollem1  49562