Theorem 1cnd 11176

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  1c1 11076

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

This theorem is referenced by:  adddirp1d  11207  1p1times  11352  addcom  11367  addcomd  11383  muladd11r  11394  pncan1  11609  npcan1  11610  muls1d  11645  mulsubfacd  11646  recrec  11886  rec11  11887  rec11r  11888  rereccl  11907  subrecd  12018  nn1m1nn  12214  add1p1  12440  sub1m1  12441  cnm2m1cnm3  12442  xp1d2m1eqxm1d2  12443  div4p1lem1div2  12444  nn0n0n1ge2  12517  zneo  12624  rpnnen1lem5  12947  lincmb01cmp  13463  iccf1o  13464  xov1plusxeqvd  13466  zpnn0elfzo1  13707  ubmelm1fzo  13731  fzosplitpr  13744  fzosplitprm1  13745  fzoshftral  13752  fladdz  13794  2tnp1ge0ge0  13798  ltdifltdiv  13803  dfceil2  13808  negmod  13888  modnegd  13898  addmodlteq  13918  binom2sub1  14193  binom3  14196  zesq  14198  sqoddm1div8  14215  bcm1k  14287  bcp1n  14288  bcp1m1  14292  bcpasc  14293  bcn2m1  14296  hashfz  14399  hashfzo  14401  hashfzp1  14403  hashf1lem2  14428  hashf1  14429  hashdifsnp1  14478  lswccatn0lsw  14563  ccatws1lenp1b  14593  revccat  14738  repswrevw  14759  cshwidxm1  14779  cshwidxn  14781  cshweqrep  14793  cshimadifsn0  14803  swrds2m  14914  swrd2lsw  14925  relexpaddnn  15024  absexpz  15278  reccn2  15570  rlimno1  15627  isercolllem1  15638  isercoll2  15642  iseraltlem2  15656  iseraltlem3  15657  fsump1  15729  hashiun  15795  hash2iun1dif1  15797  binomlem  15802  bcxmas  15808  incexc  15810  incexc2  15811  climcndslem1  15822  arisum  15833  arisum2  15834  trireciplem  15835  pwdif  15841  pwm1geoser  15842  geolim2  15844  georeclim  15845  mertenslem1  15857  prodfrec  15868  ntrivcvg  15870  ntrivcvgtail  15873  prodrblem  15902  prodmolem2a  15907  fprodntriv  15915  prod1  15917  fprodser  15922  fprodcl  15925  fprodm1  15940  fprodp1  15942  fprodclf  15965  risefacval2  15983  fallfacval2  15984  risefacp1  16002  fallfacp1  16003  risefacfac  16008  fallfacfwd  16009  binomfallfaclem2  16013  fallfacval4  16016  bpolydiflem  16027  ef0lem  16051  tanaddlem  16141  tanadd  16142  cos01bnd  16161  oddm1even  16320  oddp1even  16321  oexpneg  16322  ltoddhalfle  16338  halfleoddlt  16339  nn0ob  16361  pwp1fsum  16368  flodddiv4  16392  bitsp1o  16410  bitsf1  16423  sadcp1  16432  qredeu  16635  prmdiv  16762  prmdiveq  16763  vfermltlALT  16780  pc2dvds  16857  4sqlem11  16933  4sqlem12  16934  vdwapun  16952  vdwlem3  16961  vdwlem6  16964  vdwlem9  16967  ramub1lem2  17005  prmop1  17016  prmdvdsprmo  17020  prmgaplem8  17036  cshwshashnsame  17081  gsumsgrpccat  18774  psgnunilem5  19431  psgnunilem2  19432  sylow1lem1  19535  efgredlemc  19682  odadd2  19786  ablsimpgfindlem1  20046  srgbinomlem3  20144  srgbinomlem4  20145  cncrng  21307  cncrngOLD  21308  gzrngunit  21357  zringunit  21383  prmirredlem  21389  pzriprnglem12  21409  freshmansdream  21491  mhppwdeg  22044  psdmul  22060  cayhamlem1  22760  expcn  24770  expcnOLD  24772  iirevcn  24831  iihalf2cn  24836  iihalf2cnOLD  24837  icchmeo  24845  icchmeoOLD  24846  icopnfcnv  24847  icopnfhmeo  24848  evth  24865  pcoass  24931  pjthlem1  25344  ovolunlem1a  25404  ovolunlem1  25405  opnmbllem  25509  mbfi1fseqlem6  25628  bddibl  25748  dvnadd  25838  dvmptid  25868  dvmptdiv  25885  dvcnvlem  25887  dveflem  25890  dvef  25891  dvsincos  25892  dvlipcn  25906  dvivthlem1  25920  lhop2  25927  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgpowd  25964  ply1divex  26049  fta1glem1  26080  dgrcolem1  26186  dgrcolem2  26187  vieta1lem1  26225  aaliou3lem2  26258  aaliou3lem8  26260  dvtaylp  26285  dvntaylp  26286  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  abelthlem1  26348  abelthlem2  26349  abelthlem6  26353  abelthlem7  26355  logdivlti  26536  advlog  26570  advlogexp  26571  logtayl  26576  cxpmul2  26605  dvcxp1  26656  dvcxp2  26657  dvcncxp1  26659  dvcnsqrt  26660  loglesqrt  26678  relogbdiv  26696  ang180lem4  26729  ang180lem5  26730  isosctrlem2  26736  isosctrlem3  26737  affineequiv  26740  affineequiv2  26741  affineequiv3  26742  angpieqvdlem  26745  chordthmlem2  26750  chordthmlem3  26751  chordthmlem5  26753  dcubic2  26761  dcubic  26763  quart1lem  26772  quart1  26773  quart  26778  asinlem  26785  asinlem3  26788  atansopn  26849  dvatan  26852  leibpi  26859  birthdaylem2  26869  efrlim  26886  efrlimOLD  26887  cxplim  26889  divsqrtsumlem  26897  logdifbnd  26911  emcllem2  26914  emcllem3  26915  emcllem5  26917  zetacvg  26932  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamgulm2  26953  lgamcvg2  26972  gamcvg  26973  gamcvg2lem  26976  lgam1  26981  gamfac  26984  wilthlem2  26986  wilthimp  26989  ftalem5  26994  basellem3  27000  basellem5  27002  basellem8  27005  basellem9  27006  sqff1o  27099  muinv  27110  logfaclbnd  27140  logfacrlim  27142  logexprlim  27143  perfectlem2  27148  dchr1cl  27169  dchrinvcl  27171  dchrfi  27173  dchr1  27175  dchrsum2  27186  bcmono  27195  bcp1ctr  27197  bclbnd  27198  bposlem9  27210  gausslemma2dlem1a  27283  gausslemma2dlem5  27289  lgseisenlem4  27296  lgsquadlem1  27298  m1lgs  27306  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgslem3d1  27321  2lgsoddprmlem1  27326  2sqlem8  27344  2sq2  27351  addsqn2reu  27359  addsqrexnreu  27360  addsqnreup  27361  addsq2nreurex  27362  chtppilim  27393  rpvmasumlem  27405  dchrisumlem1  27407  dchrisum0re  27431  dchrisum0lem2a  27435  mudivsum  27448  mulogsumlem  27449  mulogsum  27450  2vmadivsumlem  27458  selberg4lem1  27478  pntrsumo1  27483  selberg34r  27489  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntibndlem2  27509  pntlemg  27516  pntlemr  27520  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntlem3  27527  ostth2lem2  27552  ttgcontlem1  28819  cusgrsize2inds  29388  wlklenvclwlk  29590  pthdadjvtx  29665  crctcshwlkn0lem1  29747  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  wlklnwwlkln2lem  29819  wlknwwlksnbij  29825  wwlksnred  29829  wwlksnext  29830  wwlksnextbi  29831  wwlksnredwwlkn  29832  wwlksnextwrd  29834  wwlksnextinj  29836  wwlksnextproplem2  29847  wwlksnextproplem3  29848  clwwlkccatlem  29925  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlklem3  29937  clwlkclwwlk  29938  clwwisshclwwslemlem  29949  clwwisshclwws  29951  clwwlkel  29982  clwwlkf  29983  clwwlkwwlksb  29990  clwwlkext2edg  29992  wwlksext2clwwlk  29993  clwwlknonex2lem1  30043  clwwlknonex2lem2  30044  eucrct2eupth  30181  numclwwlk1lem2foalem  30287  numclwwlk1lem2fo  30294  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  numclwwlk6  30326  smcnlem  30633  receqid  32675  fzm1ne1  32718  bcm1n  32725  fzom1ne1  32731  ltesubnnd  32754  sgn0bi  32772  oexpled  32779  wrdt2ind  32882  chnub  32945  chnlt  32946  omndmul2  33033  psgnfzto1stlem  33064  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  archirngz  33150  archiabllem1a  33152  archiabllem2c  33156  ccfldextdgrr  33674  constrfin  33743  nn0constr  33758  iconstr  33763  constrrecl  33766  constrimcl  33767  constrreinvcl  33769  constrinvcl  33770  constrresqrtcl  33774  2sqr3minply  33777  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminply  33785  cos9thpinconstrlem1  33786  1smat1  33801  madjusmdetlem2  33825  madjusmdetlem4  33827  dya2icoseg  34275  iwrdsplit  34385  fibp1  34399  ballotlemfp1  34490  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemic  34505  ballotlem1c  34506  ballotlemsgt1  34509  ballotlemsdom  34510  ballotlemsel1i  34511  ballotlemsi  34513  ballotlemsima  34514  ballotlem1ri  34533  signstfvn  34567  signsvtn0  34568  signstfveq0  34575  signsvfn  34580  signsvtn  34582  signshf  34586  hashreprin  34618  circlemeth  34638  logdivsqrle  34648  revpfxsfxrev  35110  revwlk  35119  swrdwlk  35121  subfacp1lem1  35173  subfacp1lem5  35178  cvxpconn  35236  sinccvglem  35666  divcnvlin  35727  bcm1nt  35731  bcprod  35732  bccolsum  35733  iprodgam  35736  faclimlem1  35737  faclimlem2  35738  faclimlem3  35739  faclim  35740  iprodfac  35741  faclim2  35742  fwddifnp1  36160  dnizphlfeqhlf  36471  dnibndlem3  36475  dnibndlem13  36485  unblimceq0  36502  knoppndvlem6  36512  knoppndvlem9  36515  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem16  36522  knoppndvlem17  36523  bj-bary1lem1  37306  irrdiff  37321  poimirlem25  37646  poimirlem26  37647  poimirlem32  37653  opnmbllem0  37657  itg2addnclem2  37673  dvasin  37705  dvacos  37706  areacirclem1  37709  areacirclem4  37712  areacirc  37714  bfp  37825  fzsplitnd  41977  lcmfunnnd  42007  lcmineqlem1  42024  lcmineqlem3  42026  lcmineqlem4  42027  lcmineqlem7  42030  lcmineqlem8  42031  lcmineqlem10  42033  lcmineqlem11  42034  lcmineqlem12  42035  lcmineqlem18  42041  lcmineqlem19  42042  lcmineqlem22  42045  lcmineqlem23  42046  dvrelogpow2b  42063  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p3  42073  aks4d1p7d1  42077  primrootsunit1  42092  posbezout  42095  primrootscoprbij  42097  primrootspoweq0  42101  aks6d1c1  42111  hashscontpow1  42116  2np3bcnp1  42139  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones16  42157  sticksstones22  42163  aks6d1c6lem3  42167  aks6d1c7lem1  42175  unitscyglem5  42194  nnadd1com  42262  nnaddcom  42263  nnadddir  42265  nnmul1com  42266  nnmulcom  42267  3rdpwhole  42287  fz1sump1  42305  oddnumth  42306  nicomachus  42307  sumcubes  42308  tan3rdpi  42347  redvmptabs  42355  readvrec  42357  reixi  42418  sn-mullid  42431  sn-0tie0  42446  renegmulnnass  42460  fiabv  42531  fltnltalem  42657  fltnlta  42658  3cubeslem1  42679  3cubeslem2  42680  3cubeslem4  42684  pell1qrge1  42865  rmspecfund  42904  acongeq  42979  jm2.18  42984  jm2.19lem3  42987  jm2.25  42995  jm2.16nn0  43000  jm3.1lem1  43013  jm3.1lem2  43014  areaquad  43212  relexpmulnn  43705  relexpaddss  43714  cvgdvgrat  44309  radcnvrat  44310  hashnzfzclim  44318  ofdivrec  44322  expgrowthi  44329  bccm1k  44338  dvradcnv2  44343  binomcxplemwb  44344  binomcxplemnn0  44345  binomcxplemrat  44346  binomcxplemfrat  44347  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  refsum2cnlem1  45038  fzisoeu  45305  fperiodmullem  45308  fzdifsuc2  45315  xralrple2  45357  nnsplit  45361  infleinflem2  45374  fmul01lt1lem2  45590  fprodcn  45605  clim1fr1  45606  isumneg  45607  climneg  45615  sumnnodd  45635  reclimc  45658  coseq0  45869  coskpi2  45871  cosknegpi  45874  fprodcncf  45905  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnxpaek  45947  dvnmul  45948  dvmptfprod  45950  dvnprodlem3  45953  itgsinexp  45960  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  stoweidlem1  46006  stoweidlem7  46012  stoweidlem10  46015  stoweidlem11  46016  stoweidlem14  46019  stoweidlem17  46022  stoweidlem34  46039  stoweidlem42  46047  wallispilem3  46072  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem15  46093  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem11  46123  fourierdlem15  46127  fourierdlem26  46138  fourierdlem36  46148  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem56  46167  fourierdlem58  46169  fourierdlem59  46170  fourierdlem62  46173  fourierdlem64  46175  fourierdlem65  46176  fourierdlem78  46189  fourierdlem79  46190  sqwvfoura  46233  fourierswlem  46235  fouriersw  46236  etransclem23  46262  etransclem24  46263  etransclem28  46267  etransclem35  46274  etransclem38  46277  nnfoctbdjlem  46460  smfmullem1  46796  sigaradd  46871  deccarry  47316  ceilbi  47338  m1modne  47353  m1modmmod  47363  modm1nep2  47373  modm1nem2  47374  fargshiftf1  47446  fargshiftfo  47447  fmtnof1  47540  sqrtpwpw2p  47543  fmtnorec2lem  47547  fmtnorec4  47554  fmtnoprmfac1lem  47569  fmtnoprmfac1  47570  fmtnoprmfac2  47572  2pwp1prm  47594  mod42tp1mod8  47607  sfprmdvdsmersenne  47608  lighneallem3  47612  lighneallem4  47615  onego  47651  zofldiv2ALTV  47667  oexpnegALTV  47682  opoeALTV  47688  opeoALTV  47689  epee  47710  perfectALTVlem1  47726  fppr2odd  47736  fpprwppr  47744  gpg3nbgrvtx0  48071  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  0nodd  48162  2nodd  48164  nnsgrpnmnd  48170  1neven  48230  altgsumbc  48344  pw2m1lepw2m1  48513  zofldiv2  48524  nnpw2pmod  48576  blen1b  48581  blennn0em1  48584  dignn0flhalflem1  48608  dignn0flhalflem2  48609  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  nn0sumshdiglem2  48615  itcovalpclem2  48664  ackval1  48674  ackval2  48675  ackval3  48676  affineid  48697  1subrec1sub  48698  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2vlinest  48734