Theorem 1cnd 8342

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 8272	. 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 8177   1c1 8180

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

This theorem is used by:  adddirp1d  8352  muladd11r  8483  muls1d  8746  recrecap  9041  rec11ap  9042  rec11rap  9043  rerecclap  9062  subrecap  9171  recp1lt1  9231  nn1m1nn  9324  add1p1  9559  sub1m1  9560  cnm2m1cnm3  9561  xp1d2m1eqxm1d2  9562  div4p1lem1div2  9563  peano2z  9684  zaddcllempos  9685  peano2zm  9686  zaddcllemneg  9687  nn0n0n1ge2  9719  zneo  9751  peano5uzti  9758  ltesubnnd  10180  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  fzsplit3  10468  nnsplit  10554  zpnn0elfzo1  10636  ubmelm1fzo  10654  fzosplitpr  10662  fzoshftral  10667  exbtwnzlemstep  10692  rebtwn2zlemstep  10697  qbtwnrelemcalc  10700  flqaddz  10745  2tnp1ge0ge0  10749  ceiqm1l  10761  qnegmod  10819  addmodlteq  10848  uzsinds  10894  seq3shft2  10931  iseqf1olemab  10952  exp3val  10991  binom2sub1  11104  binom3  11107  zesq  11109  sqoddm1div8  11144  nn0opthlem1d  11172  bcm1k  11212  bcp1n  11213  bcp1m1  11217  bcpasc  11218  bcm1n  11221  bcn2m1  11222  omgadd  11256  hashfz  11276  hashfzo  11277  hashfzp1  11279  hashf1lem2  11300  hashf1  11301  zfz1isolemsplit  11304  zfz1isolem1  11306  lswccatn0lsw  11393  ccatws1lenp1bg  11417  lswccats1  11425  sq01  11674  resqrexlemover  11790  absexpzap  11861  reccn2ap  12095  hashiun  12261  hash2iun1dif1  12263  binomlem  12266  bcxmas  12272  arisum  12281  arisum2  12282  trireciplem  12283  geosergap  12289  pwm1geoserap1  12291  geolim  12294  geolim2  12295  georeclim  12296  geoisum1c  12303  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemsumlt  12311  cvgratz  12315  mertenslemi1  12318  prodf1f  12326  prodfrecap  12329  ntrivcvgap  12331  prodrbdclem  12354  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodntrivap  12367  prod1dc  12369  fprodmul  12374  prodsnf  12375  fprodsplitdc  12379  fprodm1  12381  fprodp1  12383  fprodcl  12390  fprodfac  12398  fprodrec  12412  fprodclf  12418  ef0lem  12443  efsub  12464  tanaddaplem  12521  tanaddap  12522  cos01bnd  12541  zeo3  12651  oddm1even  12658  oddp1even  12659  oexpneg  12660  ltoddhalfle  12676  halfleoddlt  12677  nn0ob  12691  flodddiv4  12719  bitsp1o  12736  bezoutlema  12792  bezoutlemb  12793  uzwodc  12830  qredeu  12891  prmdiv  13033  prmdiveq  13034  pc2dvds  13129  4sqlem11  13200  4sqlem12  13201  ballotfilemfp1  13280  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsgt1  13303  ballotfilemsdom  13304  ballotfilemsel1i  13305  ballotfilemsi  13307  ballotfilemsima  13308  ballotfilem1ri  13327  oddennn  13332  ennnfonelemp1  13346  gzsumconst  14192  gzsumsplit0  14197  gzsumshift  14198  gzsumgsum  14204  cncrng  14955  expcn  15719  hoverb  15798  dveflem  15876  dvef  15877  dvply2g  15916  reeff1oleme  15922  efap1p  15929  sin0pilem1  15932  logdivlti  16033  logdivlt  16046  rpcxpmul2  16068  rplogbval  16100  birthdaylem2  16145  perfectlem2  16198  bcmono  16202  bcp1ctr  16204  bclbnd  16205  lgsvalmod  16236  lgsdir2  16250  lgsdir  16252  gausslemma2dlem1a  16275  gausslemma2dlem5  16283  lgseisenlem4  16290  lgsquadlem1  16294  m1lgs  16302  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgslem3d1  16317  2lgsoddprmlem1  16322  2sqlem8  16340  wlklenvclwlk  16712  clwwlkccatlem  16739  clwwlkext2edg  16761  clwwlknonex2lem1  16776  clwwlknonex2lem2  16777  cvgcmp2nlemabs  17179  iooref1o  17181  trilpolemeq1  17187  trilpolemlt1  17188  apdifflemr  17194  qdiff  17196  iswomni0  17199  nconstwlpolemgt0  17212