Theorem 1cnd 11285

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  1c1 11185

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

This theorem is referenced by:  adddirp1d  11316  1p1times  11461  addcom  11476  addcomd  11492  muladd11r  11503  pncan1  11714  npcan1  11715  muls1d  11750  mulsubfacd  11751  recrec  11991  rec11  11992  rec11r  11993  rereccl  12012  subrec  12123  nn1m1nn  12314  add1p1  12544  sub1m1  12545  cnm2m1cnm3  12546  xp1d2m1eqxm1d2  12547  div4p1lem1div2  12548  nn0n0n1ge2  12620  zneo  12726  rpnnen1lem5  13046  lincmb01cmp  13555  iccf1o  13556  xov1plusxeqvd  13558  zpnn0elfzo1  13790  ubmelm1fzo  13813  fzosplitpr  13826  fzosplitprm1  13827  fzoshftral  13834  fladdz  13876  2tnp1ge0ge0  13880  ltdifltdiv  13885  dfceil2  13890  negmod  13967  modnegd  13977  addmodlteq  13997  binom2sub1  14270  binom3  14273  zesq  14275  sqoddm1div8  14292  bcm1k  14364  bcp1n  14365  bcp1m1  14369  bcpasc  14370  bcn2m1  14373  hashfz  14476  hashfzo  14478  hashfzp1  14480  hashf1lem2  14505  hashf1  14506  hashdifsnp1  14555  lswccatn0lsw  14639  ccatws1lenp1b  14669  revccat  14814  repswrevw  14835  cshwidxm1  14855  cshwidxn  14857  cshweqrep  14869  cshimadifsn0  14879  swrds2m  14990  swrd2lsw  15001  relexpaddnn  15100  absexpz  15354  reccn2  15643  rlimno1  15702  isercolllem1  15713  isercoll2  15717  iseraltlem2  15731  iseraltlem3  15732  fsump1  15804  hashiun  15870  hash2iun1dif1  15872  binomlem  15877  bcxmas  15883  incexc  15885  incexc2  15886  climcndslem1  15897  arisum  15908  arisum2  15909  trireciplem  15910  pwdif  15916  pwm1geoser  15917  geolim2  15919  georeclim  15920  mertenslem1  15932  prodfrec  15943  ntrivcvg  15945  ntrivcvgtail  15948  prodrblem  15977  prodmolem2a  15982  fprodntriv  15990  prod1  15992  fprodser  15997  fprodcl  16000  fprodm1  16015  fprodp1  16017  fprodclf  16040  risefacval2  16058  fallfacval2  16059  risefacp1  16077  fallfacp1  16078  risefacfac  16083  fallfacfwd  16084  binomfallfaclem2  16088  fallfacval4  16091  bpolydiflem  16102  ef0lem  16126  tanaddlem  16214  tanadd  16215  cos01bnd  16234  oddm1even  16391  oddp1even  16392  oexpneg  16393  ltoddhalfle  16409  halfleoddlt  16410  nn0ob  16432  pwp1fsum  16439  flodddiv4  16461  bitsp1o  16479  bitsf1  16492  sadcp1  16501  qredeu  16705  prmdiv  16832  prmdiveq  16833  vfermltlALT  16849  pc2dvds  16926  4sqlem11  17002  4sqlem12  17003  vdwapun  17021  vdwlem3  17030  vdwlem6  17033  vdwlem9  17036  ramub1lem2  17074  prmop1  17085  prmdvdsprmo  17089  prmgaplem8  17105  cshwshashnsame  17151  gsumsgrpccat  18875  psgnunilem5  19536  psgnunilem2  19537  sylow1lem1  19640  efgredlemc  19787  odadd2  19891  ablsimpgfindlem1  20151  srgbinomlem3  20255  srgbinomlem4  20256  cncrng  21424  cncrngOLD  21425  gzrngunit  21474  zringunit  21500  prmirredlem  21506  pzriprnglem12  21526  freshmansdream  21616  mhppwdeg  22177  psdmul  22193  cayhamlem1  22893  expcn  24915  expcnOLD  24917  iirevcn  24976  iihalf2cn  24981  iihalf2cnOLD  24982  icchmeo  24990  icchmeoOLD  24991  icopnfcnv  24992  icopnfhmeo  24993  evth  25010  pcoass  25076  pjthlem1  25490  ovolunlem1a  25550  ovolunlem1  25551  opnmbllem  25655  mbfi1fseqlem6  25775  bddibl  25895  dvnadd  25985  dvmptid  26015  dvmptdiv  26032  dvcnvlem  26034  dveflem  26037  dvef  26038  dvsincos  26039  dvlipcn  26053  dvivthlem1  26067  lhop2  26074  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgpowd  26111  ply1divex  26196  fta1glem1  26227  dgrcolem1  26333  dgrcolem2  26334  vieta1lem1  26370  aaliou3lem2  26403  aaliou3lem8  26405  dvtaylp  26430  dvntaylp  26431  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  abelthlem1  26493  abelthlem2  26494  abelthlem6  26498  abelthlem7  26500  logdivlti  26680  advlog  26714  advlogexp  26715  logtayl  26720  cxpmul2  26749  dvcxp1  26800  dvcxp2  26801  dvcncxp1  26803  dvcnsqrt  26804  loglesqrt  26822  relogbdiv  26840  ang180lem4  26873  ang180lem5  26874  isosctrlem2  26880  isosctrlem3  26881  affineequiv  26884  affineequiv2  26885  affineequiv3  26886  angpieqvdlem  26889  chordthmlem2  26894  chordthmlem3  26895  chordthmlem5  26897  dcubic2  26905  dcubic  26907  quart1lem  26916  quart1  26917  quart  26922  asinlem  26929  asinlem3  26932  atansopn  26993  dvatan  26996  leibpi  27003  birthdaylem2  27013  efrlim  27030  efrlimOLD  27031  cxplim  27033  divsqrtsumlem  27041  logdifbnd  27055  emcllem2  27058  emcllem3  27059  emcllem5  27061  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgamcvg2  27116  gamcvg  27117  gamcvg2lem  27120  lgam1  27125  gamfac  27128  wilthlem2  27130  wilthimp  27133  ftalem5  27138  basellem3  27144  basellem5  27146  basellem8  27149  basellem9  27150  sqff1o  27243  muinv  27254  logfaclbnd  27284  logfacrlim  27286  logexprlim  27287  perfectlem2  27292  dchr1cl  27313  dchrinvcl  27315  dchrfi  27317  dchr1  27319  dchrsum2  27330  bcmono  27339  bcp1ctr  27341  bclbnd  27342  bposlem9  27354  gausslemma2dlem1a  27427  gausslemma2dlem5  27433  lgseisenlem4  27440  lgsquadlem1  27442  m1lgs  27450  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgslem3d1  27465  2lgsoddprmlem1  27470  2sqlem8  27488  2sq2  27495  addsqn2reu  27503  addsqrexnreu  27504  addsqnreup  27505  addsq2nreurex  27506  chtppilim  27537  rpvmasumlem  27549  dchrisumlem1  27551  dchrisum0re  27575  dchrisum0lem2a  27579  mudivsum  27592  mulogsumlem  27593  mulogsum  27594  2vmadivsumlem  27602  selberg4lem1  27622  pntrsumo1  27627  selberg34r  27633  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntibndlem2  27653  pntlemg  27660  pntlemr  27664  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntlem3  27671  ostth2lem2  27696  ttgcontlem1  28917  cusgrsize2inds  29489  wlklenvclwlk  29691  pthdadjvtx  29766  crctcshwlkn0lem1  29843  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  wlklnwwlkln2lem  29915  wlknwwlksnbij  29921  wwlksnred  29925  wwlksnext  29926  wwlksnextbi  29927  wwlksnredwwlkn  29928  wwlksnextwrd  29930  wwlksnextinj  29932  wwlksnextproplem2  29943  wwlksnextproplem3  29944  clwwlkccatlem  30021  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlklem3  30033  clwlkclwwlk  30034  clwwisshclwwslemlem  30045  clwwisshclwws  30047  clwwlkel  30078  clwwlkf  30079  clwwlkwwlksb  30086  clwwlkext2edg  30088  wwlksext2clwwlk  30089  clwwlknonex2lem1  30139  clwwlknonex2lem2  30140  eucrct2eupth  30277  numclwwlk1lem2foalem  30383  numclwwlk1lem2fo  30390  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  numclwwlk6  30422  smcnlem  30729  fzm1ne1  32794  bcm1n  32800  fzom1ne1  32806  ltesubnnd  32826  wrdt2ind  32920  chnub  32984  chnlt  32985  omndmul2  33062  psgnfzto1stlem  33093  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  archirngz  33169  archiabllem1a  33171  archiabllem2c  33175  ccfldextdgrr  33682  constrfin  33736  2sqr3minply  33738  1smat1  33750  madjusmdetlem2  33774  madjusmdetlem4  33776  dya2icoseg  34242  iwrdsplit  34352  fibp1  34366  ballotlemfp1  34456  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemic  34471  ballotlem1c  34472  ballotlemsgt1  34475  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemsi  34479  ballotlemsima  34480  ballotlem1ri  34499  sgn0bi  34512  signstfvn  34546  signsvtn0  34547  signstfveq0  34554  signsvfn  34559  signsvtn  34561  signshf  34565  hashreprin  34597  circlemeth  34617  logdivsqrle  34627  revpfxsfxrev  35083  revwlk  35092  swrdwlk  35094  subfacp1lem1  35147  subfacp1lem5  35152  cvxpconn  35210  sinccvglem  35640  divcnvlin  35695  bcm1nt  35699  bcprod  35700  bccolsum  35701  iprodgam  35704  faclimlem1  35705  faclimlem2  35706  faclimlem3  35707  faclim  35708  iprodfac  35709  faclim2  35710  fwddifnp1  36129  dnizphlfeqhlf  36442  dnibndlem3  36446  dnibndlem13  36456  unblimceq0  36473  knoppndvlem6  36483  knoppndvlem9  36486  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem16  36493  knoppndvlem17  36494  bj-bary1lem1  37277  irrdiff  37292  poimirlem25  37605  poimirlem26  37606  poimirlem32  37612  opnmbllem0  37616  itg2addnclem2  37632  dvasin  37664  dvacos  37665  areacirclem1  37668  areacirclem4  37671  areacirc  37673  bfp  37784  fzsplitnd  41939  lcmfunnnd  41969  lcmineqlem1  41986  lcmineqlem3  41988  lcmineqlem4  41989  lcmineqlem7  41992  lcmineqlem8  41993  lcmineqlem10  41995  lcmineqlem11  41996  lcmineqlem12  41997  lcmineqlem18  42003  lcmineqlem19  42004  lcmineqlem22  42007  lcmineqlem23  42008  dvrelogpow2b  42025  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p3  42035  aks4d1p7d1  42039  primrootsunit1  42054  posbezout  42057  primrootscoprbij  42059  primrootspoweq0  42063  aks6d1c1  42073  hashscontpow1  42078  2np3bcnp1  42101  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones16  42119  sticksstones22  42125  aks6d1c6lem3  42129  aks6d1c7lem1  42137  unitscyglem5  42156  metakunt8  42169  metakunt12  42173  metakunt15  42176  metakunt16  42177  metakunt28  42189  nnadd1com  42256  nnaddcom  42257  nnadddir  42259  nnmul1com  42260  nnmulcom  42261  fz1sump1  42298  oddnumth  42299  nicomachus  42300  sumcubes  42301  tan3rdpi  42338  reixi  42398  sn-mullid  42411  sn-0tie0  42415  renegmulnnass  42429  fiabv  42491  fltnltalem  42617  fltnlta  42618  3cubeslem1  42640  3cubeslem2  42641  3cubeslem4  42645  pell1qrge1  42826  rmspecfund  42865  acongeq  42940  jm2.18  42945  jm2.19lem3  42948  jm2.25  42956  jm2.16nn0  42961  jm3.1lem1  42974  jm3.1lem2  42975  areaquad  43177  relexpmulnn  43671  relexpaddss  43680  cvgdvgrat  44282  radcnvrat  44283  hashnzfzclim  44291  ofdivrec  44295  expgrowthi  44302  bccm1k  44311  dvradcnv2  44316  binomcxplemwb  44317  binomcxplemnn0  44318  binomcxplemrat  44319  binomcxplemfrat  44320  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  refsum2cnlem1  44937  fzisoeu  45215  fperiodmullem  45218  fzdifsuc2  45225  xralrple2  45269  nnsplit  45273  infleinflem2  45286  fmul01lt1lem2  45506  fprodcn  45521  clim1fr1  45522  isumneg  45523  climneg  45531  sumnnodd  45551  reclimc  45574  coseq0  45785  coskpi2  45787  cosknegpi  45790  fprodcncf  45821  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnxpaek  45863  dvnmul  45864  dvmptfprod  45866  dvnprodlem3  45869  itgsinexp  45876  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stoweidlem1  45922  stoweidlem7  45928  stoweidlem10  45931  stoweidlem11  45932  stoweidlem14  45935  stoweidlem17  45938  stoweidlem34  45955  stoweidlem42  45963  wallispilem3  45988  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem15  46009  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem11  46039  fourierdlem15  46043  fourierdlem26  46054  fourierdlem36  46064  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem56  46083  fourierdlem58  46085  fourierdlem59  46086  fourierdlem62  46089  fourierdlem64  46091  fourierdlem65  46092  fourierdlem78  46105  fourierdlem79  46106  sqwvfoura  46149  fourierswlem  46151  fouriersw  46152  etransclem23  46178  etransclem24  46179  etransclem28  46183  etransclem35  46190  etransclem38  46193  nnfoctbdjlem  46376  smfmullem1  46712  sigaradd  46787  deccarry  47226  fargshiftf1  47315  fargshiftfo  47316  fmtnof1  47409  sqrtpwpw2p  47412  fmtnorec2lem  47416  fmtnorec4  47423  fmtnoprmfac1lem  47438  fmtnoprmfac1  47439  fmtnoprmfac2  47441  2pwp1prm  47463  mod42tp1mod8  47476  sfprmdvdsmersenne  47477  lighneallem3  47481  lighneallem4  47484  onego  47520  zofldiv2ALTV  47536  oexpnegALTV  47551  opoeALTV  47557  opeoALTV  47558  epee  47579  perfectALTVlem1  47595  fppr2odd  47605  fpprwppr  47613  0nodd  47893  2nodd  47895  nnsgrpnmnd  47901  1neven  47961  altgsumbc  48077  pw2m1lepw2m1  48249  m1modmmod  48255  zofldiv2  48265  nnpw2pmod  48317  blen1b  48322  blennn0em1  48325  dignn0flhalflem1  48349  dignn0flhalflem2  48350  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  nn0sumshdiglem2  48356  itcovalpclem2  48405  ackval1  48415  ackval2  48416  ackval3  48417  affineid  48438  1subrec1sub  48439  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2vlinest  48475