Theorem 1cnd 8343

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 8273	. 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 8178   1c1 8181

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

This theorem is used by:  adddirp1d  8353  muladd11r  8484  muls1d  8747  recrecap  9042  rec11ap  9043  rec11rap  9044  rerecclap  9063  subrecap  9172  recp1lt1  9232  nn1m1nn  9325  add1p1  9560  sub1m1  9561  cnm2m1cnm3  9562  xp1d2m1eqxm1d2  9563  div4p1lem1div2  9564  peano2z  9685  zaddcllempos  9686  peano2zm  9687  zaddcllemneg  9688  nn0n0n1ge2  9720  zneo  9752  peano5uzti  9759  ltesubnnd  10181  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  fzsplit3  10469  nnsplit  10555  zpnn0elfzo1  10637  ubmelm1fzo  10655  fzosplitpr  10663  fzoshftral  10668  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  qbtwnrelemcalc  10701  flqaddz  10747  2tnp1ge0ge0  10751  ceiqm1l  10763  qnegmod  10821  addmodlteq  10850  uzsinds  10896  seq3shft2  10933  iseqf1olemab  10954  exp3val  10993  binom2sub1  11106  binom3  11109  zesq  11111  sqoddm1div8  11146  nn0opthlem1d  11174  bcm1k  11214  bcp1n  11215  bcp1m1  11219  bcpasc  11220  bcm1n  11223  bcn2m1  11224  omgadd  11258  hashfz  11278  hashfzo  11279  hashfzp1  11281  hashf1lem2  11302  hashf1  11303  zfz1isolemsplit  11306  zfz1isolem1  11308  lswccatn0lsw  11395  ccatws1lenp1bg  11419  lswccats1  11427  sq01  11676  resqrexlemover  11792  absexpzap  11863  reccn2ap  12098  hashiun  12264  hash2iun1dif1  12266  binomlem  12269  bcxmas  12275  arisum  12284  arisum2  12285  trireciplem  12286  geosergap  12292  pwm1geoserap1  12294  geolim  12297  geolim2  12298  georeclim  12299  geoisum1c  12306  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemsumlt  12314  cvgratz  12318  mertenslemi1  12321  prodf1f  12329  prodfrecap  12332  ntrivcvgap  12334  prodrbdclem  12357  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodntrivap  12370  prod1dc  12372  fprodmul  12377  prodsnf  12378  fprodsplitdc  12382  fprodm1  12384  fprodp1  12386  fprodcl  12393  fprodfac  12401  fprodrec  12415  fprodclf  12421  ef0lem  12446  efsub  12467  tanaddaplem  12524  tanaddap  12525  cos01bnd  12544  zeo3  12654  oddm1even  12661  oddp1even  12662  oexpneg  12663  ltoddhalfle  12679  halfleoddlt  12680  nn0ob  12694  flodddiv4  12722  bitsp1o  12739  bezoutlema  12795  bezoutlemb  12796  uzwodc  12833  qredeu  12894  prmdiv  13036  prmdiveq  13037  pc2dvds  13132  4sqlem11  13203  4sqlem12  13204  ballotfilemfp1  13283  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsgt1  13306  ballotfilemsdom  13307  ballotfilemsel1i  13308  ballotfilemsi  13310  ballotfilemsima  13311  ballotfilem1ri  13330  oddennn  13335  ennnfonelemp1  13349  gzsumconst  14227  gzsumsplit0  14232  gzsumshift  14233  gzsumgsum  14239  cncrng  14990  expcn  15761  hoverb  15840  dveflem  15918  dvef  15919  dvply2g  15958  reeff1oleme  15964  efap1p  15971  sin0pilem1  15974  logdivlti  16075  logdivlt  16088  rpcxpmul2  16110  rplogbval  16142  birthdaylem2  16187  perfectlem2  16261  bcmono  16265  bcp1ctr  16267  bclbnd  16268  bposlem9  16280  lgsvalmod  16304  lgsdir2  16318  lgsdir  16320  gausslemma2dlem1a  16343  gausslemma2dlem5  16351  lgseisenlem4  16358  lgsquadlem1  16362  m1lgs  16370  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgslem3d1  16385  2lgsoddprmlem1  16390  2sqlem8  16408  wlklenvclwlk  16780  clwwlkccatlem  16807  clwwlkext2edg  16829  clwwlknonex2lem1  16844  clwwlknonex2lem2  16845  cvgcmp2nlemabs  17247  iooref1o  17249  trilpolemeq1  17256  trilpolemlt1  17257  apdifflemr  17263  qdiff  17265  iswomni0  17268  nconstwlpolemgt0  17281