Theorem 1cnd 7775

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

Syntax hints:   -> wi 4   e. wcel 1480   CCcc 7611   1c1 7614

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

This theorem is referenced by:  adddirp1d  7785  muladd11r  7911  recrecap  8462  rec11ap  8463  rec11rap  8464  rerecclap  8483  subrecap  8591  recp1lt1  8650  nn1m1nn  8731  add1p1  8962  sub1m1  8963  cnm2m1cnm3  8964  xp1d2m1eqxm1d2  8965  div4p1lem1div2  8966  peano2z  9083  zaddcllempos  9084  peano2zm  9085  zaddcllemneg  9086  nn0n0n1ge2  9114  zneo  9145  peano5uzti  9152  lincmb01cmp  9779  iccf1o  9780  nnsplit  9907  zpnn0elfzo1  9978  ubmelm1fzo  9996  fzoshftral  10008  exbtwnzlemstep  10018  rebtwn2zlemstep  10023  qbtwnrelemcalc  10026  flqaddz  10063  2tnp1ge0ge0  10067  ceiqm1l  10077  qnegmod  10135  addmodlteq  10164  uzsinds  10208  seq3shft2  10239  iseqf1olemab  10255  exp3val  10288  binom2sub1  10399  binom3  10402  zesq  10403  sqoddm1div8  10437  nn0opthlem1d  10459  bcm1k  10499  bcp1n  10500  bcp1m1  10504  bcpasc  10505  bcn2m1  10508  omgadd  10541  hashfz  10560  hashfzo  10561  hashfzp1  10563  zfz1isolemsplit  10574  zfz1isolem1  10576  resqrexlemover  10775  absexpzap  10845  reccn2ap  11075  hashiun  11240  hash2iun1dif1  11242  binomlem  11245  bcxmas  11251  arisum  11260  arisum2  11261  trireciplem  11262  geosergap  11268  pwm1geoserap1  11270  geolim  11273  geolim2  11274  georeclim  11275  geoisum1c  11282  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemsumlt  11290  cvgratz  11294  mertenslemi1  11297  prodf1f  11305  prodfrecap  11308  ntrivcvgap  11310  prodrbdclem  11333  ef0lem  11355  efsub  11376  tanaddaplem  11434  tanaddap  11435  cos01bnd  11454  zeo3  11554  oddm1even  11561  oddp1even  11562  oexpneg  11563  ltoddhalfle  11579  halfleoddlt  11580  nn0ob  11594  flodddiv4  11620  bezoutlema  11676  bezoutlemb  11677  qredeu  11767  oddennn  11894  ennnfonelemp1  11908  dveflem  12844  dvef  12845  sin0pilem1  12851  cvgcmp2nlemabs  13216  trilpolemeq1  13222  trilpolemlt1  13223