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  9691  zaddcllempos  9692  peano2zm  9693  zaddcllemneg  9694  nn0n0n1ge2  9726  zneo  9758  peano5uzti  9765  ltesubnnd  10187  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  fzsplit3  10475  nnsplit  10561  zpnn0elfzo1  10643  ubmelm1fzo  10661  fzosplitpr  10669  fzoshftral  10674  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  qbtwnrelemcalc  10707  flqaddz  10753  2tnp1ge0ge0  10757  ceiqm1l  10769  qnegmod  10827  addmodlteq  10856  uzsinds  10902  seq3shft2  10939  iseqf1olemab  10960  exp3val  10999  binom2sub1  11112  binom3  11115  zesq  11117  sqoddm1div8  11152  nn0opthlem1d  11180  bcm1k  11220  bcp1n  11221  bcp1m1  11225  bcpasc  11226  bcm1n  11229  bcn2m1  11230  omgadd  11264  hashfz  11284  hashfzo  11285  hashfzp1  11287  hashf1lem2  11308  hashf1  11309  zfz1isolemsplit  11312  zfz1isolem1  11314  lswccatn0lsw  11401  ccatws1lenp1bg  11425  lswccats1  11433  sq01  11682  resqrexlemover  11798  absexpzap  11869  reccn2ap  12104  hashiun  12270  hash2iun1dif1  12272  binomlem  12275  bcxmas  12281  arisum  12290  arisum2  12291  trireciplem  12292  geosergap  12298  pwm1geoserap1  12300  geolim  12303  geolim2  12304  georeclim  12305  geoisum1c  12312  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemsumlt  12320  cvgratz  12324  mertenslemi1  12327  prodf1f  12335  prodfrecap  12338  ntrivcvgap  12340  prodrbdclem  12363  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodntrivap  12376  prod1dc  12378  fprodmul  12383  prodsnf  12384  fprodsplitdc  12388  fprodm1  12390  fprodp1  12392  fprodcl  12399  fprodfac  12407  fprodrec  12421  fprodclf  12427  ef0lem  12452  efsub  12473  tanaddaplem  12530  tanaddap  12531  cos01bnd  12550  zeo3  12660  oddm1even  12667  oddp1even  12668  oexpneg  12669  ltoddhalfle  12685  halfleoddlt  12686  nn0ob  12700  flodddiv4  12728  bitsp1o  12745  bezoutlema  12801  bezoutlemb  12802  uzwodc  12839  qredeu  12900  prmdiv  13042  prmdiveq  13043  pc2dvds  13138  4sqlem11  13209  4sqlem12  13210  ballotfilemfp1  13289  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemsgt1  13312  ballotfilemsdom  13313  ballotfilemsel1i  13314  ballotfilemsi  13316  ballotfilemsima  13317  ballotfilem1ri  13336  oddennn  13341  ennnfonelemp1  13355  gzsumconst  14233  gzsumsplit0  14238  gzsumshift  14239  gzsumgsum  14245  cncrng  15015  expcn  15795  hoverb  15874  dveflem  15952  dvef  15953  dvply2g  15992  reeff1oleme  15998  efap1p  16005  sin0pilem1  16008  logdivlti  16111  logdivlt  16124  rpcxpmul2  16146  rplogbval  16181  birthdaylem2  16226  perfectlem2  16300  bcmono  16304  bcp1ctr  16306  bclbnd  16307  bposlem9  16319  lgsvalmod  16343  lgsdir2  16357  lgsdir  16359  gausslemma2dlem1a  16382  gausslemma2dlem5  16390  lgseisenlem4  16397  lgsquadlem1  16401  m1lgs  16409  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3d1  16424  2lgsoddprmlem1  16429  2sqlem8  16447  wlklenvclwlk  16819  clwwlkccatlem  16846  clwwlkext2edg  16868  clwwlknonex2lem1  16883  clwwlknonex2lem2  16884  cvgcmp2nlemabs  17287  iooref1o  17289  trilpolemeq1  17296  trilpolemlt1  17297  apdifflemr  17303  qdiff  17305  iswomni0  17308  nconstwlpolemgt0  17321