Theorem 0cnd 11127

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11026  0cc0 11028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-i2m1 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  addeq0  11562  mul0or  11779  eqneg  11863  un0addcl  12436  un0mulcl  12437  modsumfzodifsn  13869  muldivbinom2  14188  reusq0  15390  clim0c  15432  rlim0  15433  rlim0lt  15434  rlimneg  15572  isercolllem3  15592  sumrblem  15636  summolem2a  15640  sumz  15647  fsumcl  15658  expcnv  15789  ntrivcvgfvn0  15824  ef4p  16040  sadadd2lem2  16379  sadadd2lem  16388  modprm0  16735  iserodd  16765  prmrec  16852  4sqlem10  16877  4sqlem11  16885  frgpnabllem1  19804  evlsvvval  22050  fsumcn  24819  cnheibor  24912  evth2  24917  rrxmval  25363  mbfmulc2lem  25606  mbfpos  25610  dvcnp2  25879  dvcmulf  25906  dvmptc  25920  dvmptcmul  25926  dvmptfsum  25937  dveflem  25941  dvef  25942  rolle  25952  elply2  26159  plyf  26161  elplyr  26164  elplyd  26165  ply1term  26167  ply0  26171  plyeq0  26174  plyaddlem  26178  plymullem  26179  dgrlem  26192  coeidlem  26200  plyco  26204  coeeq2  26205  coe0  26219  plycj  26241  coecj  26242  plycjOLD  26243  coecjOLD  26244  plymul0or  26246  dvply1  26249  fta1lem  26273  elqaalem3  26287  tayl0  26327  dvtaylp  26336  taylthlem2  26340  taylthlem2OLD  26341  radcnv0  26383  pserdvlem2  26396  pserdv  26397  ptolemy  26463  advlog  26621  advlogexp  26622  efopnlem2  26624  efopn  26625  logtayllem  26626  logtayl  26627  loglesqrt  26729  affineequiv  26791  quad2  26807  dcubic  26814  asinlem  26836  dvatan  26903  leibpilem2  26909  leibpi  26910  rlimcnp  26933  efrlim  26937  efrlimOLD  26938  emcllem7  26970  dmgmaddn0  26991  lgamgulmlem2  26998  igamf  27019  igamcl  27020  sqff1o  27150  dchrelbasd  27208  dchrsum2  27237  sumdchr2  27239  addsq2reu  27409  addsqnreup  27412  dchrvmasumiflem2  27471  occllem  31380  nlelchi  32138  divnumden2  32898  fprodeq02  32906  gsumind  33428  constrrtcc  33894  constrsslem  33900  constraddcl  33921  constrmulcl  33930  cos9thpiminplylem1  33941  cos9thpiminplylem3  33943  cos9thpinconstrlem1  33948  ballotlemic  34666  ballotlem1c  34667  signsvfn  34741  circlemeth  34799  elmrsubrn  35716  climlec3  35930  bj-bary1lem  37517  tan2h  37815  ftc1anclem5  37900  ftc1anclem6  37901  ftc1anclem7  37902  ftc1anclem8  37903  ftc1anc  37904  lcmineqlem7  42311  lcmineqlem12  42316  aks4d1p1p7  42350  aks6d1c2p2  42395  aks6d1c5lem1  42412  aks6d1c5lem2  42414  sticksstones10  42431  sticksstones12a  42433  sn-addlid  42680  remul02  42681  remul01  42683  sn-it0e0  42692  sn-addrid  42697  sn-addid0  42701  sn-mul01  42702  sn-0tie0  42727  sn-mul02  42728  3cubeslem1  42947  pell14qrgt0  43122  expgrowth  44597  binomcxplemnotnn0  44618  ellimcabssub0  45884  0ellimcdiv  45914  clim0cf  45919  cosknegpi  46134  fprodsubrecnncnvlem  46172  fprodaddrecnncnvlem  46174  dvsinax  46178  dvasinbx  46185  dvnmptconst  46206  dvnxpaek  46207  itgiccshift  46245  itgperiod  46246  itgsbtaddcnst  46247  stirlinglem7  46345  dirkertrigeqlem2  46364  fourierdlem59  46430  fourierdlem62  46433  fourierdlem74  46445  fourierdlem75  46446  sqwvfoura  46493  fouriersw  46496  etransclem20  46519  etransclem21  46520  etransclem22  46521  etransclem25  46524  etransclem35  46534  sge0z  46640  ovnhoilem1  46866  vonsn  46956  lambert0  47154  0nodd  48437  fdivmptf  48808  nn0sumshdiglem2  48889  eenglngeehlnmlem2  49005  itsclc0yqsollem1  49029