Theorem 0cnd 11172

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℂcc 11071  0cc0 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-i2m1 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  addeq0  11610  mul0or  11827  eqneg  11911  un0addcl  12514  un0mulcl  12515  modsumfzodifsn  13957  muldivbinom2  14276  reusq0  15492  clim0c  15534  rlim0  15535  rlim0lt  15536  rlimneg  15674  isercolllem3  15694  sumrblem  15738  summolem2a  15742  sumz  15749  fsumcl  15760  expcnv  15894  ntrivcvgfvn0  15929  ef4p  16145  sadadd2lem2  16484  sadadd2lem  16493  modprm0  16841  iserodd  16871  prmrec  16958  4sqlem10  16983  4sqlem11  16991  frgpnabllem1  19913  evlsvvval  22146  fsumcn  24932  cnheibor  25017  evth2  25022  rrxmval  25467  mbfmulc2lem  25709  mbfpos  25713  dvcnp2  25982  dvcmulf  26007  dvmptc  26020  dvmptcmul  26026  dvmptfsum  26037  dveflem  26041  dvef  26042  rolle  26052  elply2  26256  plyf  26258  elplyr  26261  elplyd  26262  ply1term  26264  ply0  26268  plyeq0  26271  plyaddlem  26275  plymullem  26276  dgrlem  26289  coeidlem  26297  plyco  26301  coeeq2  26302  coe0  26316  plycj  26337  coecj  26338  plycjOLD  26339  coecjOLD  26340  plymul0or  26342  dvply1  26348  fta1lem  26371  elqaalem3  26385  tayl0  26425  dvtaylp  26433  taylthlem2  26437  radcnv0  26479  pserdvlem2  26491  pserdv  26492  ptolemy  26561  advlog  26719  advlogexp  26720  efopnlem2  26722  efopn  26723  logtayllem  26724  logtayl  26725  loglesqrt  26826  affineequiv  26888  quad2  26904  dcubic  26911  asinlem  26933  dvatan  27000  leibpilem2  27006  leibpi  27007  rlimcnp  27030  efrlim  27034  emcllem7  27066  dmgmaddn0  27087  lgamgulmlem2  27094  igamf  27115  igamcl  27116  sqff1o  27246  dchrelbasd  27303  dchrsum2  27332  sumdchr2  27334  addsq2reu  27504  addsqnreup  27507  dchrvmasumiflem2  27566  occllem  31506  nlelchi  32264  divnumden2  33018  fprodeq02  33026  gsumind  33531  constrrtcc  34032  constrsslem  34038  constraddcl  34059  constrmulcl  34068  cos9thpiminplylem1  34079  cos9thpiminplylem3  34081  cos9thpinconstrlem1  34086  ballotlemic  34804  ballotlem1c  34805  signsvfn  34876  circlemeth  34934  elmrsubrn  35870  climlec3  36084  bj-bary1lem  37802  tan2h  38111  ftc1anclem5  38196  ftc1anclem6  38197  ftc1anclem7  38198  ftc1anclem8  38199  ftc1anc  38200  lcmineqlem7  42652  lcmineqlem12  42657  aks4d1p1p7  42691  aks6d1c2p2  42736  aks6d1c5lem1  42753  aks6d1c5lem2  42755  sticksstones10  42772  sticksstones12a  42774  sn-addlid  43013  remul02  43014  remul01  43016  sn-it0e0  43025  sn-addrid  43030  sn-addid0  43034  sn-mul01  43035  sn-0tie0  43073  sn-mul02  43074  3cubeslem1  43265  pell14qrgt0  43436  expgrowth  44911  binomcxplemnotnn0  44932  ellimcabssub0  46193  0ellimcdiv  46223  clim0cf  46228  cosknegpi  46443  fprodsubrecnncnvlem  46481  fprodaddrecnncnvlem  46483  dvsinax  46487  dvasinbx  46494  dvnmptconst  46515  dvnxpaek  46516  itgiccshift  46554  itgperiod  46555  itgsbtaddcnst  46556  stirlinglem7  46654  dirkertrigeqlem2  46673  fourierdlem59  46739  fourierdlem62  46742  fourierdlem74  46754  fourierdlem75  46755  sqwvfoura  46802  fouriersw  46805  etransclem20  46828  etransclem21  46829  etransclem22  46830  etransclem25  46833  etransclem35  46843  sge0z  46949  ovnhoilem1  47175  vonsn  47265  lambert0  47481  0nodd  48792  fdivmptf  49163  nn0sumshdiglem2  49244  eenglngeehlnmlem2  49360  itsclc0yqsollem1  49384