Theorem 1cnd 8185

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8020  1c1 8023

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

This theorem is referenced by:  adddirp1d  8196  muladd11r  8325  muls1d  8587  recrecap  8879  rec11ap  8880  rec11rap  8881  rerecclap  8900  subrecap  9009  recp1lt1  9069  nn1m1nn  9151  add1p1  9384  sub1m1  9385  cnm2m1cnm3  9386  xp1d2m1eqxm1d2  9387  div4p1lem1div2  9388  peano2z  9505  zaddcllempos  9506  peano2zm  9507  zaddcllemneg  9508  nn0n0n1ge2  9540  zneo  9571  peano5uzti  9578  lincmb01cmp  10228  iccf1o  10229  nnsplit  10362  zpnn0elfzo1  10443  ubmelm1fzo  10461  fzosplitpr  10469  fzoshftral  10474  exbtwnzlemstep  10497  rebtwn2zlemstep  10502  qbtwnrelemcalc  10505  flqaddz  10547  2tnp1ge0ge0  10551  ceiqm1l  10563  qnegmod  10621  addmodlteq  10650  uzsinds  10696  seq3shft2  10733  iseqf1olemab  10754  exp3val  10793  binom2sub1  10906  binom3  10909  zesq  10910  sqoddm1div8  10945  nn0opthlem1d  10972  bcm1k  11012  bcp1n  11013  bcp1m1  11017  bcpasc  11018  bcn2m1  11021  omgadd  11055  hashfz  11075  hashfzo  11076  hashfzp1  11078  zfz1isolemsplit  11092  zfz1isolem1  11094  lswccatn0lsw  11178  ccatws1lenp1bg  11202  lswccats1  11210  resqrexlemover  11561  absexpzap  11631  reccn2ap  11864  hashiun  12029  hash2iun1dif1  12031  binomlem  12034  bcxmas  12040  arisum  12049  arisum2  12050  trireciplem  12051  geosergap  12057  pwm1geoserap1  12059  geolim  12062  geolim2  12063  georeclim  12064  geoisum1c  12071  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemsumlt  12079  cvgratz  12083  mertenslemi1  12086  prodf1f  12094  prodfrecap  12097  ntrivcvgap  12099  prodrbdclem  12122  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodntrivap  12135  prod1dc  12137  fprodmul  12142  prodsnf  12143  fprodsplitdc  12147  fprodm1  12149  fprodp1  12151  fprodcl  12158  fprodfac  12166  fprodrec  12180  fprodclf  12186  ef0lem  12211  efsub  12232  tanaddaplem  12289  tanaddap  12290  cos01bnd  12309  zeo3  12419  oddm1even  12426  oddp1even  12427  oexpneg  12428  ltoddhalfle  12444  halfleoddlt  12445  nn0ob  12459  flodddiv4  12487  bitsp1o  12504  bezoutlema  12560  bezoutlemb  12561  uzwodc  12598  qredeu  12659  prmdiv  12797  prmdiveq  12798  pc2dvds  12893  4sqlem11  12964  4sqlem12  12965  oddennn  13003  ennnfonelemp1  13017  gsumfzconst  13918  cncrng  14573  expcn  15283  hoverb  15362  dveflem  15440  dvef  15441  dvply2g  15480  reeff1oleme  15486  sin0pilem1  15495  logdivlti  15595  rpcxpmul2  15627  rplogbval  15659  perfectlem2  15714  lgsvalmod  15738  lgsdir2  15752  lgsdir  15754  gausslemma2dlem1a  15777  gausslemma2dlem5  15785  lgseisenlem4  15792  lgsquadlem1  15796  m1lgs  15804  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgslem3d1  15819  2lgsoddprmlem1  15824  2sqlem8  15842  wlklenvclwlk  16170  clwwlkccatlem  16195  clwwlkext2edg  16217  clwwlknonex2lem1  16232  clwwlknonex2lem2  16233  cvgcmp2nlemabs  16572  iooref1o  16574  trilpolemeq1  16580  trilpolemlt1  16581  apdifflemr  16587  iswomni0  16591  nconstwlpolemgt0  16604