Theorem 1cnd 8195

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   1c1 8033

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

This theorem is referenced by:  adddirp1d  8206  muladd11r  8335  muls1d  8597  recrecap  8889  rec11ap  8890  rec11rap  8891  rerecclap  8910  subrecap  9019  recp1lt1  9079  nn1m1nn  9161  add1p1  9394  sub1m1  9395  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  peano2z  9515  zaddcllempos  9516  peano2zm  9517  zaddcllemneg  9518  nn0n0n1ge2  9550  zneo  9581  peano5uzti  9588  lincmb01cmp  10238  iccf1o  10239  nnsplit  10372  zpnn0elfzo1  10454  ubmelm1fzo  10472  fzosplitpr  10480  fzoshftral  10485  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  qbtwnrelemcalc  10516  flqaddz  10558  2tnp1ge0ge0  10562  ceiqm1l  10574  qnegmod  10632  addmodlteq  10661  uzsinds  10707  seq3shft2  10744  iseqf1olemab  10765  exp3val  10804  binom2sub1  10917  binom3  10920  zesq  10921  sqoddm1div8  10956  nn0opthlem1d  10983  bcm1k  11023  bcp1n  11024  bcp1m1  11028  bcpasc  11029  bcn2m1  11032  omgadd  11066  hashfz  11086  hashfzo  11087  hashfzp1  11089  zfz1isolemsplit  11103  zfz1isolem1  11105  lswccatn0lsw  11189  ccatws1lenp1bg  11213  lswccats1  11221  resqrexlemover  11572  absexpzap  11642  reccn2ap  11875  hashiun  12041  hash2iun1dif1  12043  binomlem  12046  bcxmas  12052  arisum  12061  arisum2  12062  trireciplem  12063  geosergap  12069  pwm1geoserap1  12071  geolim  12074  geolim2  12075  georeclim  12076  geoisum1c  12083  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  cvgratnnlemsumlt  12091  cvgratz  12095  mertenslemi1  12098  prodf1f  12106  prodfrecap  12109  ntrivcvgap  12111  prodrbdclem  12134  prodmodclem3  12138  prodmodclem2a  12139  zproddc  12142  fprodseq  12146  fprodntrivap  12147  prod1dc  12149  fprodmul  12154  prodsnf  12155  fprodsplitdc  12159  fprodm1  12161  fprodp1  12163  fprodcl  12170  fprodfac  12178  fprodrec  12192  fprodclf  12198  ef0lem  12223  efsub  12244  tanaddaplem  12301  tanaddap  12302  cos01bnd  12321  zeo3  12431  oddm1even  12438  oddp1even  12439  oexpneg  12440  ltoddhalfle  12456  halfleoddlt  12457  nn0ob  12471  flodddiv4  12499  bitsp1o  12516  bezoutlema  12572  bezoutlemb  12573  uzwodc  12610  qredeu  12671  prmdiv  12809  prmdiveq  12810  pc2dvds  12905  4sqlem11  12976  4sqlem12  12977  oddennn  13015  ennnfonelemp1  13029  gsumfzconst  13930  gsumsplit0  13935  cncrng  14586  expcn  15296  hoverb  15375  dveflem  15453  dvef  15454  dvply2g  15493  reeff1oleme  15499  sin0pilem1  15508  logdivlti  15608  rpcxpmul2  15640  rplogbval  15672  perfectlem2  15727  lgsvalmod  15751  lgsdir2  15765  lgsdir  15767  gausslemma2dlem1a  15790  gausslemma2dlem5  15798  lgseisenlem4  15805  lgsquadlem1  15809  m1lgs  15817  2lgslem3a  15825  2lgslem3b  15826  2lgslem3c  15827  2lgslem3d  15828  2lgslem3d1  15832  2lgsoddprmlem1  15837  2sqlem8  15855  wlklenvclwlk  16227  clwwlkccatlem  16254  clwwlkext2edg  16276  clwwlknonex2lem1  16291  clwwlknonex2lem2  16292  cvgcmp2nlemabs  16657  iooref1o  16659  trilpolemeq1  16665  trilpolemlt1  16666  apdifflemr  16672  iswomni0  16676  nconstwlpolemgt0  16689  gsumgfsumlem  16704  gsumgfsum  16705