Theorem 1cnd 8238

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 8168	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8073  1c1 8076

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

This theorem is referenced by:  adddirp1d  8248  muladd11r  8377  muls1d  8639  recrecap  8931  rec11ap  8932  rec11rap  8933  rerecclap  8952  subrecap  9061  recp1lt1  9121  nn1m1nn  9203  add1p1  9436  sub1m1  9437  cnm2m1cnm3  9438  xp1d2m1eqxm1d2  9439  div4p1lem1div2  9440  peano2z  9559  zaddcllempos  9560  peano2zm  9561  zaddcllemneg  9562  nn0n0n1ge2  9594  zneo  9625  peano5uzti  9632  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  nnsplit  10417  zpnn0elfzo1  10499  ubmelm1fzo  10517  fzosplitpr  10525  fzoshftral  10530  exbtwnzlemstep  10553  rebtwn2zlemstep  10558  qbtwnrelemcalc  10561  flqaddz  10603  2tnp1ge0ge0  10607  ceiqm1l  10619  qnegmod  10677  addmodlteq  10706  uzsinds  10752  seq3shft2  10789  iseqf1olemab  10810  exp3val  10849  binom2sub1  10962  binom3  10965  zesq  10966  sqoddm1div8  11001  nn0opthlem1d  11028  bcm1k  11068  bcp1n  11069  bcp1m1  11073  bcpasc  11074  bcn2m1  11077  omgadd  11111  hashfz  11131  hashfzo  11132  hashfzp1  11134  zfz1isolemsplit  11148  zfz1isolem1  11150  lswccatn0lsw  11237  ccatws1lenp1bg  11261  lswccats1  11269  resqrexlemover  11633  absexpzap  11703  reccn2ap  11936  hashiun  12102  hash2iun1dif1  12104  binomlem  12107  bcxmas  12113  arisum  12122  arisum2  12123  trireciplem  12124  geosergap  12130  pwm1geoserap1  12132  geolim  12135  geolim2  12136  georeclim  12137  geoisum1c  12144  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemsumlt  12152  cvgratz  12156  mertenslemi1  12159  prodf1f  12167  prodfrecap  12170  ntrivcvgap  12172  prodrbdclem  12195  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodntrivap  12208  prod1dc  12210  fprodmul  12215  prodsnf  12216  fprodsplitdc  12220  fprodm1  12222  fprodp1  12224  fprodcl  12231  fprodfac  12239  fprodrec  12253  fprodclf  12259  ef0lem  12284  efsub  12305  tanaddaplem  12362  tanaddap  12363  cos01bnd  12382  zeo3  12492  oddm1even  12499  oddp1even  12500  oexpneg  12501  ltoddhalfle  12517  halfleoddlt  12518  nn0ob  12532  flodddiv4  12560  bitsp1o  12577  bezoutlema  12633  bezoutlemb  12634  uzwodc  12671  qredeu  12732  prmdiv  12870  prmdiveq  12871  pc2dvds  12966  4sqlem11  13037  4sqlem12  13038  oddennn  13076  ennnfonelemp1  13090  gsumfzconst  13991  gsumsplit0  13996  cncrng  14648  expcn  15363  hoverb  15442  dveflem  15520  dvef  15521  dvply2g  15560  reeff1oleme  15566  sin0pilem1  15575  logdivlti  15675  rpcxpmul2  15707  rplogbval  15739  perfectlem2  15797  lgsvalmod  15821  lgsdir2  15835  lgsdir  15837  gausslemma2dlem1a  15860  gausslemma2dlem5  15868  lgseisenlem4  15875  lgsquadlem1  15879  m1lgs  15887  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgslem3d1  15902  2lgsoddprmlem1  15907  2sqlem8  15925  wlklenvclwlk  16297  clwwlkccatlem  16324  clwwlkext2edg  16346  clwwlknonex2lem1  16361  clwwlknonex2lem2  16362  cvgcmp2nlemabs  16747  iooref1o  16749  trilpolemeq1  16755  trilpolemlt1  16756  apdifflemr  16762  qdiff  16764  iswomni0  16767  nconstwlpolemgt0  16780  gsumgfsumlem  16795  gsumgfsum  16796