Theorem 1cnd 8342

Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 8272	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8177  1c1 8180

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-1cn 8272

This theorem is used by:  adddirp1d  8352  muladd11r  8482  muls1d  8745  recrecap  9039  rec11ap  9040  rec11rap  9041  rerecclap  9060  subrecap  9169  recp1lt1  9229  nn1m1nn  9322  add1p1  9555  sub1m1  9556  cnm2m1cnm3  9557  xp1d2m1eqxm1d2  9558  div4p1lem1div2  9559  peano2z  9680  zaddcllempos  9681  peano2zm  9682  zaddcllemneg  9683  nn0n0n1ge2  9715  zneo  9747  peano5uzti  9754  ltesubnnd  10170  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  fzsplit3  10458  nnsplit  10544  zpnn0elfzo1  10626  ubmelm1fzo  10644  fzosplitpr  10652  fzoshftral  10657  exbtwnzlemstep  10682  rebtwn2zlemstep  10687  qbtwnrelemcalc  10690  flqaddz  10732  2tnp1ge0ge0  10736  ceiqm1l  10748  qnegmod  10806  addmodlteq  10835  uzsinds  10881  seq3shft2  10918  iseqf1olemab  10939  exp3val  10978  binom2sub1  11091  binom3  11094  zesq  11096  sqoddm1div8  11131  nn0opthlem1d  11158  bcm1k  11198  bcp1n  11199  bcp1m1  11203  bcpasc  11204  bcm1n  11207  bcn2m1  11208  omgadd  11242  hashfz  11262  hashfzo  11263  hashfzp1  11265  hashf1lem2  11286  hashf1  11287  zfz1isolemsplit  11290  zfz1isolem1  11292  lswccatn0lsw  11379  ccatws1lenp1bg  11403  lswccats1  11411  sq01  11660  resqrexlemover  11776  absexpzap  11846  reccn2ap  12079  hashiun  12245  hash2iun1dif1  12247  binomlem  12250  bcxmas  12256  arisum  12265  arisum2  12266  trireciplem  12267  geosergap  12273  pwm1geoserap1  12275  geolim  12278  geolim2  12279  georeclim  12280  geoisum1c  12287  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemsumlt  12295  cvgratz  12299  mertenslemi1  12302  prodf1f  12310  prodfrecap  12313  ntrivcvgap  12315  prodrbdclem  12338  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodntrivap  12351  prod1dc  12353  fprodmul  12358  prodsnf  12359  fprodsplitdc  12363  fprodm1  12365  fprodp1  12367  fprodcl  12374  fprodfac  12382  fprodrec  12396  fprodclf  12402  ef0lem  12427  efsub  12448  tanaddaplem  12505  tanaddap  12506  cos01bnd  12525  zeo3  12635  oddm1even  12642  oddp1even  12643  oexpneg  12644  ltoddhalfle  12660  halfleoddlt  12661  nn0ob  12675  flodddiv4  12703  bitsp1o  12720  bezoutlema  12776  bezoutlemb  12777  uzwodc  12814  qredeu  12875  prmdiv  13013  prmdiveq  13014  pc2dvds  13109  4sqlem11  13180  4sqlem12  13181  ballotfilemfp1  13231  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemsgt1  13254  ballotfilemsdom  13255  ballotfilemsel1i  13256  ballotfilemsi  13258  ballotfilemsima  13259  ballotfilem1ri  13278  oddennn  13283  ennnfonelemp1  13297  gzsumconst  14143  gzsumsplit0  14148  gzsumshift  14149  gzsumgsum  14155  cncrng  14906  expcn  15670  hoverb  15749  dveflem  15827  dvef  15828  dvply2g  15867  reeff1oleme  15873  sin0pilem1  15882  logdivlti  15982  rpcxpmul2  16015  rplogbval  16047  birthdaylem2  16088  perfectlem2  16114  lgsvalmod  16138  lgsdir2  16152  lgsdir  16154  gausslemma2dlem1a  16177  gausslemma2dlem5  16185  lgseisenlem4  16192  lgsquadlem1  16196  m1lgs  16204  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3d1  16219  2lgsoddprmlem1  16224  2sqlem8  16242  wlklenvclwlk  16614  clwwlkccatlem  16641  clwwlkext2edg  16663  clwwlknonex2lem1  16678  clwwlknonex2lem2  16679  cvgcmp2nlemabs  17081  iooref1o  17083  trilpolemeq1  17089  trilpolemlt1  17090  apdifflemr  17096  qdiff  17098  iswomni0  17101  nconstwlpolemgt0  17114