Theorem 1cnd 8090

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7925   1c1 7928

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

This theorem is referenced by:  adddirp1d  8101  muladd11r  8230  muls1d  8492  recrecap  8784  rec11ap  8785  rec11rap  8786  rerecclap  8805  subrecap  8914  recp1lt1  8974  nn1m1nn  9056  add1p1  9289  sub1m1  9290  cnm2m1cnm3  9291  xp1d2m1eqxm1d2  9292  div4p1lem1div2  9293  peano2z  9410  zaddcllempos  9411  peano2zm  9412  zaddcllemneg  9413  nn0n0n1ge2  9445  zneo  9476  peano5uzti  9483  lincmb01cmp  10127  iccf1o  10128  nnsplit  10261  zpnn0elfzo1  10339  ubmelm1fzo  10357  fzoshftral  10369  exbtwnzlemstep  10392  rebtwn2zlemstep  10397  qbtwnrelemcalc  10400  flqaddz  10442  2tnp1ge0ge0  10446  ceiqm1l  10458  qnegmod  10516  addmodlteq  10545  uzsinds  10591  seq3shft2  10628  iseqf1olemab  10649  exp3val  10688  binom2sub1  10801  binom3  10804  zesq  10805  sqoddm1div8  10840  nn0opthlem1d  10867  bcm1k  10907  bcp1n  10908  bcp1m1  10912  bcpasc  10913  bcn2m1  10916  omgadd  10949  hashfz  10968  hashfzo  10969  hashfzp1  10971  zfz1isolemsplit  10985  zfz1isolem1  10987  lswccatn0lsw  11070  ccatws1lenp1bg  11092  lswccats1  11098  resqrexlemover  11354  absexpzap  11424  reccn2ap  11657  hashiun  11822  hash2iun1dif1  11824  binomlem  11827  bcxmas  11833  arisum  11842  arisum2  11843  trireciplem  11844  geosergap  11850  pwm1geoserap1  11852  geolim  11855  geolim2  11856  georeclim  11857  geoisum1c  11864  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratnnlemsumlt  11872  cvgratz  11876  mertenslemi1  11879  prodf1f  11887  prodfrecap  11890  ntrivcvgap  11892  prodrbdclem  11915  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodntrivap  11928  prod1dc  11930  fprodmul  11935  prodsnf  11936  fprodsplitdc  11940  fprodm1  11942  fprodp1  11944  fprodcl  11951  fprodfac  11959  fprodrec  11973  fprodclf  11979  ef0lem  12004  efsub  12025  tanaddaplem  12082  tanaddap  12083  cos01bnd  12102  zeo3  12212  oddm1even  12219  oddp1even  12220  oexpneg  12221  ltoddhalfle  12237  halfleoddlt  12238  nn0ob  12252  flodddiv4  12280  bitsp1o  12297  bezoutlema  12353  bezoutlemb  12354  uzwodc  12391  qredeu  12452  prmdiv  12590  prmdiveq  12591  pc2dvds  12686  4sqlem11  12757  4sqlem12  12758  oddennn  12796  ennnfonelemp1  12810  gsumfzconst  13710  cncrng  14364  expcn  15074  hoverb  15153  dveflem  15231  dvef  15232  dvply2g  15271  reeff1oleme  15277  sin0pilem1  15286  logdivlti  15386  rpcxpmul2  15418  rplogbval  15450  perfectlem2  15505  lgsvalmod  15529  lgsdir2  15543  lgsdir  15545  gausslemma2dlem1a  15568  gausslemma2dlem5  15576  lgseisenlem4  15583  lgsquadlem1  15587  m1lgs  15595  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgslem3d1  15610  2lgsoddprmlem1  15615  2sqlem8  15633  cvgcmp2nlemabs  16008  iooref1o  16010  trilpolemeq1  16016  trilpolemlt1  16017  apdifflemr  16023  iswomni0  16027  nconstwlpolemgt0  16040