Theorem 1cnd 8292

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8127   1c1 8130

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

This theorem is referenced by:  adddirp1d  8302  muladd11r  8431  muls1d  8693  recrecap  8985  rec11ap  8986  rec11rap  8987  rerecclap  9006  subrecap  9115  recp1lt1  9175  nn1m1nn  9257  add1p1  9490  sub1m1  9491  cnm2m1cnm3  9492  xp1d2m1eqxm1d2  9493  div4p1lem1div2  9494  peano2z  9615  zaddcllempos  9616  peano2zm  9617  zaddcllemneg  9618  nn0n0n1ge2  9650  zneo  9682  peano5uzti  9689  lincmb01cmp  10339  lincmble  10340  iccf1o  10341  nnsplit  10475  zpnn0elfzo1  10557  ubmelm1fzo  10575  fzosplitpr  10583  fzoshftral  10588  exbtwnzlemstep  10611  rebtwn2zlemstep  10616  qbtwnrelemcalc  10619  flqaddz  10661  2tnp1ge0ge0  10665  ceiqm1l  10677  qnegmod  10735  addmodlteq  10764  uzsinds  10810  seq3shft2  10847  iseqf1olemab  10868  exp3val  10907  binom2sub1  11020  binom3  11023  zesq  11024  sqoddm1div8  11059  nn0opthlem1d  11086  bcm1k  11126  bcp1n  11127  bcp1m1  11131  bcpasc  11132  bcm1n  11135  bcn2m1  11136  omgadd  11170  hashfz  11190  hashfzo  11191  hashfzp1  11193  zfz1isolemsplit  11214  zfz1isolem1  11216  lswccatn0lsw  11303  ccatws1lenp1bg  11327  lswccats1  11335  resqrexlemover  11699  absexpzap  11769  reccn2ap  12002  hashiun  12168  hash2iun1dif1  12170  binomlem  12173  bcxmas  12179  arisum  12188  arisum2  12189  trireciplem  12190  geosergap  12196  pwm1geoserap1  12198  geolim  12201  geolim2  12202  georeclim  12203  geoisum1c  12210  cvgratnnlemnexp  12214  cvgratnnlemmn  12215  cvgratnnlemsumlt  12218  cvgratz  12222  mertenslemi1  12225  prodf1f  12233  prodfrecap  12236  ntrivcvgap  12238  prodrbdclem  12261  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  fprodntrivap  12274  prod1dc  12276  fprodmul  12281  prodsnf  12282  fprodsplitdc  12286  fprodm1  12288  fprodp1  12290  fprodcl  12297  fprodfac  12305  fprodrec  12319  fprodclf  12325  ef0lem  12350  efsub  12371  tanaddaplem  12428  tanaddap  12429  cos01bnd  12448  zeo3  12558  oddm1even  12565  oddp1even  12566  oexpneg  12567  ltoddhalfle  12583  halfleoddlt  12584  nn0ob  12598  flodddiv4  12626  bitsp1o  12643  bezoutlema  12699  bezoutlemb  12700  uzwodc  12737  qredeu  12798  prmdiv  12936  prmdiveq  12937  pc2dvds  13032  4sqlem11  13103  4sqlem12  13104  ballotfilemfp1  13152  ballotfilemfc0  13153  ballotfilemfcc  13154  oddennn  13160  ennnfonelemp1  13174  gsumfzconst  14075  gsumsplit0  14080  cncrng  14734  expcn  15451  hoverb  15530  dveflem  15608  dvef  15609  dvply2g  15648  reeff1oleme  15654  sin0pilem1  15663  logdivlti  15763  rpcxpmul2  15795  rplogbval  15827  perfectlem2  15885  lgsvalmod  15909  lgsdir2  15923  lgsdir  15925  gausslemma2dlem1a  15948  gausslemma2dlem5  15956  lgseisenlem4  15963  lgsquadlem1  15967  m1lgs  15975  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986  2lgslem3d1  15990  2lgsoddprmlem1  15995  2sqlem8  16013  wlklenvclwlk  16385  clwwlkccatlem  16412  clwwlkext2edg  16434  clwwlknonex2lem1  16449  clwwlknonex2lem2  16450  cvgcmp2nlemabs  16833  iooref1o  16835  trilpolemeq1  16841  trilpolemlt1  16842  apdifflemr  16848  qdiff  16850  iswomni0  16853  nconstwlpolemgt0  16867  gsumgfsumlem  16882  gsumgfsum  16883