Theorem 1cnd 8173

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8008   1c1 8011

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

This theorem is referenced by:  adddirp1d  8184  muladd11r  8313  muls1d  8575  recrecap  8867  rec11ap  8868  rec11rap  8869  rerecclap  8888  subrecap  8997  recp1lt1  9057  nn1m1nn  9139  add1p1  9372  sub1m1  9373  cnm2m1cnm3  9374  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  peano2z  9493  zaddcllempos  9494  peano2zm  9495  zaddcllemneg  9496  nn0n0n1ge2  9528  zneo  9559  peano5uzti  9566  lincmb01cmp  10211  iccf1o  10212  nnsplit  10345  zpnn0elfzo1  10426  ubmelm1fzo  10444  fzoshftral  10456  exbtwnzlemstep  10479  rebtwn2zlemstep  10484  qbtwnrelemcalc  10487  flqaddz  10529  2tnp1ge0ge0  10533  ceiqm1l  10545  qnegmod  10603  addmodlteq  10632  uzsinds  10678  seq3shft2  10715  iseqf1olemab  10736  exp3val  10775  binom2sub1  10888  binom3  10891  zesq  10892  sqoddm1div8  10927  nn0opthlem1d  10954  bcm1k  10994  bcp1n  10995  bcp1m1  10999  bcpasc  11000  bcn2m1  11003  omgadd  11036  hashfz  11056  hashfzo  11057  hashfzp1  11059  zfz1isolemsplit  11073  zfz1isolem1  11075  lswccatn0lsw  11159  ccatws1lenp1bg  11183  lswccats1  11190  resqrexlemover  11537  absexpzap  11607  reccn2ap  11840  hashiun  12005  hash2iun1dif1  12007  binomlem  12010  bcxmas  12016  arisum  12025  arisum2  12026  trireciplem  12027  geosergap  12033  pwm1geoserap1  12035  geolim  12038  geolim2  12039  georeclim  12040  geoisum1c  12047  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratnnlemsumlt  12055  cvgratz  12059  mertenslemi1  12062  prodf1f  12070  prodfrecap  12073  ntrivcvgap  12075  prodrbdclem  12098  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  fprodntrivap  12111  prod1dc  12113  fprodmul  12118  prodsnf  12119  fprodsplitdc  12123  fprodm1  12125  fprodp1  12127  fprodcl  12134  fprodfac  12142  fprodrec  12156  fprodclf  12162  ef0lem  12187  efsub  12208  tanaddaplem  12265  tanaddap  12266  cos01bnd  12285  zeo3  12395  oddm1even  12402  oddp1even  12403  oexpneg  12404  ltoddhalfle  12420  halfleoddlt  12421  nn0ob  12435  flodddiv4  12463  bitsp1o  12480  bezoutlema  12536  bezoutlemb  12537  uzwodc  12574  qredeu  12635  prmdiv  12773  prmdiveq  12774  pc2dvds  12869  4sqlem11  12940  4sqlem12  12941  oddennn  12979  ennnfonelemp1  12993  gsumfzconst  13894  cncrng  14549  expcn  15259  hoverb  15338  dveflem  15416  dvef  15417  dvply2g  15456  reeff1oleme  15462  sin0pilem1  15471  logdivlti  15571  rpcxpmul2  15603  rplogbval  15635  perfectlem2  15690  lgsvalmod  15714  lgsdir2  15728  lgsdir  15730  gausslemma2dlem1a  15753  gausslemma2dlem5  15761  lgseisenlem4  15768  lgsquadlem1  15772  m1lgs  15780  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgslem3d1  15795  2lgsoddprmlem1  15800  2sqlem8  15818  wlklenvclwlk  16119  clwwlkccatlem  16143  clwwlkext2edg  16164  cvgcmp2nlemabs  16488  iooref1o  16490  trilpolemeq1  16496  trilpolemlt1  16497  apdifflemr  16503  iswomni0  16507  nconstwlpolemgt0  16520