Theorem 1cnd 8348

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

Assertion

Ref	Expression
1cnd	|- ( ph -> 1 e. CC )

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 8278	. 2 |- 1 e. CC
2	1	a1i 9	1 |- ( ph -> 1 e. CC )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8183   1c1 8186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-1cn 8278

This theorem is used by:  adddirp1d  8358  muladd11r  8489  muls1d  8752  recrecap  9047  rec11ap  9048  rec11rap  9049  rerecclap  9068  subrecap  9177  recp1lt1  9237  nn1m1nn  9331  add1p1  9566  sub1m1  9567  cnm2m1cnm3  9568  xp1d2m1eqxm1d2  9569  div4p1lem1div2  9570  peano2z  9689  zaddcllempos  9690  peano2zm  9691  zaddcllemneg  9692  nn0n0n1ge2  9724  zneo  9757  peano5uzti  9764  ltesubnnd  10186  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  fzsplit3  10474  nnsplit  10560  zpnn0elfzo1  10642  ubmelm1fzo  10660  fzosplitpr  10668  fzoshftral  10673  exbtwnzlemstep  10698  rebtwn2zlemstep  10703  qbtwnrelemcalc  10706  flqaddz  10752  2tnp1ge0ge0  10756  ceiqm1l  10768  qnegmod  10826  addmodlteq  10855  uzsinds  10901  seq3shft2  10938  iseqf1olemab  10959  exp3val  10998  binom2sub1  11111  binom3  11114  zesq  11116  sqoddm1div8  11151  nn0opthlem1d  11179  bcm1k  11219  bcp1n  11220  bcp1m1  11224  bcpasc  11225  bcm1n  11228  bcn2m1  11229  omgadd  11263  hashfz  11283  hashfzo  11284  hashfzp1  11286  hashf1lem2  11307  hashf1  11308  zfz1isolemsplit  11311  zfz1isolem1  11313  lswccatn0lsw  11400  ccatws1lenp1bg  11424  lswccats1  11432  sq01  11681  resqrexlemover  11797  absexpzap  11868  reccn2ap  12103  hashiun  12269  hash2iun1dif1  12271  binomlem  12274  bcxmas  12280  arisum  12289  arisum2  12290  trireciplem  12291  geosergap  12297  pwm1geoserap1  12299  geolim  12302  geolim2  12303  georeclim  12304  geoisum1c  12311  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemsumlt  12319  cvgratz  12323  mertenslemi1  12326  prodf1f  12334  prodfrecap  12337  ntrivcvgap  12339  prodrbdclem  12362  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodntrivap  12375  prod1dc  12377  fprodmul  12382  prodsnf  12383  fprodsplitdc  12387  fprodm1  12389  fprodp1  12391  fprodcl  12398  fprodfac  12406  fprodrec  12420  fprodclf  12426  ef0lem  12451  efsub  12472  tanaddaplem  12529  tanaddap  12530  cos01bnd  12549  zeo3  12659  oddm1even  12666  oddp1even  12667  oexpneg  12668  ltoddhalfle  12684  halfleoddlt  12685  nn0ob  12699  flodddiv4  12727  bitsp1o  12744  bezoutlema  12800  bezoutlemb  12801  uzwodc  12838  qredeu  12899  prmdiv  13041  prmdiveq  13042  pc2dvds  13137  4sqlem11  13208  4sqlem12  13209  ballotfilemfp1  13288  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsgt1  13311  ballotfilemsdom  13312  ballotfilemsel1i  13313  ballotfilemsi  13315  ballotfilemsima  13316  ballotfilem1ri  13335  oddennn  13340  ennnfonelemp1  13354  gzsumconst  14232  gzsumsplit0  14237  gzsumshift  14238  gzsumgsum  14244  cncrng  15014  expcn  15812  hoverb  15891  dveflem  15969  dvef  15970  dvply2g  16009  reeff1oleme  16015  efap1p  16022  sin0pilem1  16025  logdivlti  16128  logdivlt  16141  rpcxpmul2  16163  rplogbval  16198  birthdaylem2  16243  perfectlem2  16317  bcmono  16321  bcp1ctr  16323  bclbnd  16324  bposlem9  16336  lgsvalmod  16360  lgsdir2  16374  lgsdir  16376  gausslemma2dlem1a  16399  gausslemma2dlem5  16407  lgseisenlem4  16414  lgsquadlem1  16418  m1lgs  16426  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgslem3d1  16441  2lgsoddprmlem1  16446  2sqlem8  16464  wlklenvclwlk  16836  clwwlkccatlem  16863  clwwlkext2edg  16885  clwwlknonex2lem1  16900  clwwlknonex2lem2  16901  cvgcmp2nlemabs  17304  iooref1o  17306  trilpolemeq1  17313  trilpolemlt1  17314  apdifflemr  17320  qdiff  17322  iswomni0  17325  nconstwlpolemgt0  17338