Theorem 0cnd 10033

Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0cnd	⊢ (𝜑 → 0 ∈ ℂ)

Proof of Theorem 0cnd

Step	Hyp	Ref	Expression
1		0cn 10032	. 2 ⊢ 0 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1990  ℂcc 9934  0cc0 9936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-i2m1 10004

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  mul0or  10667  diveq0  10695  eqneg  10745  un0addcl  11326  un0mulcl  11327  modsumfzodifsn  12743  muldivbinom2  13047  repswcshw  13558  clim0c  14238  rlim0  14239  rlim0lt  14240  rlimneg  14377  isercolllem3  14397  sumrblem  14442  summolem2a  14446  sumz  14453  fsumcl  14464  expcnv  14596  ntrivcvgfvn0  14631  ef4p  14843  sadadd2lem2  15172  sadadd2lem  15181  modprm0  15510  iserodd  15540  prmrec  15626  4sqlem10  15651  4sqlem11  15659  frgpnabllem1  18276  fsumcn  22673  cnheibor  22754  evth2  22759  rrxmval  23188  mbfmulc2lem  23414  mbfpos  23418  dvcmulf  23708  dvmptc  23721  dvmptcmul  23727  dvmptfsum  23738  dveflem  23742  rolle  23753  elply2  23952  plyf  23954  elplyr  23957  elplyd  23958  ply1term  23960  ply0  23964  plyeq0  23967  plyaddlem  23971  plymullem  23972  dgrlem  23985  coeidlem  23993  plyco  23997  coeeq2  23998  coe0  24012  plycj  24033  coecj  24034  plymul0or  24036  dvply1  24039  fta1lem  24062  elqaalem3  24076  tayl0  24116  dvtaylp  24124  taylthlem2  24128  radcnv0  24170  pserdvlem2  24182  pserdv  24183  ptolemy  24248  advlog  24400  advlogexp  24401  efopnlem2  24403  efopn  24404  logtayllem  24405  logtayl  24406  loglesqrt  24499  affineequiv  24553  quad2  24566  dcubic  24573  asinlem  24595  dvatan  24662  leibpilem2  24668  leibpi  24669  rlimcnp  24692  efrlim  24696  emcllem7  24728  dmgmaddn0  24749  lgamgulmlem2  24756  igamf  24777  igamcl  24778  sqff1o  24908  dchrelbasd  24964  dchrsum2  24993  sumdchr2  24995  dchrvmasumiflem2  25191  occllem  28162  nlelchi  28920  addeq0  29510  divnumden2  29564  fprodeq02  29569  ballotlemic  30568  ballotlem1c  30569  signsvfn  30659  circlemeth  30718  elmrsubrn  31417  climlec3  31619  bj-bary1lem  33160  tan2h  33401  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  pell14qrgt0  37423  expgrowth  38534  binomcxplemnotnn0  38555  ellimcabssub0  39849  0ellimcdiv  39881  clim0cf  39886  cosknegpi  40080  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvsinax  40127  dvasinbx  40135  dvnmptconst  40156  dvnxpaek  40157  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stirlinglem7  40297  dirkertrigeqlem2  40316  fourierdlem59  40382  fourierdlem62  40385  fourierdlem74  40397  fourierdlem75  40398  sqwvfoura  40445  fouriersw  40448  etransclem20  40471  etransclem21  40472  etransclem22  40473  etransclem25  40476  etransclem35  40486  sge0z  40592  ovnhoilem1  40815  vonsn  40905  0nodd  41810  fdivmptf  42335  nn0sumshdiglem2  42416