Theorem 1cnd 8255

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 8185	. 2 |- 1 e. CC
2	1	a1i 9	1 |- ( ph -> 1 e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8090   1c1 8093

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

This theorem is referenced by:  adddirp1d  8265  muladd11r  8394  muls1d  8656  recrecap  8948  rec11ap  8949  rec11rap  8950  rerecclap  8969  subrecap  9078  recp1lt1  9138  nn1m1nn  9220  add1p1  9453  sub1m1  9454  cnm2m1cnm3  9455  xp1d2m1eqxm1d2  9456  div4p1lem1div2  9457  peano2z  9576  zaddcllempos  9577  peano2zm  9578  zaddcllemneg  9579  nn0n0n1ge2  9611  zneo  9642  peano5uzti  9649  lincmb01cmp  10299  lincmble  10300  iccf1o  10301  nnsplit  10434  zpnn0elfzo1  10516  ubmelm1fzo  10534  fzosplitpr  10542  fzoshftral  10547  exbtwnzlemstep  10570  rebtwn2zlemstep  10575  qbtwnrelemcalc  10578  flqaddz  10620  2tnp1ge0ge0  10624  ceiqm1l  10636  qnegmod  10694  addmodlteq  10723  uzsinds  10769  seq3shft2  10806  iseqf1olemab  10827  exp3val  10866  binom2sub1  10979  binom3  10982  zesq  10983  sqoddm1div8  11018  nn0opthlem1d  11045  bcm1k  11085  bcp1n  11086  bcp1m1  11090  bcpasc  11091  bcn2m1  11094  omgadd  11128  hashfz  11148  hashfzo  11149  hashfzp1  11151  zfz1isolemsplit  11165  zfz1isolem1  11167  lswccatn0lsw  11254  ccatws1lenp1bg  11278  lswccats1  11286  resqrexlemover  11650  absexpzap  11720  reccn2ap  11953  hashiun  12119  hash2iun1dif1  12121  binomlem  12124  bcxmas  12130  arisum  12139  arisum2  12140  trireciplem  12141  geosergap  12147  pwm1geoserap1  12149  geolim  12152  geolim2  12153  georeclim  12154  geoisum1c  12161  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratnnlemsumlt  12169  cvgratz  12173  mertenslemi1  12176  prodf1f  12184  prodfrecap  12187  ntrivcvgap  12189  prodrbdclem  12212  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  fprodntrivap  12225  prod1dc  12227  fprodmul  12232  prodsnf  12233  fprodsplitdc  12237  fprodm1  12239  fprodp1  12241  fprodcl  12248  fprodfac  12256  fprodrec  12270  fprodclf  12276  ef0lem  12301  efsub  12322  tanaddaplem  12379  tanaddap  12380  cos01bnd  12399  zeo3  12509  oddm1even  12516  oddp1even  12517  oexpneg  12518  ltoddhalfle  12534  halfleoddlt  12535  nn0ob  12549  flodddiv4  12577  bitsp1o  12594  bezoutlema  12650  bezoutlemb  12651  uzwodc  12688  qredeu  12749  prmdiv  12887  prmdiveq  12888  pc2dvds  12983  4sqlem11  13054  4sqlem12  13055  oddennn  13093  ennnfonelemp1  13107  gsumfzconst  14008  gsumsplit0  14013  cncrng  14665  expcn  15380  hoverb  15459  dveflem  15537  dvef  15538  dvply2g  15577  reeff1oleme  15583  sin0pilem1  15592  logdivlti  15692  rpcxpmul2  15724  rplogbval  15756  perfectlem2  15814  lgsvalmod  15838  lgsdir2  15852  lgsdir  15854  gausslemma2dlem1a  15877  gausslemma2dlem5  15885  lgseisenlem4  15892  lgsquadlem1  15896  m1lgs  15904  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgslem3d1  15919  2lgsoddprmlem1  15924  2sqlem8  15942  wlklenvclwlk  16314  clwwlkccatlem  16341  clwwlkext2edg  16363  clwwlknonex2lem1  16378  clwwlknonex2lem2  16379  cvgcmp2nlemabs  16764  iooref1o  16766  trilpolemeq1  16772  trilpolemlt1  16773  apdifflemr  16779  qdiff  16781  iswomni0  16784  nconstwlpolemgt0  16797  gsumgfsumlem  16812  gsumgfsum  16813