Theorem 1cnd 7782

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

Syntax hints:   -> wi 4   e. wcel 1480   CCcc 7618   1c1 7621

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

This theorem is referenced by:  adddirp1d  7792  muladd11r  7918  recrecap  8469  rec11ap  8470  rec11rap  8471  rerecclap  8490  subrecap  8598  recp1lt1  8657  nn1m1nn  8738  add1p1  8969  sub1m1  8970  cnm2m1cnm3  8971  xp1d2m1eqxm1d2  8972  div4p1lem1div2  8973  peano2z  9090  zaddcllempos  9091  peano2zm  9092  zaddcllemneg  9093  nn0n0n1ge2  9121  zneo  9152  peano5uzti  9159  lincmb01cmp  9786  iccf1o  9787  nnsplit  9914  zpnn0elfzo1  9985  ubmelm1fzo  10003  fzoshftral  10015  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  qbtwnrelemcalc  10033  flqaddz  10070  2tnp1ge0ge0  10074  ceiqm1l  10084  qnegmod  10142  addmodlteq  10171  uzsinds  10215  seq3shft2  10246  iseqf1olemab  10262  exp3val  10295  binom2sub1  10406  binom3  10409  zesq  10410  sqoddm1div8  10444  nn0opthlem1d  10466  bcm1k  10506  bcp1n  10507  bcp1m1  10511  bcpasc  10512  bcn2m1  10515  omgadd  10548  hashfz  10567  hashfzo  10568  hashfzp1  10570  zfz1isolemsplit  10581  zfz1isolem1  10583  resqrexlemover  10782  absexpzap  10852  reccn2ap  11082  hashiun  11247  hash2iun1dif1  11249  binomlem  11252  bcxmas  11258  arisum  11267  arisum2  11268  trireciplem  11269  geosergap  11275  pwm1geoserap1  11277  geolim  11280  geolim2  11281  georeclim  11282  geoisum1c  11289  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemsumlt  11297  cvgratz  11301  mertenslemi1  11304  prodf1f  11312  prodfrecap  11315  ntrivcvgap  11317  prodrbdclem  11340  prodmodclem3  11344  prodmodclem2a  11345  ef0lem  11366  efsub  11387  tanaddaplem  11445  tanaddap  11446  cos01bnd  11465  zeo3  11565  oddm1even  11572  oddp1even  11573  oexpneg  11574  ltoddhalfle  11590  halfleoddlt  11591  nn0ob  11605  flodddiv4  11631  bezoutlema  11687  bezoutlemb  11688  qredeu  11778  oddennn  11905  ennnfonelemp1  11919  dveflem  12855  dvef  12856  sin0pilem1  12862  cvgcmp2nlemabs  13227  trilpolemeq1  13233  trilpolemlt1  13234