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  11192  ccatws1lenp1bg  11216  lswccats1  11224  resqrexlemover  11588  absexpzap  11658  reccn2ap  11891  hashiun  12057  hash2iun1dif1  12059  binomlem  12062  bcxmas  12068  arisum  12077  arisum2  12078  trireciplem  12079  geosergap  12085  pwm1geoserap1  12087  geolim  12090  geolim2  12091  georeclim  12092  geoisum1c  12099  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemsumlt  12107  cvgratz  12111  mertenslemi1  12114  prodf1f  12122  prodfrecap  12125  ntrivcvgap  12127  prodrbdclem  12150  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodntrivap  12163  prod1dc  12165  fprodmul  12170  prodsnf  12171  fprodsplitdc  12175  fprodm1  12177  fprodp1  12179  fprodcl  12186  fprodfac  12194  fprodrec  12208  fprodclf  12214  ef0lem  12239  efsub  12260  tanaddaplem  12317  tanaddap  12318  cos01bnd  12337  zeo3  12447  oddm1even  12454  oddp1even  12455  oexpneg  12456  ltoddhalfle  12472  halfleoddlt  12473  nn0ob  12487  flodddiv4  12515  bitsp1o  12532  bezoutlema  12588  bezoutlemb  12589  uzwodc  12626  qredeu  12687  prmdiv  12825  prmdiveq  12826  pc2dvds  12921  4sqlem11  12992  4sqlem12  12993  oddennn  13031  ennnfonelemp1  13045  gsumfzconst  13946  gsumsplit0  13951  cncrng  14602  expcn  15312  hoverb  15391  dveflem  15469  dvef  15470  dvply2g  15509  reeff1oleme  15515  sin0pilem1  15524  logdivlti  15624  rpcxpmul2  15656  rplogbval  15688  perfectlem2  15743  lgsvalmod  15767  lgsdir2  15781  lgsdir  15783  gausslemma2dlem1a  15806  gausslemma2dlem5  15814  lgseisenlem4  15821  lgsquadlem1  15825  m1lgs  15833  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgslem3d1  15848  2lgsoddprmlem1  15853  2sqlem8  15871  wlklenvclwlk  16243  clwwlkccatlem  16270  clwwlkext2edg  16292  clwwlknonex2lem1  16307  clwwlknonex2lem2  16308  cvgcmp2nlemabs  16687  iooref1o  16689  trilpolemeq1  16695  trilpolemlt1  16696  apdifflemr  16702  qdiff  16704  iswomni0  16707  nconstwlpolemgt0  16720  gsumgfsumlem  16735  gsumgfsum  16736