Theorem 0cnd 11108

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  0cc0 11009

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-i2m1 11077

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

This theorem is referenced by:  addeq0  11543  mul0or  11760  eqneg  11844  un0addcl  12417  un0mulcl  12418  modsumfzodifsn  13851  muldivbinom2  14170  reusq0  15372  clim0c  15414  rlim0  15415  rlim0lt  15416  rlimneg  15554  isercolllem3  15574  sumrblem  15618  summolem2a  15622  sumz  15629  fsumcl  15640  expcnv  15771  ntrivcvgfvn0  15806  ef4p  16022  sadadd2lem2  16361  sadadd2lem  16370  modprm0  16717  iserodd  16747  prmrec  16834  4sqlem10  16859  4sqlem11  16867  frgpnabllem1  19752  fsumcn  24759  cnheibor  24852  evth2  24857  rrxmval  25303  mbfmulc2lem  25546  mbfpos  25550  dvcnp2  25819  dvcmulf  25846  dvmptc  25860  dvmptcmul  25866  dvmptfsum  25877  dveflem  25881  dvef  25882  rolle  25892  elply2  26099  plyf  26101  elplyr  26104  elplyd  26105  ply1term  26107  ply0  26111  plyeq0  26114  plyaddlem  26118  plymullem  26119  dgrlem  26132  coeidlem  26140  plyco  26144  coeeq2  26145  coe0  26159  plycj  26181  coecj  26182  plycjOLD  26183  coecjOLD  26184  plymul0or  26186  dvply1  26189  fta1lem  26213  elqaalem3  26227  tayl0  26267  dvtaylp  26276  taylthlem2  26280  taylthlem2OLD  26281  radcnv0  26323  pserdvlem2  26336  pserdv  26337  ptolemy  26403  advlog  26561  advlogexp  26562  efopnlem2  26564  efopn  26565  logtayllem  26566  logtayl  26567  loglesqrt  26669  affineequiv  26731  quad2  26747  dcubic  26754  asinlem  26776  dvatan  26843  leibpilem2  26849  leibpi  26850  rlimcnp  26873  efrlim  26877  efrlimOLD  26878  emcllem7  26910  dmgmaddn0  26931  lgamgulmlem2  26938  igamf  26959  igamcl  26960  sqff1o  27090  dchrelbasd  27148  dchrsum2  27177  sumdchr2  27179  addsq2reu  27349  addsqnreup  27352  dchrvmasumiflem2  27411  occllem  31247  nlelchi  32005  divnumden2  32761  fprodeq02  32769  constrrtcc  33708  constrsslem  33714  constraddcl  33735  constrmulcl  33744  cos9thpiminplylem1  33755  cos9thpiminplylem3  33757  cos9thpinconstrlem1  33762  ballotlemic  34481  ballotlem1c  34482  signsvfn  34556  circlemeth  34614  elmrsubrn  35503  climlec3  35717  bj-bary1lem  37294  tan2h  37602  ftc1anclem5  37687  ftc1anclem6  37688  ftc1anclem7  37689  ftc1anclem8  37690  ftc1anc  37691  lcmineqlem7  42018  lcmineqlem12  42023  aks4d1p1p7  42057  aks6d1c2p2  42102  aks6d1c5lem1  42119  aks6d1c5lem2  42121  sticksstones10  42138  sticksstones12a  42140  sn-addlid  42387  remul02  42388  remul01  42390  sn-it0e0  42399  sn-addrid  42404  sn-addid0  42408  sn-mul01  42409  sn-0tie0  42434  sn-mul02  42435  evlsvvval  42546  3cubeslem1  42667  pell14qrgt0  42842  expgrowth  44318  binomcxplemnotnn0  44339  ellimcabssub0  45608  0ellimcdiv  45640  clim0cf  45645  cosknegpi  45860  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  dvsinax  45904  dvasinbx  45911  dvnmptconst  45932  dvnxpaek  45933  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  stirlinglem7  46071  dirkertrigeqlem2  46090  fourierdlem59  46156  fourierdlem62  46159  fourierdlem74  46171  fourierdlem75  46172  sqwvfoura  46219  fouriersw  46222  etransclem20  46245  etransclem21  46246  etransclem22  46247  etransclem25  46250  etransclem35  46260  sge0z  46366  ovnhoilem1  46592  vonsn  46682  lambert0  46881  0nodd  48164  fdivmptf  48536  nn0sumshdiglem2  48617  eenglngeehlnmlem2  48733  itsclc0yqsollem1  48757