Theorem 1cnd 8332

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

Syntax hints:   -> wi 4   e. wcel 2209   CCcc 8167   1c1 8170

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

This theorem is referenced by:  adddirp1d  8342  muladd11r  8472  muls1d  8735  recrecap  9029  rec11ap  9030  rec11rap  9031  rerecclap  9050  subrecap  9159  recp1lt1  9219  nn1m1nn  9301  add1p1  9534  sub1m1  9535  cnm2m1cnm3  9536  xp1d2m1eqxm1d2  9537  div4p1lem1div2  9538  peano2z  9659  zaddcllempos  9660  peano2zm  9661  zaddcllemneg  9662  nn0n0n1ge2  9694  zneo  9726  peano5uzti  9733  ltesubnnd  10149  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  fzsplit3  10436  nnsplit  10522  zpnn0elfzo1  10604  ubmelm1fzo  10622  fzosplitpr  10630  fzoshftral  10635  exbtwnzlemstep  10660  rebtwn2zlemstep  10665  qbtwnrelemcalc  10668  flqaddz  10710  2tnp1ge0ge0  10714  ceiqm1l  10726  qnegmod  10784  addmodlteq  10813  uzsinds  10859  seq3shft2  10896  iseqf1olemab  10917  exp3val  10956  binom2sub1  11069  binom3  11072  zesq  11074  sqoddm1div8  11109  nn0opthlem1d  11136  bcm1k  11176  bcp1n  11177  bcp1m1  11181  bcpasc  11182  bcm1n  11185  bcn2m1  11186  omgadd  11220  hashfz  11240  hashfzo  11241  hashfzp1  11243  hashf1lem2  11264  hashf1  11265  zfz1isolemsplit  11268  zfz1isolem1  11270  lswccatn0lsw  11357  ccatws1lenp1bg  11381  lswccats1  11389  sq01  11638  resqrexlemover  11754  absexpzap  11824  reccn2ap  12057  hashiun  12223  hash2iun1dif1  12225  binomlem  12228  bcxmas  12234  arisum  12243  arisum2  12244  trireciplem  12245  geosergap  12251  pwm1geoserap1  12253  geolim  12256  geolim2  12257  georeclim  12258  geoisum1c  12265  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemsumlt  12273  cvgratz  12277  mertenslemi1  12280  prodf1f  12288  prodfrecap  12291  ntrivcvgap  12293  prodrbdclem  12316  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodntrivap  12329  prod1dc  12331  fprodmul  12336  prodsnf  12337  fprodsplitdc  12341  fprodm1  12343  fprodp1  12345  fprodcl  12352  fprodfac  12360  fprodrec  12374  fprodclf  12380  ef0lem  12405  efsub  12426  tanaddaplem  12483  tanaddap  12484  cos01bnd  12503  zeo3  12613  oddm1even  12620  oddp1even  12621  oexpneg  12622  ltoddhalfle  12638  halfleoddlt  12639  nn0ob  12653  flodddiv4  12681  bitsp1o  12698  bezoutlema  12754  bezoutlemb  12755  uzwodc  12792  qredeu  12853  prmdiv  12991  prmdiveq  12992  pc2dvds  13087  4sqlem11  13158  4sqlem12  13159  ballotfilemfp1  13209  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemsgt1  13232  ballotfilemsdom  13233  ballotfilemsel1i  13234  ballotfilemsi  13236  ballotfilemsima  13237  ballotfilem1ri  13256  oddennn  13261  ennnfonelemp1  13275  gzsumconst  14120  gzsumsplit0  14125  gzsumshift  14126  gzsumgsum  14132  cncrng  14878  expcn  15593  hoverb  15672  dveflem  15750  dvef  15751  dvply2g  15790  reeff1oleme  15796  sin0pilem1  15805  logdivlti  15905  rpcxpmul2  15938  rplogbval  15970  perfectlem2  16028  lgsvalmod  16052  lgsdir2  16066  lgsdir  16068  gausslemma2dlem1a  16091  gausslemma2dlem5  16099  lgseisenlem4  16106  lgsquadlem1  16110  m1lgs  16118  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgslem3d1  16133  2lgsoddprmlem1  16138  2sqlem8  16156  wlklenvclwlk  16528  clwwlkccatlem  16555  clwwlkext2edg  16577  clwwlknonex2lem1  16592  clwwlknonex2lem2  16593  cvgcmp2nlemabs  16986  iooref1o  16988  trilpolemeq1  16994  trilpolemlt1  16995  apdifflemr  17001  qdiff  17003  iswomni0  17006  nconstwlpolemgt0  17019