Theorem 1cnd 11253

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  1c1 11153

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

This theorem is referenced by:  adddirp1d  11284  1p1times  11429  addcom  11444  addcomd  11460  muladd11r  11471  pncan1  11684  npcan1  11685  muls1d  11720  mulsubfacd  11721  recrec  11961  rec11  11962  rec11r  11963  rereccl  11982  subrec  12093  nn1m1nn  12284  add1p1  12514  sub1m1  12515  cnm2m1cnm3  12516  xp1d2m1eqxm1d2  12517  div4p1lem1div2  12518  nn0n0n1ge2  12591  zneo  12698  rpnnen1lem5  13020  lincmb01cmp  13531  iccf1o  13532  xov1plusxeqvd  13534  zpnn0elfzo1  13774  ubmelm1fzo  13798  fzosplitpr  13811  fzosplitprm1  13812  fzoshftral  13819  fladdz  13861  2tnp1ge0ge0  13865  ltdifltdiv  13870  dfceil2  13875  negmod  13953  modnegd  13963  addmodlteq  13983  binom2sub1  14256  binom3  14259  zesq  14261  sqoddm1div8  14278  bcm1k  14350  bcp1n  14351  bcp1m1  14355  bcpasc  14356  bcn2m1  14359  hashfz  14462  hashfzo  14464  hashfzp1  14466  hashf1lem2  14491  hashf1  14492  hashdifsnp1  14541  lswccatn0lsw  14625  ccatws1lenp1b  14655  revccat  14800  repswrevw  14821  cshwidxm1  14841  cshwidxn  14843  cshweqrep  14855  cshimadifsn0  14865  swrds2m  14976  swrd2lsw  14987  relexpaddnn  15086  absexpz  15340  reccn2  15629  rlimno1  15686  isercolllem1  15697  isercoll2  15701  iseraltlem2  15715  iseraltlem3  15716  fsump1  15788  hashiun  15854  hash2iun1dif1  15856  binomlem  15861  bcxmas  15867  incexc  15869  incexc2  15870  climcndslem1  15881  arisum  15892  arisum2  15893  trireciplem  15894  pwdif  15900  pwm1geoser  15901  geolim2  15903  georeclim  15904  mertenslem1  15916  prodfrec  15927  ntrivcvg  15929  ntrivcvgtail  15932  prodrblem  15961  prodmolem2a  15966  fprodntriv  15974  prod1  15976  fprodser  15981  fprodcl  15984  fprodm1  15999  fprodp1  16001  fprodclf  16024  risefacval2  16042  fallfacval2  16043  risefacp1  16061  fallfacp1  16062  risefacfac  16067  fallfacfwd  16068  binomfallfaclem2  16072  fallfacval4  16075  bpolydiflem  16086  ef0lem  16110  tanaddlem  16198  tanadd  16199  cos01bnd  16218  oddm1even  16376  oddp1even  16377  oexpneg  16378  ltoddhalfle  16394  halfleoddlt  16395  nn0ob  16417  pwp1fsum  16424  flodddiv4  16448  bitsp1o  16466  bitsf1  16479  sadcp1  16488  qredeu  16691  prmdiv  16818  prmdiveq  16819  vfermltlALT  16835  pc2dvds  16912  4sqlem11  16988  4sqlem12  16989  vdwapun  17007  vdwlem3  17016  vdwlem6  17019  vdwlem9  17022  ramub1lem2  17060  prmop1  17071  prmdvdsprmo  17075  prmgaplem8  17091  cshwshashnsame  17137  gsumsgrpccat  18865  psgnunilem5  19526  psgnunilem2  19527  sylow1lem1  19630  efgredlemc  19777  odadd2  19881  ablsimpgfindlem1  20141  srgbinomlem3  20245  srgbinomlem4  20246  cncrng  21418  cncrngOLD  21419  gzrngunit  21468  zringunit  21494  prmirredlem  21500  pzriprnglem12  21520  freshmansdream  21610  mhppwdeg  22171  psdmul  22187  cayhamlem1  22887  expcn  24909  expcnOLD  24911  iirevcn  24970  iihalf2cn  24975  iihalf2cnOLD  24976  icchmeo  24984  icchmeoOLD  24985  icopnfcnv  24986  icopnfhmeo  24987  evth  25004  pcoass  25070  pjthlem1  25484  ovolunlem1a  25544  ovolunlem1  25545  opnmbllem  25649  mbfi1fseqlem6  25769  bddibl  25889  dvnadd  25979  dvmptid  26009  dvmptdiv  26026  dvcnvlem  26028  dveflem  26031  dvef  26032  dvsincos  26033  dvlipcn  26047  dvivthlem1  26061  lhop2  26068  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgpowd  26105  ply1divex  26190  fta1glem1  26221  dgrcolem1  26327  dgrcolem2  26328  vieta1lem1  26366  aaliou3lem2  26399  aaliou3lem8  26401  dvtaylp  26426  dvntaylp  26427  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  abelthlem1  26489  abelthlem2  26490  abelthlem6  26494  abelthlem7  26496  logdivlti  26676  advlog  26710  advlogexp  26711  logtayl  26716  cxpmul2  26745  dvcxp1  26796  dvcxp2  26797  dvcncxp1  26799  dvcnsqrt  26800  loglesqrt  26818  relogbdiv  26836  ang180lem4  26869  ang180lem5  26870  isosctrlem2  26876  isosctrlem3  26877  affineequiv  26880  affineequiv2  26881  affineequiv3  26882  angpieqvdlem  26885  chordthmlem2  26890  chordthmlem3  26891  chordthmlem5  26893  dcubic2  26901  dcubic  26903  quart1lem  26912  quart1  26913  quart  26918  asinlem  26925  asinlem3  26928  atansopn  26989  dvatan  26992  leibpi  26999  birthdaylem2  27009  efrlim  27026  efrlimOLD  27027  cxplim  27029  divsqrtsumlem  27037  logdifbnd  27051  emcllem2  27054  emcllem3  27055  emcllem5  27057  zetacvg  27072  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgamcvg2  27112  gamcvg  27113  gamcvg2lem  27116  lgam1  27121  gamfac  27124  wilthlem2  27126  wilthimp  27129  ftalem5  27134  basellem3  27140  basellem5  27142  basellem8  27145  basellem9  27146  sqff1o  27239  muinv  27250  logfaclbnd  27280  logfacrlim  27282  logexprlim  27283  perfectlem2  27288  dchr1cl  27309  dchrinvcl  27311  dchrfi  27313  dchr1  27315  dchrsum2  27326  bcmono  27335  bcp1ctr  27337  bclbnd  27338  bposlem9  27350  gausslemma2dlem1a  27423  gausslemma2dlem5  27429  lgseisenlem4  27436  lgsquadlem1  27438  m1lgs  27446  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2lgslem3d1  27461  2lgsoddprmlem1  27466  2sqlem8  27484  2sq2  27491  addsqn2reu  27499  addsqrexnreu  27500  addsqnreup  27501  addsq2nreurex  27502  chtppilim  27533  rpvmasumlem  27545  dchrisumlem1  27547  dchrisum0re  27571  dchrisum0lem2a  27575  mudivsum  27588  mulogsumlem  27589  mulogsum  27590  2vmadivsumlem  27598  selberg4lem1  27618  pntrsumo1  27623  selberg34r  27629  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntibndlem2  27649  pntlemg  27656  pntlemr  27660  pntlemf  27663  pntlemk  27664  pntlemo  27665  pntlem3  27667  ostth2lem2  27692  ttgcontlem1  28913  cusgrsize2inds  29485  wlklenvclwlk  29687  pthdadjvtx  29762  crctcshwlkn0lem1  29839  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  wlklnwwlkln2lem  29911  wlknwwlksnbij  29917  wwlksnred  29921  wwlksnext  29922  wwlksnextbi  29923  wwlksnredwwlkn  29924  wwlksnextwrd  29926  wwlksnextinj  29928  wwlksnextproplem2  29939  wwlksnextproplem3  29940  clwwlkccatlem  30017  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlklem3  30029  clwlkclwwlk  30030  clwwisshclwwslemlem  30041  clwwisshclwws  30043  clwwlkel  30074  clwwlkf  30075  clwwlkwwlksb  30082  clwwlkext2edg  30084  wwlksext2clwwlk  30085  clwwlknonex2lem1  30135  clwwlknonex2lem2  30136  eucrct2eupth  30273  numclwwlk1lem2foalem  30379  numclwwlk1lem2fo  30386  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  numclwwlk6  30418  smcnlem  30725  fzm1ne1  32796  bcm1n  32802  fzom1ne1  32808  ltesubnnd  32828  wrdt2ind  32922  chnub  32985  chnlt  32986  omndmul2  33071  psgnfzto1stlem  33102  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  archirngz  33178  archiabllem1a  33180  archiabllem2c  33184  ccfldextdgrr  33696  constrfin  33750  2sqr3minply  33752  1smat1  33764  madjusmdetlem2  33788  madjusmdetlem4  33790  dya2icoseg  34258  iwrdsplit  34368  fibp1  34382  ballotlemfp1  34472  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemic  34487  ballotlem1c  34488  ballotlemsgt1  34491  ballotlemsdom  34492  ballotlemsel1i  34493  ballotlemsi  34495  ballotlemsima  34496  ballotlem1ri  34515  sgn0bi  34528  signstfvn  34562  signsvtn0  34563  signstfveq0  34570  signsvfn  34575  signsvtn  34577  signshf  34581  hashreprin  34613  circlemeth  34633  logdivsqrle  34643  revpfxsfxrev  35099  revwlk  35108  swrdwlk  35110  subfacp1lem1  35163  subfacp1lem5  35168  cvxpconn  35226  sinccvglem  35656  divcnvlin  35712  bcm1nt  35716  bcprod  35717  bccolsum  35718  iprodgam  35721  faclimlem1  35722  faclimlem2  35723  faclimlem3  35724  faclim  35725  iprodfac  35726  faclim2  35727  fwddifnp1  36146  dnizphlfeqhlf  36458  dnibndlem3  36462  dnibndlem13  36472  unblimceq0  36489  knoppndvlem6  36499  knoppndvlem9  36502  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem16  36509  knoppndvlem17  36510  bj-bary1lem1  37293  irrdiff  37308  poimirlem25  37631  poimirlem26  37632  poimirlem32  37638  opnmbllem0  37642  itg2addnclem2  37658  dvasin  37690  dvacos  37691  areacirclem1  37694  areacirclem4  37697  areacirc  37699  bfp  37810  fzsplitnd  41963  lcmfunnnd  41993  lcmineqlem1  42010  lcmineqlem3  42012  lcmineqlem4  42013  lcmineqlem7  42016  lcmineqlem8  42017  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem12  42021  lcmineqlem18  42027  lcmineqlem19  42028  lcmineqlem22  42031  lcmineqlem23  42032  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p3  42059  aks4d1p7d1  42063  primrootsunit1  42078  posbezout  42081  primrootscoprbij  42083  primrootspoweq0  42087  aks6d1c1  42097  hashscontpow1  42102  2np3bcnp1  42125  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones16  42143  sticksstones22  42149  aks6d1c6lem3  42153  aks6d1c7lem1  42161  unitscyglem5  42180  metakunt8  42193  metakunt12  42197  metakunt15  42200  metakunt16  42201  metakunt28  42213  nnadd1com  42280  nnaddcom  42281  nnadddir  42283  nnmul1com  42284  nnmulcom  42285  fz1sump1  42322  oddnumth  42323  nicomachus  42324  sumcubes  42325  tan3rdpi  42364  redvmptabs  42368  readvrec  42370  reixi  42428  sn-mullid  42441  sn-0tie0  42445  renegmulnnass  42459  fiabv  42522  fltnltalem  42648  fltnlta  42649  3cubeslem1  42671  3cubeslem2  42672  3cubeslem4  42676  pell1qrge1  42857  rmspecfund  42896  acongeq  42971  jm2.18  42976  jm2.19lem3  42979  jm2.25  42987  jm2.16nn0  42992  jm3.1lem1  43005  jm3.1lem2  43006  areaquad  43204  relexpmulnn  43698  relexpaddss  43707  cvgdvgrat  44308  radcnvrat  44309  hashnzfzclim  44317  ofdivrec  44321  expgrowthi  44328  bccm1k  44337  dvradcnv2  44342  binomcxplemwb  44343  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemfrat  44346  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  refsum2cnlem1  44974  fzisoeu  45250  fperiodmullem  45253  fzdifsuc2  45260  xralrple2  45303  nnsplit  45307  infleinflem2  45320  fmul01lt1lem2  45540  fprodcn  45555  clim1fr1  45556  isumneg  45557  climneg  45565  sumnnodd  45585  reclimc  45608  coseq0  45819  coskpi2  45821  cosknegpi  45824  fprodcncf  45855  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnxpaek  45897  dvnmul  45898  dvmptfprod  45900  dvnprodlem3  45903  itgsinexp  45910  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem1  45956  stoweidlem7  45962  stoweidlem10  45965  stoweidlem11  45966  stoweidlem14  45969  stoweidlem17  45972  stoweidlem34  45989  stoweidlem42  45997  wallispilem3  46022  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem15  46043  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem11  46073  fourierdlem15  46077  fourierdlem26  46088  fourierdlem36  46098  fourierdlem40  46102  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem56  46117  fourierdlem58  46119  fourierdlem59  46120  fourierdlem62  46123  fourierdlem64  46125  fourierdlem65  46126  fourierdlem78  46139  fourierdlem79  46140  sqwvfoura  46183  fourierswlem  46185  fouriersw  46186  etransclem23  46212  etransclem24  46213  etransclem28  46217  etransclem35  46224  etransclem38  46227  nnfoctbdjlem  46410  smfmullem1  46746  sigaradd  46821  deccarry  47260  m1modne  47287  fargshiftf1  47365  fargshiftfo  47366  fmtnof1  47459  sqrtpwpw2p  47462  fmtnorec2lem  47466  fmtnorec4  47473  fmtnoprmfac1lem  47488  fmtnoprmfac1  47489  fmtnoprmfac2  47491  2pwp1prm  47513  mod42tp1mod8  47526  sfprmdvdsmersenne  47527  lighneallem3  47531  lighneallem4  47534  onego  47570  zofldiv2ALTV  47586  oexpnegALTV  47601  opoeALTV  47607  opeoALTV  47608  epee  47629  perfectALTVlem1  47645  fppr2odd  47655  fpprwppr  47663  gpg3nbgrvtx0  47966  0nodd  48013  2nodd  48015  nnsgrpnmnd  48021  1neven  48081  altgsumbc  48196  pw2m1lepw2m1  48365  m1modmmod  48370  zofldiv2  48380  nnpw2pmod  48432  blen1b  48437  blennn0em1  48440  dignn0flhalflem1  48464  dignn0flhalflem2  48465  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  nn0sumshdiglem2  48471  itcovalpclem2  48520  ackval1  48530  ackval2  48531  ackval3  48532  affineid  48553  1subrec1sub  48554  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2vlinest  48590