Theorem 1cnd 8173

Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

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

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 8103	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8008  1c1 8011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 8103

This theorem is referenced by:  adddirp1d  8184  muladd11r  8313  muls1d  8575  recrecap  8867  rec11ap  8868  rec11rap  8869  rerecclap  8888  subrecap  8997  recp1lt1  9057  nn1m1nn  9139  add1p1  9372  sub1m1  9373  cnm2m1cnm3  9374  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  peano2z  9493  zaddcllempos  9494  peano2zm  9495  zaddcllemneg  9496  nn0n0n1ge2  9528  zneo  9559  peano5uzti  9566  lincmb01cmp  10211  iccf1o  10212  nnsplit  10345  zpnn0elfzo1  10426  ubmelm1fzo  10444  fzoshftral  10456  exbtwnzlemstep  10479  rebtwn2zlemstep  10484  qbtwnrelemcalc  10487  flqaddz  10529  2tnp1ge0ge0  10533  ceiqm1l  10545  qnegmod  10603  addmodlteq  10632  uzsinds  10678  seq3shft2  10715  iseqf1olemab  10736  exp3val  10775  binom2sub1  10888  binom3  10891  zesq  10892  sqoddm1div8  10927  nn0opthlem1d  10954  bcm1k  10994  bcp1n  10995  bcp1m1  10999  bcpasc  11000  bcn2m1  11003  omgadd  11036  hashfz  11056  hashfzo  11057  hashfzp1  11059  zfz1isolemsplit  11073  zfz1isolem1  11075  lswccatn0lsw  11159  ccatws1lenp1bg  11183  lswccats1  11189  resqrexlemover  11536  absexpzap  11606  reccn2ap  11839  hashiun  12004  hash2iun1dif1  12006  binomlem  12009  bcxmas  12015  arisum  12024  arisum2  12025  trireciplem  12026  geosergap  12032  pwm1geoserap1  12034  geolim  12037  geolim2  12038  georeclim  12039  geoisum1c  12046  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  cvgratnnlemsumlt  12054  cvgratz  12058  mertenslemi1  12061  prodf1f  12069  prodfrecap  12072  ntrivcvgap  12074  prodrbdclem  12097  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prod1dc  12112  fprodmul  12117  prodsnf  12118  fprodsplitdc  12122  fprodm1  12124  fprodp1  12126  fprodcl  12133  fprodfac  12141  fprodrec  12155  fprodclf  12161  ef0lem  12186  efsub  12207  tanaddaplem  12264  tanaddap  12265  cos01bnd  12284  zeo3  12394  oddm1even  12401  oddp1even  12402  oexpneg  12403  ltoddhalfle  12419  halfleoddlt  12420  nn0ob  12434  flodddiv4  12462  bitsp1o  12479  bezoutlema  12535  bezoutlemb  12536  uzwodc  12573  qredeu  12634  prmdiv  12772  prmdiveq  12773  pc2dvds  12868  4sqlem11  12939  4sqlem12  12940  oddennn  12978  ennnfonelemp1  12992  gsumfzconst  13893  cncrng  14548  expcn  15258  hoverb  15337  dveflem  15415  dvef  15416  dvply2g  15455  reeff1oleme  15461  sin0pilem1  15470  logdivlti  15570  rpcxpmul2  15602  rplogbval  15634  perfectlem2  15689  lgsvalmod  15713  lgsdir2  15727  lgsdir  15729  gausslemma2dlem1a  15752  gausslemma2dlem5  15760  lgseisenlem4  15767  lgsquadlem1  15771  m1lgs  15779  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgslem3d1  15794  2lgsoddprmlem1  15799  2sqlem8  15817  wlklenvclwlk  16114  clwwlkccatlem  16137  cvgcmp2nlemabs  16460  iooref1o  16462  trilpolemeq1  16468  trilpolemlt1  16469  apdifflemr  16475  iswomni0  16479  nconstwlpolemgt0  16492