Theorem 1cnd 11216

Description: One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

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

Proof of Theorem 1cnd

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11114  1c1 11117

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

This theorem is referenced by:  adddirp1d  11247  1p1times  11392  addcom  11407  addcomd  11423  muladd11r  11434  pncan1  11645  npcan1  11646  muls1d  11681  mulsubfacd  11682  recrec  11918  rec11  11919  rec11r  11920  rereccl  11939  subrec  12050  nn1m1nn  12240  add1p1  12470  sub1m1  12471  cnm2m1cnm3  12472  xp1d2m1eqxm1d2  12473  div4p1lem1div2  12474  nn0n0n1ge2  12546  zneo  12652  rpnnen1lem5  12972  lincmb01cmp  13479  iccf1o  13480  xov1plusxeqvd  13482  zpnn0elfzo1  13713  ubmelm1fzo  13735  fzosplitpr  13748  fzosplitprm1  13749  fzoshftral  13756  fladdz  13797  2tnp1ge0ge0  13801  ltdifltdiv  13806  dfceil2  13811  negmod  13888  modnegd  13898  addmodlteq  13918  binom2sub1  14191  binom3  14194  zesq  14196  sqoddm1div8  14213  bcm1k  14282  bcp1n  14283  bcp1m1  14287  bcpasc  14288  bcn2m1  14291  hashfz  14394  hashfzo  14396  hashfzp1  14398  hashf1lem2  14424  hashf1  14425  hashdifsnp1  14464  lswccatn0lsw  14548  ccatws1lenp1b  14578  revccat  14723  repswrevw  14744  cshwidxm1  14764  cshwidxn  14766  cshweqrep  14778  cshimadifsn0  14788  swrds2m  14899  swrd2lsw  14910  relexpaddnn  15005  absexpz  15259  reccn2  15548  rlimno1  15607  isercolllem1  15618  isercoll2  15622  iseraltlem2  15636  iseraltlem3  15637  fsump1  15709  hashiun  15775  hash2iun1dif1  15777  binomlem  15782  bcxmas  15788  incexc  15790  incexc2  15791  climcndslem1  15802  arisum  15813  arisum2  15814  trireciplem  15815  pwdif  15821  pwm1geoser  15822  geolim2  15824  georeclim  15825  mertenslem1  15837  prodfrec  15848  ntrivcvg  15850  ntrivcvgtail  15853  prodrblem  15880  prodmolem2a  15885  fprodntriv  15893  prod1  15895  fprodser  15900  fprodcl  15903  fprodm1  15918  fprodp1  15920  fprodclf  15943  risefacval2  15961  fallfacval2  15962  risefacp1  15980  fallfacp1  15981  risefacfac  15986  fallfacfwd  15987  binomfallfaclem2  15991  fallfacval4  15994  bpolydiflem  16005  ef0lem  16029  tanaddlem  16116  tanadd  16117  cos01bnd  16136  oddm1even  16293  oddp1even  16294  oexpneg  16295  ltoddhalfle  16311  halfleoddlt  16312  nn0ob  16334  pwp1fsum  16341  flodddiv4  16363  bitsp1o  16381  bitsf1  16394  sadcp1  16403  qredeu  16602  prmdiv  16725  prmdiveq  16726  vfermltlALT  16742  pc2dvds  16819  4sqlem11  16895  4sqlem12  16896  vdwapun  16914  vdwlem3  16923  vdwlem6  16926  vdwlem9  16929  ramub1lem2  16967  prmop1  16978  prmdvdsprmo  16982  prmgaplem8  16998  cshwshashnsame  17044  gsumsgrpccat  18763  psgnunilem5  19410  psgnunilem2  19411  sylow1lem1  19514  efgredlemc  19661  odadd2  19765  ablsimpgfindlem1  20025  srgbinomlem3  20129  srgbinomlem4  20130  cncrng  21254  gzrngunit  21299  zringunit  21325  prmirredlem  21331  pzriprnglem12  21351  mhppwdeg  22001  cayhamlem1  22687  expcn  24709  expcnOLD  24711  iirevcn  24770  iihalf2cn  24775  iihalf2cnOLD  24776  icchmeo  24784  icchmeoOLD  24785  icopnfcnv  24786  icopnfhmeo  24787  evth  24804  pcoass  24870  pjthlem1  25284  ovolunlem1a  25344  ovolunlem1  25345  opnmbllem  25449  mbfi1fseqlem6  25569  bddibl  25688  dvnadd  25778  dvmptid  25808  dvmptdiv  25825  dvcnvlem  25827  dveflem  25830  dvef  25831  dvsincos  25832  dvlipcn  25846  dvivthlem1  25860  lhop2  25867  dvcvx  25872  dvfsumle  25873  dvfsumleOLD  25874  dvfsumabs  25876  dvfsumlem1  25879  dvfsumlem2  25880  dvfsumlem2OLD  25881  itgpowd  25904  ply1divex  25991  fta1glem1  26020  dgrcolem1  26125  dgrcolem2  26126  vieta1lem1  26161  aaliou3lem2  26194  aaliou3lem8  26196  dvtaylp  26220  dvntaylp  26221  taylthlem1  26223  taylthlem2  26224  abelthlem1  26282  abelthlem2  26283  abelthlem6  26287  abelthlem7  26289  logdivlti  26467  advlog  26501  advlogexp  26502  logtayl  26507  cxpmul2  26536  dvcxp1  26587  dvcxp2  26588  dvcncxp1  26590  dvcnsqrt  26591  loglesqrt  26606  relogbdiv  26624  ang180lem4  26657  ang180lem5  26658  isosctrlem2  26664  isosctrlem3  26665  affineequiv  26668  affineequiv2  26669  affineequiv3  26670  angpieqvdlem  26673  chordthmlem2  26678  chordthmlem3  26679  chordthmlem5  26681  dcubic2  26689  dcubic  26691  quart1lem  26700  quart1  26701  quart  26706  asinlem  26713  asinlem3  26716  atansopn  26777  dvatan  26780  leibpi  26787  birthdaylem2  26797  efrlim  26814  cxplim  26816  divsqrtsumlem  26824  logdifbnd  26838  emcllem2  26841  emcllem3  26842  emcllem5  26844  zetacvg  26859  lgamgulmlem2  26874  lgamgulmlem3  26875  lgamgulmlem4  26876  lgamgulmlem5  26877  lgamgulmlem6  26878  lgamgulm2  26880  lgamcvg2  26899  gamcvg  26900  gamcvg2lem  26903  lgam1  26908  gamfac  26911  wilthlem2  26913  wilthimp  26916  ftalem5  26921  basellem3  26927  basellem5  26929  basellem8  26932  basellem9  26933  sqff1o  27026  muinv  27037  logfaclbnd  27067  logfacrlim  27069  logexprlim  27070  perfectlem2  27075  dchr1cl  27096  dchrinvcl  27098  dchrfi  27100  dchr1  27102  dchrsum2  27113  bcmono  27122  bcp1ctr  27124  bclbnd  27125  bposlem9  27137  gausslemma2dlem1a  27210  gausslemma2dlem5  27216  lgseisenlem4  27223  lgsquadlem1  27225  m1lgs  27233  2lgslem3a  27241  2lgslem3b  27242  2lgslem3c  27243  2lgslem3d  27244  2lgslem3d1  27248  2lgsoddprmlem1  27253  2sqlem8  27271  2sq2  27278  addsqn2reu  27286  addsqrexnreu  27287  addsqnreup  27288  addsq2nreurex  27289  chtppilim  27320  rpvmasumlem  27332  dchrisumlem1  27334  dchrisum0re  27358  dchrisum0lem2a  27362  mudivsum  27375  mulogsumlem  27376  mulogsum  27377  2vmadivsumlem  27385  selberg4lem1  27405  pntrsumo1  27410  selberg34r  27416  pntrlog2bndlem2  27423  pntrlog2bndlem4  27425  pntrlog2bndlem5  27426  pntrlog2bndlem6  27428  pntibndlem2  27436  pntlemg  27443  pntlemr  27447  pntlemf  27450  pntlemk  27451  pntlemo  27452  pntlem3  27454  ostth2lem2  27479  ttgcontlem1  28574  cusgrsize2inds  29142  wlklenvclwlk  29344  pthdadjvtx  29419  crctcshwlkn0lem1  29496  crctcshwlkn0lem4  29499  crctcshwlkn0lem5  29500  wlklnwwlkln2lem  29568  wlknwwlksnbij  29574  wwlksnred  29578  wwlksnext  29579  wwlksnextbi  29580  wwlksnredwwlkn  29581  wwlksnextwrd  29583  wwlksnextinj  29585  wwlksnextproplem2  29596  wwlksnextproplem3  29597  clwwlkccatlem  29674  clwlkclwwlklem2a1  29677  clwlkclwwlklem2a4  29682  clwlkclwwlklem2a  29683  clwlkclwwlklem2  29685  clwlkclwwlklem3  29686  clwlkclwwlk  29687  clwwisshclwwslemlem  29698  clwwisshclwws  29700  clwwlkel  29731  clwwlkf  29732  clwwlkwwlksb  29739  clwwlkext2edg  29741  wwlksext2clwwlk  29742  clwwlknonex2lem1  29792  clwwlknonex2lem2  29793  eucrct2eupth  29930  numclwwlk1lem2foalem  30036  numclwwlk1lem2fo  30043  numclwlk2lem2f  30062  numclwlk2lem2f1o  30064  numclwwlk6  30075  smcnlem  30382  fzm1ne1  32432  bcm1n  32438  fzom1ne1  32444  ltesubnnd  32460  wrdt2ind  32549  omndmul2  32665  psgnfzto1stlem  32694  cycpmco2lem3  32722  cycpmco2lem4  32723  cycpmco2lem5  32724  cycpmco2lem6  32725  cycpmco2lem7  32726  cycpmco2  32727  archirngz  32770  archiabllem1a  32772  archiabllem2c  32776  freshmansdream  32816  ccfldextdgrr  33200  1smat1  33247  madjusmdetlem2  33271  madjusmdetlem4  33273  dya2icoseg  33739  iwrdsplit  33849  fibp1  33863  ballotlemfp1  33953  ballotlemfc0  33954  ballotlemfcc  33955  ballotlemic  33968  ballotlem1c  33969  ballotlemsgt1  33972  ballotlemsdom  33973  ballotlemsel1i  33974  ballotlemsi  33976  ballotlemsima  33977  ballotlem1ri  33996  sgn0bi  34009  signstfvn  34043  signsvtn0  34044  signstfveq0  34051  signsvfn  34056  signsvtn  34058  signshf  34062  hashreprin  34095  circlemeth  34115  logdivsqrle  34125  revpfxsfxrev  34569  revwlk  34578  swrdwlk  34580  subfacp1lem1  34633  subfacp1lem5  34638  cvxpconn  34696  sinccvglem  35120  divcnvlin  35171  bcm1nt  35176  bcprod  35177  bccolsum  35178  iprodgam  35181  faclimlem1  35182  faclimlem2  35183  faclimlem3  35184  faclim  35185  iprodfac  35186  faclim2  35187  fwddifnp1  35606  gg-cncrng  35646  gg-cnfld1  35647  dnizphlfeqhlf  35815  dnibndlem3  35819  dnibndlem13  35829  unblimceq0  35846  knoppndvlem6  35856  knoppndvlem9  35859  knoppndvlem14  35864  knoppndvlem15  35865  knoppndvlem16  35866  knoppndvlem17  35867  bj-bary1lem1  36655  irrdiff  36670  poimirlem25  36976  poimirlem26  36977  poimirlem32  36983  opnmbllem0  36987  itg2addnclem2  37003  dvasin  37035  dvacos  37036  areacirclem1  37039  areacirclem4  37042  areacirc  37044  bfp  37155  fzsplitnd  41314  lcmfunnnd  41343  lcmineqlem1  41360  lcmineqlem3  41362  lcmineqlem4  41363  lcmineqlem7  41366  lcmineqlem8  41367  lcmineqlem10  41369  lcmineqlem11  41370  lcmineqlem12  41371  lcmineqlem18  41377  lcmineqlem19  41378  lcmineqlem22  41381  lcmineqlem23  41382  dvrelogpow2b  41399  aks4d1p1p4  41402  aks4d1p1p6  41404  aks4d1p1p7  41405  aks4d1p1p5  41406  aks4d1p1  41407  aks4d1p3  41409  aks4d1p7d1  41413  2np3bcnp1  41426  sticksstones10  41437  sticksstones12a  41439  sticksstones12  41440  sticksstones16  41444  sticksstones22  41450  metakunt8  41458  metakunt12  41462  metakunt15  41465  metakunt16  41466  metakunt28  41478  nnadd1com  41643  nnaddcom  41644  nnadddir  41646  nnmul1com  41647  nnmulcom  41648  fz1sump1  41670  oddnumth  41671  nicomachus  41672  sumcubes  41673  reixi  41757  sn-mullid  41770  sn-0tie0  41774  renegmulnnass  41788  fltnltalem  41866  fltnlta  41867  3cubeslem1  41884  3cubeslem2  41885  3cubeslem4  41889  pell1qrge1  42070  rmspecfund  42109  acongeq  42184  jm2.18  42189  jm2.19lem3  42192  jm2.25  42200  jm2.16nn0  42205  jm3.1lem1  42218  jm3.1lem2  42219  areaquad  42427  relexpmulnn  42922  relexpaddss  42931  cvgdvgrat  43534  radcnvrat  43535  hashnzfzclim  43543  ofdivrec  43547  expgrowthi  43554  bccm1k  43563  dvradcnv2  43568  binomcxplemwb  43569  binomcxplemnn0  43570  binomcxplemrat  43571  binomcxplemfrat  43572  binomcxplemdvbinom  43574  binomcxplemnotnn0  43577  refsum2cnlem1  44183  fzisoeu  44468  fperiodmullem  44471  fzdifsuc2  44478  xralrple2  44522  nnsplit  44526  infleinflem2  44539  fmul01lt1lem2  44759  fprodcn  44774  clim1fr1  44775  isumneg  44776  climneg  44784  sumnnodd  44804  reclimc  44827  coseq0  45038  coskpi2  45040  cosknegpi  45043  fprodcncf  45074  fprodsubrecnncnvlem  45081  fprodaddrecnncnvlem  45083  ioodvbdlimc1lem2  45106  ioodvbdlimc2lem  45108  dvnxpaek  45116  dvnmul  45117  dvmptfprod  45119  dvnprodlem3  45122  itgsinexp  45129  itgiccshift  45154  itgperiod  45155  itgsbtaddcnst  45156  stoweidlem1  45175  stoweidlem7  45181  stoweidlem10  45184  stoweidlem11  45185  stoweidlem14  45188  stoweidlem17  45191  stoweidlem34  45208  stoweidlem42  45216  wallispilem3  45241  wallispilem5  45243  wallispi  45244  wallispi2lem1  45245  wallispi2lem2  45246  wallispi2  45247  stirlinglem1  45248  stirlinglem3  45250  stirlinglem4  45251  stirlinglem5  45252  stirlinglem6  45253  stirlinglem7  45254  stirlinglem8  45255  stirlinglem10  45257  stirlinglem11  45258  stirlinglem12  45259  stirlinglem13  45260  stirlinglem15  45262  dirkertrigeqlem2  45273  dirkertrigeqlem3  45274  dirkertrigeq  45275  dirkercncflem1  45277  dirkercncflem2  45278  dirkercncflem4  45280  fourierdlem11  45292  fourierdlem15  45296  fourierdlem26  45307  fourierdlem36  45317  fourierdlem40  45321  fourierdlem41  45322  fourierdlem42  45323  fourierdlem48  45328  fourierdlem49  45329  fourierdlem56  45336  fourierdlem58  45338  fourierdlem59  45339  fourierdlem62  45342  fourierdlem64  45344  fourierdlem65  45345  fourierdlem78  45358  fourierdlem79  45359  sqwvfoura  45402  fourierswlem  45404  fouriersw  45405  etransclem23  45431  etransclem24  45432  etransclem28  45436  etransclem35  45443  etransclem38  45446  nnfoctbdjlem  45629  smfmullem1  45965  sigaradd  46040  deccarry  46477  fargshiftf1  46567  fargshiftfo  46568  fmtnof1  46661  sqrtpwpw2p  46664  fmtnorec2lem  46668  fmtnorec4  46675  fmtnoprmfac1lem  46690  fmtnoprmfac1  46691  fmtnoprmfac2  46693  2pwp1prm  46715  mod42tp1mod8  46728  sfprmdvdsmersenne  46729  lighneallem3  46733  lighneallem4  46736  onego  46772  zofldiv2ALTV  46788  oexpnegALTV  46803  opoeALTV  46809  opeoALTV  46810  epee  46831  perfectALTVlem1  46847  fppr2odd  46857  fpprwppr  46865  0nodd  47006  2nodd  47008  nnsgrpnmnd  47014  1neven  47074  altgsumbc  47190  pw2m1lepw2m1  47362  m1modmmod  47368  zofldiv2  47378  nnpw2pmod  47430  blen1b  47435  blennn0em1  47438  dignn0flhalflem1  47462  dignn0flhalflem2  47463  nn0sumshdiglemB  47467  nn0sumshdiglem1  47468  nn0sumshdiglem2  47469  itcovalpclem2  47518  ackval1  47528  ackval2  47529  ackval3  47530  affineid  47551  1subrec1sub  47552  eenglngeehlnmlem1  47584  eenglngeehlnmlem2  47585  rrx2vlinest  47588