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 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11125  0cc0 11127

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

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

This theorem is referenced by:  addeq0  11658  mul0or  11875  eqneg  11959  un0addcl  12532  un0mulcl  12533  modsumfzodifsn  13960  muldivbinom2  14279  reusq0  15479  clim0c  15521  rlim0  15522  rlim0lt  15523  rlimneg  15661  isercolllem3  15681  sumrblem  15725  summolem2a  15729  sumz  15736  fsumcl  15747  expcnv  15878  ntrivcvgfvn0  15913  ef4p  16129  sadadd2lem2  16467  sadadd2lem  16476  modprm0  16823  iserodd  16853  prmrec  16940  4sqlem10  16965  4sqlem11  16973  frgpnabllem1  19852  fsumcn  24810  cnheibor  24903  evth2  24908  rrxmval  25355  mbfmulc2lem  25598  mbfpos  25602  dvcnp2  25871  dvcmulf  25898  dvmptc  25912  dvmptcmul  25918  dvmptfsum  25929  dveflem  25933  dvef  25934  rolle  25944  elply2  26151  plyf  26153  elplyr  26156  elplyd  26157  ply1term  26159  ply0  26163  plyeq0  26166  plyaddlem  26170  plymullem  26171  dgrlem  26184  coeidlem  26192  plyco  26196  coeeq2  26197  coe0  26211  plycj  26233  coecj  26234  plycjOLD  26235  coecjOLD  26236  plymul0or  26238  dvply1  26241  fta1lem  26265  elqaalem3  26279  tayl0  26319  dvtaylp  26328  taylthlem2  26332  taylthlem2OLD  26333  radcnv0  26375  pserdvlem2  26388  pserdv  26389  ptolemy  26455  advlog  26613  advlogexp  26614  efopnlem2  26616  efopn  26617  logtayllem  26618  logtayl  26619  loglesqrt  26721  affineequiv  26783  quad2  26799  dcubic  26806  asinlem  26828  dvatan  26895  leibpilem2  26901  leibpi  26902  rlimcnp  26925  efrlim  26929  efrlimOLD  26930  emcllem7  26962  dmgmaddn0  26983  lgamgulmlem2  26990  igamf  27011  igamcl  27012  sqff1o  27142  dchrelbasd  27200  dchrsum2  27229  sumdchr2  27231  addsq2reu  27401  addsqnreup  27404  dchrvmasumiflem2  27463  occllem  31230  nlelchi  31988  divnumden2  32740  fprodeq02  32748  constrrtcc  33715  constrsslem  33721  constraddcl  33742  constrmulcl  33751  cos9thpiminplylem1  33762  cos9thpiminplylem3  33764  cos9thpinconstrlem1  33769  ballotlemic  34485  ballotlem1c  34486  signsvfn  34560  circlemeth  34618  elmrsubrn  35488  climlec3  35697  bj-bary1lem  37274  tan2h  37582  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  lcmineqlem7  41994  lcmineqlem12  41999  aks4d1p1p7  42033  aks6d1c2p2  42078  aks6d1c5lem1  42095  aks6d1c5lem2  42097  sticksstones10  42114  sticksstones12a  42116  sn-addlid  42394  remul02  42395  remul01  42397  sn-it0e0  42405  sn-addrid  42410  sn-addid0  42414  sn-mul01  42415  sn-0tie0  42429  sn-mul02  42430  evlsvvval  42533  3cubeslem1  42654  pell14qrgt0  42829  expgrowth  44307  binomcxplemnotnn0  44328  ellimcabssub0  45594  0ellimcdiv  45626  clim0cf  45631  cosknegpi  45846  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  dvsinax  45890  dvasinbx  45897  dvnmptconst  45918  dvnxpaek  45919  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stirlinglem7  46057  dirkertrigeqlem2  46076  fourierdlem59  46142  fourierdlem62  46145  fourierdlem74  46157  fourierdlem75  46158  sqwvfoura  46205  fouriersw  46208  etransclem20  46231  etransclem21  46232  etransclem22  46233  etransclem25  46236  etransclem35  46246  sge0z  46352  ovnhoilem1  46578  vonsn  46668  lambert0  46867  0nodd  48093  fdivmptf  48469  nn0sumshdiglem2  48550  eenglngeehlnmlem2  48666  itsclc0yqsollem1  48690