Theorem 1cnd 8158

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 8088	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 7993  1c1 7996

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

This theorem is referenced by:  adddirp1d  8169  muladd11r  8298  muls1d  8560  recrecap  8852  rec11ap  8853  rec11rap  8854  rerecclap  8873  subrecap  8982  recp1lt1  9042  nn1m1nn  9124  add1p1  9357  sub1m1  9358  cnm2m1cnm3  9359  xp1d2m1eqxm1d2  9360  div4p1lem1div2  9361  peano2z  9478  zaddcllempos  9479  peano2zm  9480  zaddcllemneg  9481  nn0n0n1ge2  9513  zneo  9544  peano5uzti  9551  lincmb01cmp  10195  iccf1o  10196  nnsplit  10329  zpnn0elfzo1  10409  ubmelm1fzo  10427  fzoshftral  10439  exbtwnzlemstep  10462  rebtwn2zlemstep  10467  qbtwnrelemcalc  10470  flqaddz  10512  2tnp1ge0ge0  10516  ceiqm1l  10528  qnegmod  10586  addmodlteq  10615  uzsinds  10661  seq3shft2  10698  iseqf1olemab  10719  exp3val  10758  binom2sub1  10871  binom3  10874  zesq  10875  sqoddm1div8  10910  nn0opthlem1d  10937  bcm1k  10977  bcp1n  10978  bcp1m1  10982  bcpasc  10983  bcn2m1  10986  omgadd  11019  hashfz  11038  hashfzo  11039  hashfzp1  11041  zfz1isolemsplit  11055  zfz1isolem1  11057  lswccatn0lsw  11141  ccatws1lenp1bg  11163  lswccats1  11169  resqrexlemover  11516  absexpzap  11586  reccn2ap  11819  hashiun  11984  hash2iun1dif1  11986  binomlem  11989  bcxmas  11995  arisum  12004  arisum2  12005  trireciplem  12006  geosergap  12012  pwm1geoserap1  12014  geolim  12017  geolim2  12018  georeclim  12019  geoisum1c  12026  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratnnlemsumlt  12034  cvgratz  12038  mertenslemi1  12041  prodf1f  12049  prodfrecap  12052  ntrivcvgap  12054  prodrbdclem  12077  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodntrivap  12090  prod1dc  12092  fprodmul  12097  prodsnf  12098  fprodsplitdc  12102  fprodm1  12104  fprodp1  12106  fprodcl  12113  fprodfac  12121  fprodrec  12135  fprodclf  12141  ef0lem  12166  efsub  12187  tanaddaplem  12244  tanaddap  12245  cos01bnd  12264  zeo3  12374  oddm1even  12381  oddp1even  12382  oexpneg  12383  ltoddhalfle  12399  halfleoddlt  12400  nn0ob  12414  flodddiv4  12442  bitsp1o  12459  bezoutlema  12515  bezoutlemb  12516  uzwodc  12553  qredeu  12614  prmdiv  12752  prmdiveq  12753  pc2dvds  12848  4sqlem11  12919  4sqlem12  12920  oddennn  12958  ennnfonelemp1  12972  gsumfzconst  13873  cncrng  14527  expcn  15237  hoverb  15316  dveflem  15394  dvef  15395  dvply2g  15434  reeff1oleme  15440  sin0pilem1  15449  logdivlti  15549  rpcxpmul2  15581  rplogbval  15613  perfectlem2  15668  lgsvalmod  15692  lgsdir2  15706  lgsdir  15708  gausslemma2dlem1a  15731  gausslemma2dlem5  15739  lgseisenlem4  15746  lgsquadlem1  15750  m1lgs  15758  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgslem3d1  15773  2lgsoddprmlem1  15778  2sqlem8  15796  cvgcmp2nlemabs  16359  iooref1o  16361  trilpolemeq1  16367  trilpolemlt1  16368  apdifflemr  16374  iswomni0  16378  nconstwlpolemgt0  16391