Theorem 0cnd 11254

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  0cc0 11155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  addeq0  11686  mul0or  11903  eqneg  11987  un0addcl  12559  un0mulcl  12560  modsumfzodifsn  13985  muldivbinom2  14302  reusq0  15501  clim0c  15543  rlim0  15544  rlim0lt  15545  rlimneg  15683  isercolllem3  15703  sumrblem  15747  summolem2a  15751  sumz  15758  fsumcl  15769  expcnv  15900  ntrivcvgfvn0  15935  ef4p  16149  sadadd2lem2  16487  sadadd2lem  16496  modprm0  16843  iserodd  16873  prmrec  16960  4sqlem10  16985  4sqlem11  16993  frgpnabllem1  19891  fsumcn  24894  cnheibor  24987  evth2  24992  rrxmval  25439  mbfmulc2lem  25682  mbfpos  25686  dvcnp2  25955  dvcmulf  25982  dvmptc  25996  dvmptcmul  26002  dvmptfsum  26013  dveflem  26017  dvef  26018  rolle  26028  elply2  26235  plyf  26237  elplyr  26240  elplyd  26241  ply1term  26243  ply0  26247  plyeq0  26250  plyaddlem  26254  plymullem  26255  dgrlem  26268  coeidlem  26276  plyco  26280  coeeq2  26281  coe0  26295  plycj  26317  coecj  26318  plycjOLD  26319  coecjOLD  26320  plymul0or  26322  dvply1  26325  fta1lem  26349  elqaalem3  26363  tayl0  26403  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  radcnv0  26459  pserdvlem2  26472  pserdv  26473  ptolemy  26538  advlog  26696  advlogexp  26697  efopnlem2  26699  efopn  26700  logtayllem  26701  logtayl  26702  loglesqrt  26804  affineequiv  26866  quad2  26882  dcubic  26889  asinlem  26911  dvatan  26978  leibpilem2  26984  leibpi  26985  rlimcnp  27008  efrlim  27012  efrlimOLD  27013  emcllem7  27045  dmgmaddn0  27066  lgamgulmlem2  27073  igamf  27094  igamcl  27095  sqff1o  27225  dchrelbasd  27283  dchrsum2  27312  sumdchr2  27314  addsq2reu  27484  addsqnreup  27487  dchrvmasumiflem2  27546  occllem  31322  nlelchi  32080  divnumden2  32817  fprodeq02  32825  constrrtcc  33776  constrsslem  33782  ballotlemic  34509  ballotlem1c  34510  signsvfn  34597  circlemeth  34655  elmrsubrn  35525  climlec3  35734  bj-bary1lem  37311  tan2h  37619  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  lcmineqlem7  42036  lcmineqlem12  42041  aks4d1p1p7  42075  aks6d1c2p2  42120  aks6d1c5lem1  42137  aks6d1c5lem2  42139  sticksstones10  42156  sticksstones12a  42158  sn-addlid  42434  remul02  42435  remul01  42437  sn-it0e0  42445  sn-addrid  42450  sn-addid0  42454  sn-mul01  42455  sn-0tie0  42469  sn-mul02  42470  evlsvvval  42573  3cubeslem1  42695  pell14qrgt0  42870  expgrowth  44354  binomcxplemnotnn0  44375  ellimcabssub0  45632  0ellimcdiv  45664  clim0cf  45669  cosknegpi  45884  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  dvsinax  45928  dvasinbx  45935  dvnmptconst  45956  dvnxpaek  45957  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stirlinglem7  46095  dirkertrigeqlem2  46114  fourierdlem59  46180  fourierdlem62  46183  fourierdlem74  46195  fourierdlem75  46196  sqwvfoura  46243  fouriersw  46246  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem25  46274  etransclem35  46284  sge0z  46390  ovnhoilem1  46616  vonsn  46706  0nodd  48086  fdivmptf  48462  nn0sumshdiglem2  48543  eenglngeehlnmlem2  48659  itsclc0yqsollem1  48683