Theorem 1cnd 8059

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7894   1c1 7897

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

This theorem is referenced by:  adddirp1d  8070  muladd11r  8199  muls1d  8461  recrecap  8753  rec11ap  8754  rec11rap  8755  rerecclap  8774  subrecap  8883  recp1lt1  8943  nn1m1nn  9025  add1p1  9258  sub1m1  9259  cnm2m1cnm3  9260  xp1d2m1eqxm1d2  9261  div4p1lem1div2  9262  peano2z  9379  zaddcllempos  9380  peano2zm  9381  zaddcllemneg  9382  nn0n0n1ge2  9413  zneo  9444  peano5uzti  9451  lincmb01cmp  10095  iccf1o  10096  nnsplit  10229  zpnn0elfzo1  10301  ubmelm1fzo  10319  fzoshftral  10331  exbtwnzlemstep  10354  rebtwn2zlemstep  10359  qbtwnrelemcalc  10362  flqaddz  10404  2tnp1ge0ge0  10408  ceiqm1l  10420  qnegmod  10478  addmodlteq  10507  uzsinds  10553  seq3shft2  10590  iseqf1olemab  10611  exp3val  10650  binom2sub1  10763  binom3  10766  zesq  10767  sqoddm1div8  10802  nn0opthlem1d  10829  bcm1k  10869  bcp1n  10870  bcp1m1  10874  bcpasc  10875  bcn2m1  10878  omgadd  10911  hashfz  10930  hashfzo  10931  hashfzp1  10933  zfz1isolemsplit  10947  zfz1isolem1  10949  resqrexlemover  11192  absexpzap  11262  reccn2ap  11495  hashiun  11660  hash2iun1dif1  11662  binomlem  11665  bcxmas  11671  arisum  11680  arisum2  11681  trireciplem  11682  geosergap  11688  pwm1geoserap1  11690  geolim  11693  geolim2  11694  georeclim  11695  geoisum1c  11702  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemsumlt  11710  cvgratz  11714  mertenslemi1  11717  prodf1f  11725  prodfrecap  11728  ntrivcvgap  11730  prodrbdclem  11753  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodntrivap  11766  prod1dc  11768  fprodmul  11773  prodsnf  11774  fprodsplitdc  11778  fprodm1  11780  fprodp1  11782  fprodcl  11789  fprodfac  11797  fprodrec  11811  fprodclf  11817  ef0lem  11842  efsub  11863  tanaddaplem  11920  tanaddap  11921  cos01bnd  11940  zeo3  12050  oddm1even  12057  oddp1even  12058  oexpneg  12059  ltoddhalfle  12075  halfleoddlt  12076  nn0ob  12090  flodddiv4  12118  bitsp1o  12135  bezoutlema  12191  bezoutlemb  12192  uzwodc  12229  qredeu  12290  prmdiv  12428  prmdiveq  12429  pc2dvds  12524  4sqlem11  12595  4sqlem12  12596  oddennn  12634  ennnfonelemp1  12648  gsumfzconst  13547  cncrng  14201  expcn  14889  hoverb  14968  dveflem  15046  dvef  15047  dvply2g  15086  reeff1oleme  15092  sin0pilem1  15101  logdivlti  15201  rpcxpmul2  15233  rplogbval  15265  perfectlem2  15320  lgsvalmod  15344  lgsdir2  15358  lgsdir  15360  gausslemma2dlem1a  15383  gausslemma2dlem5  15391  lgseisenlem4  15398  lgsquadlem1  15402  m1lgs  15410  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3d1  15425  2lgsoddprmlem1  15430  2sqlem8  15448  cvgcmp2nlemabs  15763  iooref1o  15765  trilpolemeq1  15771  trilpolemlt1  15772  apdifflemr  15778  iswomni0  15782  nconstwlpolemgt0  15795