Theorem 0cnd 11243

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℂcc 11142  0cc0 11144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-mulcl 11206  ax-i2m1 11212

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2719  df-clel 2805

This theorem is referenced by:  addeq0  11673  mul0or  11890  diveq0  11918  eqneg  11970  un0addcl  12541  un0mulcl  12542  modsumfzodifsn  13947  muldivbinom2  14260  reusq0  15447  clim0c  15489  rlim0  15490  rlim0lt  15491  rlimneg  15631  isercolllem3  15651  sumrblem  15695  summolem2a  15699  sumz  15706  fsumcl  15717  expcnv  15848  ntrivcvgfvn0  15883  ef4p  16095  sadadd2lem2  16430  sadadd2lem  16439  modprm0  16779  iserodd  16809  prmrec  16896  4sqlem10  16921  4sqlem11  16929  frgpnabllem1  19833  fsumcn  24806  cnheibor  24899  evth2  24904  rrxmval  25351  mbfmulc2lem  25594  mbfpos  25598  dvcnp2  25867  dvcmulf  25894  dvmptc  25908  dvmptcmul  25914  dvmptfsum  25925  dveflem  25929  dvef  25930  rolle  25940  elply2  26148  plyf  26150  elplyr  26153  elplyd  26154  ply1term  26156  ply0  26160  plyeq0  26163  plyaddlem  26167  plymullem  26168  dgrlem  26181  coeidlem  26189  plyco  26193  coeeq2  26194  coe0  26208  plycj  26230  coecj  26231  plymul0or  26233  dvply1  26236  fta1lem  26260  elqaalem3  26274  tayl0  26314  dvtaylp  26323  taylthlem2  26327  taylthlem2OLD  26328  radcnv0  26370  pserdvlem2  26383  pserdv  26384  ptolemy  26449  advlog  26606  advlogexp  26607  efopnlem2  26609  efopn  26610  logtayllem  26611  logtayl  26612  loglesqrt  26711  affineequiv  26773  quad2  26789  dcubic  26796  asinlem  26818  dvatan  26885  leibpilem2  26891  leibpi  26892  rlimcnp  26915  efrlim  26919  efrlimOLD  26920  emcllem7  26952  dmgmaddn0  26973  lgamgulmlem2  26980  igamf  27001  igamcl  27002  sqff1o  27132  dchrelbasd  27190  dchrsum2  27219  sumdchr2  27221  addsq2reu  27391  addsqnreup  27394  dchrvmasumiflem2  27453  occllem  31131  nlelchi  31889  divnumden2  32599  fprodeq02  32604  ballotlemic  34131  ballotlem1c  34132  signsvfn  34219  circlemeth  34277  elmrsubrn  35135  climlec3  35333  bj-bary1lem  36794  tan2h  37090  ftc1anclem5  37175  ftc1anclem6  37176  ftc1anclem7  37177  ftc1anclem8  37178  ftc1anc  37179  lcmineqlem7  41510  lcmineqlem12  41515  aks4d1p1p7  41549  aks6d1c2p2  41594  aks6d1c5lem1  41611  aks6d1c5lem2  41613  sticksstones10  41631  sticksstones12a  41633  evlsvvval  41799  sn-addlid  41962  remul02  41963  remul01  41965  sn-it0e0  41973  sn-addrid  41978  sn-addid0  41982  sn-mul01  41983  sn-0tie0  41997  sn-mul02  41998  3cubeslem1  42107  pell14qrgt0  42282  expgrowth  43775  binomcxplemnotnn0  43796  ellimcabssub0  45007  0ellimcdiv  45039  clim0cf  45044  cosknegpi  45259  fprodsubrecnncnvlem  45297  fprodaddrecnncnvlem  45299  dvsinax  45303  dvasinbx  45310  dvnmptconst  45331  dvnxpaek  45332  itgiccshift  45370  itgperiod  45371  itgsbtaddcnst  45372  stirlinglem7  45470  dirkertrigeqlem2  45489  fourierdlem59  45555  fourierdlem62  45558  fourierdlem74  45570  fourierdlem75  45571  sqwvfoura  45618  fouriersw  45621  etransclem20  45644  etransclem21  45645  etransclem22  45646  etransclem25  45649  etransclem35  45659  sge0z  45765  ovnhoilem1  45991  vonsn  46081  0nodd  47283  fdivmptf  47665  nn0sumshdiglem2  47746  eenglngeehlnmlem2  47862  itsclc0yqsollem1  47886

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »