Theorem 1cnd 11215

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

Syntax hints:   → wi 4   ∈ wcel 2104  ℂcc 11112  1c1 11115

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

This theorem is referenced by:  adddirp1d  11246  1p1times  11391  addcom  11406  addcomd  11422  muladd11r  11433  pncan1  11644  npcan1  11645  muls1d  11680  mulsubfacd  11681  recrec  11917  rec11  11918  rec11r  11919  rereccl  11938  subrec  12049  nn1m1nn  12239  add1p1  12469  sub1m1  12470  cnm2m1cnm3  12471  xp1d2m1eqxm1d2  12472  div4p1lem1div2  12473  nn0n0n1ge2  12545  zneo  12651  rpnnen1lem5  12971  lincmb01cmp  13478  iccf1o  13479  xov1plusxeqvd  13481  zpnn0elfzo1  13712  ubmelm1fzo  13734  fzosplitpr  13747  fzosplitprm1  13748  fzoshftral  13755  fladdz  13796  2tnp1ge0ge0  13800  ltdifltdiv  13805  dfceil2  13810  negmod  13887  modnegd  13897  addmodlteq  13917  binom2sub1  14190  binom3  14193  zesq  14195  sqoddm1div8  14212  bcm1k  14281  bcp1n  14282  bcp1m1  14286  bcpasc  14287  bcn2m1  14290  hashfz  14393  hashfzo  14395  hashfzp1  14397  hashf1lem2  14423  hashf1  14424  hashdifsnp1  14463  lswccatn0lsw  14547  ccatws1lenp1b  14577  revccat  14722  repswrevw  14743  cshwidxm1  14763  cshwidxn  14765  cshweqrep  14777  cshimadifsn0  14787  swrds2m  14898  swrd2lsw  14909  relexpaddnn  15004  absexpz  15258  reccn2  15547  rlimno1  15606  isercolllem1  15617  isercoll2  15621  iseraltlem2  15635  iseraltlem3  15636  fsump1  15708  hashiun  15774  hash2iun1dif1  15776  binomlem  15781  bcxmas  15787  incexc  15789  incexc2  15790  climcndslem1  15801  arisum  15812  arisum2  15813  trireciplem  15814  pwdif  15820  pwm1geoser  15821  geolim2  15823  georeclim  15824  mertenslem1  15836  prodfrec  15847  ntrivcvg  15849  ntrivcvgtail  15852  prodrblem  15879  prodmolem2a  15884  fprodntriv  15892  prod1  15894  fprodser  15899  fprodcl  15902  fprodm1  15917  fprodp1  15919  fprodclf  15942  risefacval2  15960  fallfacval2  15961  risefacp1  15979  fallfacp1  15980  risefacfac  15985  fallfacfwd  15986  binomfallfaclem2  15990  fallfacval4  15993  bpolydiflem  16004  ef0lem  16028  tanaddlem  16115  tanadd  16116  cos01bnd  16135  oddm1even  16292  oddp1even  16293  oexpneg  16294  ltoddhalfle  16310  halfleoddlt  16311  nn0ob  16333  pwp1fsum  16340  flodddiv4  16362  bitsp1o  16380  bitsf1  16393  sadcp1  16402  qredeu  16601  prmdiv  16724  prmdiveq  16725  vfermltlALT  16741  pc2dvds  16818  4sqlem11  16894  4sqlem12  16895  vdwapun  16913  vdwlem3  16922  vdwlem6  16925  vdwlem9  16928  ramub1lem2  16966  prmop1  16977  prmdvdsprmo  16981  prmgaplem8  16997  cshwshashnsame  17043  gsumsgrpccat  18759  psgnunilem5  19405  psgnunilem2  19406  sylow1lem1  19509  efgredlemc  19656  odadd2  19760  ablsimpgfindlem1  20020  srgbinomlem3  20124  srgbinomlem4  20125  cncrng  21168  gzrngunit  21213  zringunit  21239  prmirredlem  21245  pzriprnglem12  21263  mhppwdeg  21914  cayhamlem1  22590  expcn  24612  expcnOLD  24614  iirevcn  24673  iihalf2cn  24678  iihalf2cnOLD  24679  icchmeo  24687  icchmeoOLD  24688  icopnfcnv  24689  icopnfhmeo  24690  evth  24707  pcoass  24773  pjthlem1  25187  ovolunlem1a  25247  ovolunlem1  25248  opnmbllem  25352  mbfi1fseqlem6  25472  bddibl  25591  dvnadd  25680  dvmptid  25708  dvmptdiv  25725  dvcnvlem  25727  dveflem  25730  dvef  25731  dvsincos  25732  dvlipcn  25745  dvivthlem1  25759  lhop2  25766  dvcvx  25771  dvfsumle  25772  dvfsumabs  25774  dvfsumlem1  25777  dvfsumlem2  25778  itgpowd  25801  ply1divex  25888  fta1glem1  25917  dgrcolem1  26021  dgrcolem2  26022  vieta1lem1  26057  aaliou3lem2  26090  aaliou3lem8  26092  dvtaylp  26116  dvntaylp  26117  taylthlem1  26119  taylthlem2  26120  abelthlem1  26177  abelthlem2  26178  abelthlem6  26182  abelthlem7  26184  logdivlti  26362  advlog  26396  advlogexp  26397  logtayl  26402  cxpmul2  26431  dvcxp1  26482  dvcxp2  26483  dvcncxp1  26485  dvcnsqrt  26486  loglesqrt  26500  relogbdiv  26518  ang180lem4  26551  ang180lem5  26552  isosctrlem2  26558  isosctrlem3  26559  affineequiv  26562  affineequiv2  26563  affineequiv3  26564  angpieqvdlem  26567  chordthmlem2  26572  chordthmlem3  26573  chordthmlem5  26575  dcubic2  26583  dcubic  26585  quart1lem  26594  quart1  26595  quart  26600  asinlem  26607  asinlem3  26610  atansopn  26671  dvatan  26674  leibpi  26681  birthdaylem2  26691  efrlim  26708  cxplim  26710  divsqrtsumlem  26718  logdifbnd  26732  emcllem2  26735  emcllem3  26736  emcllem5  26738  zetacvg  26753  lgamgulmlem2  26768  lgamgulmlem3  26769  lgamgulmlem4  26770  lgamgulmlem5  26771  lgamgulmlem6  26772  lgamgulm2  26774  lgamcvg2  26793  gamcvg  26794  gamcvg2lem  26797  lgam1  26802  gamfac  26805  wilthlem2  26807  wilthimp  26810  ftalem5  26815  basellem3  26821  basellem5  26823  basellem8  26826  basellem9  26827  sqff1o  26920  muinv  26931  logfaclbnd  26959  logfacrlim  26961  logexprlim  26962  perfectlem2  26967  dchr1cl  26988  dchrinvcl  26990  dchrfi  26992  dchr1  26994  dchrsum2  27005  bcmono  27014  bcp1ctr  27016  bclbnd  27017  bposlem9  27029  gausslemma2dlem1a  27102  gausslemma2dlem5  27108  lgseisenlem4  27115  lgsquadlem1  27117  m1lgs  27125  2lgslem3a  27133  2lgslem3b  27134  2lgslem3c  27135  2lgslem3d  27136  2lgslem3d1  27140  2lgsoddprmlem1  27145  2sqlem8  27163  2sq2  27170  addsqn2reu  27178  addsqrexnreu  27179  addsqnreup  27180  addsq2nreurex  27181  chtppilim  27212  rpvmasumlem  27224  dchrisumlem1  27226  dchrisum0re  27250  dchrisum0lem2a  27254  mudivsum  27267  mulogsumlem  27268  mulogsum  27269  2vmadivsumlem  27277  selberg4lem1  27297  pntrsumo1  27302  selberg34r  27308  pntrlog2bndlem2  27315  pntrlog2bndlem4  27317  pntrlog2bndlem5  27318  pntrlog2bndlem6  27320  pntibndlem2  27328  pntlemg  27335  pntlemr  27339  pntlemf  27342  pntlemk  27343  pntlemo  27344  pntlem3  27346  ostth2lem2  27371  ttgcontlem1  28407  cusgrsize2inds  28975  wlklenvclwlk  29177  pthdadjvtx  29252  crctcshwlkn0lem1  29329  crctcshwlkn0lem4  29332  crctcshwlkn0lem5  29333  wlklnwwlkln2lem  29401  wlknwwlksnbij  29407  wwlksnred  29411  wwlksnext  29412  wwlksnextbi  29413  wwlksnredwwlkn  29414  wwlksnextwrd  29416  wwlksnextinj  29418  wwlksnextproplem2  29429  wwlksnextproplem3  29430  clwwlkccatlem  29507  clwlkclwwlklem2a1  29510  clwlkclwwlklem2a4  29515  clwlkclwwlklem2a  29516  clwlkclwwlklem2  29518  clwlkclwwlklem3  29519  clwlkclwwlk  29520  clwwisshclwwslemlem  29531  clwwisshclwws  29533  clwwlkel  29564  clwwlkf  29565  clwwlkwwlksb  29572  clwwlkext2edg  29574  wwlksext2clwwlk  29575  clwwlknonex2lem1  29625  clwwlknonex2lem2  29626  eucrct2eupth  29763  numclwwlk1lem2foalem  29869  numclwwlk1lem2fo  29876  numclwlk2lem2f  29895  numclwlk2lem2f1o  29897  numclwwlk6  29908  smcnlem  30215  fzm1ne1  32265  bcm1n  32271  fzom1ne1  32277  ltesubnnd  32293  wrdt2ind  32382  omndmul2  32498  psgnfzto1stlem  32527  cycpmco2lem3  32555  cycpmco2lem4  32556  cycpmco2lem5  32557  cycpmco2lem6  32558  cycpmco2lem7  32559  cycpmco2  32560  archirngz  32603  archiabllem1a  32605  archiabllem2c  32609  freshmansdream  32649  ccfldextdgrr  33033  1smat1  33080  madjusmdetlem2  33104  madjusmdetlem4  33106  dya2icoseg  33572  iwrdsplit  33682  fibp1  33696  ballotlemfp1  33786  ballotlemfc0  33787  ballotlemfcc  33788  ballotlemic  33801  ballotlem1c  33802  ballotlemsgt1  33805  ballotlemsdom  33806  ballotlemsel1i  33807  ballotlemsi  33809  ballotlemsima  33810  ballotlem1ri  33829  sgn0bi  33842  signstfvn  33876  signsvtn0  33877  signstfveq0  33884  signsvfn  33889  signsvtn  33891  signshf  33895  hashreprin  33928  circlemeth  33948  logdivsqrle  33958  revpfxsfxrev  34402  revwlk  34411  swrdwlk  34413  subfacp1lem1  34466  subfacp1lem5  34471  cvxpconn  34529  sinccvglem  34953  divcnvlin  35004  bcm1nt  35009  bcprod  35010  bccolsum  35011  iprodgam  35014  faclimlem1  35015  faclimlem2  35016  faclimlem3  35017  faclim  35018  iprodfac  35019  faclim2  35020  fwddifnp1  35439  gg-dvfsumle  35470  gg-dvfsumlem2  35471  gg-cncrng  35488  gg-cnfld1  35489  dnizphlfeqhlf  35657  dnibndlem3  35661  dnibndlem13  35671  unblimceq0  35688  knoppndvlem6  35698  knoppndvlem9  35701  knoppndvlem14  35706  knoppndvlem15  35707  knoppndvlem16  35708  knoppndvlem17  35709  bj-bary1lem1  36497  irrdiff  36512  poimirlem25  36818  poimirlem26  36819  poimirlem32  36825  opnmbllem0  36829  itg2addnclem2  36845  dvasin  36877  dvacos  36878  areacirclem1  36881  areacirclem4  36884  areacirc  36886  bfp  36997  fzsplitnd  41156  lcmfunnnd  41185  lcmineqlem1  41202  lcmineqlem3  41204  lcmineqlem4  41205  lcmineqlem7  41208  lcmineqlem8  41209  lcmineqlem10  41211  lcmineqlem11  41212  lcmineqlem12  41213  lcmineqlem18  41219  lcmineqlem19  41220  lcmineqlem22  41223  lcmineqlem23  41224  dvrelogpow2b  41241  aks4d1p1p4  41244  aks4d1p1p6  41246  aks4d1p1p7  41247  aks4d1p1p5  41248  aks4d1p1  41249  aks4d1p3  41251  aks4d1p7d1  41255  2np3bcnp1  41268  sticksstones10  41279  sticksstones12a  41281  sticksstones12  41282  sticksstones16  41286  sticksstones22  41292  metakunt8  41300  metakunt12  41304  metakunt15  41307  metakunt16  41308  metakunt28  41320  nnadd1com  41485  nnaddcom  41486  nnadddir  41488  nnmul1com  41489  nnmulcom  41490  fz1sump1  41512  oddnumth  41513  nicomachus  41514  sumcubes  41515  reixi  41599  sn-mullid  41612  sn-0tie0  41616  renegmulnnass  41630  fltnltalem  41708  fltnlta  41709  3cubeslem1  41726  3cubeslem2  41727  3cubeslem4  41731  pell1qrge1  41912  rmspecfund  41951  acongeq  42026  jm2.18  42031  jm2.19lem3  42034  jm2.25  42042  jm2.16nn0  42047  jm3.1lem1  42060  jm3.1lem2  42061  areaquad  42269  relexpmulnn  42764  relexpaddss  42773  cvgdvgrat  43376  radcnvrat  43377  hashnzfzclim  43385  ofdivrec  43389  expgrowthi  43396  bccm1k  43405  dvradcnv2  43410  binomcxplemwb  43411  binomcxplemnn0  43412  binomcxplemrat  43413  binomcxplemfrat  43414  binomcxplemdvbinom  43416  binomcxplemnotnn0  43419  refsum2cnlem1  44025  fzisoeu  44310  fperiodmullem  44313  fzdifsuc2  44320  xralrple2  44364  nnsplit  44368  infleinflem2  44381  fmul01lt1lem2  44601  fprodcn  44616  clim1fr1  44617  isumneg  44618  climneg  44626  sumnnodd  44646  reclimc  44669  coseq0  44880  coskpi2  44882  cosknegpi  44885  fprodcncf  44916  fprodsubrecnncnvlem  44923  fprodaddrecnncnvlem  44925  ioodvbdlimc1lem2  44948  ioodvbdlimc2lem  44950  dvnxpaek  44958  dvnmul  44959  dvmptfprod  44961  dvnprodlem3  44964  itgsinexp  44971  itgiccshift  44996  itgperiod  44997  itgsbtaddcnst  44998  stoweidlem1  45017  stoweidlem7  45023  stoweidlem10  45026  stoweidlem11  45027  stoweidlem14  45030  stoweidlem17  45033  stoweidlem34  45050  stoweidlem42  45058  wallispilem3  45083  wallispilem5  45085  wallispi  45086  wallispi2lem1  45087  wallispi2lem2  45088  wallispi2  45089  stirlinglem1  45090  stirlinglem3  45092  stirlinglem4  45093  stirlinglem5  45094  stirlinglem6  45095  stirlinglem7  45096  stirlinglem8  45097  stirlinglem10  45099  stirlinglem11  45100  stirlinglem12  45101  stirlinglem13  45102  stirlinglem15  45104  dirkertrigeqlem2  45115  dirkertrigeqlem3  45116  dirkertrigeq  45117  dirkercncflem1  45119  dirkercncflem2  45120  dirkercncflem4  45122  fourierdlem11  45134  fourierdlem15  45138  fourierdlem26  45149  fourierdlem36  45159  fourierdlem40  45163  fourierdlem41  45164  fourierdlem42  45165  fourierdlem48  45170  fourierdlem49  45171  fourierdlem56  45178  fourierdlem58  45180  fourierdlem59  45181  fourierdlem62  45184  fourierdlem64  45186  fourierdlem65  45187  fourierdlem78  45200  fourierdlem79  45201  sqwvfoura  45244  fourierswlem  45246  fouriersw  45247  etransclem23  45273  etransclem24  45274  etransclem28  45278  etransclem35  45285  etransclem38  45288  nnfoctbdjlem  45471  smfmullem1  45807  sigaradd  45882  deccarry  46319  fargshiftf1  46409  fargshiftfo  46410  fmtnof1  46503  sqrtpwpw2p  46506  fmtnorec2lem  46510  fmtnorec4  46517  fmtnoprmfac1lem  46532  fmtnoprmfac1  46533  fmtnoprmfac2  46535  2pwp1prm  46557  mod42tp1mod8  46570  sfprmdvdsmersenne  46571  lighneallem3  46575  lighneallem4  46578  onego  46614  zofldiv2ALTV  46630  oexpnegALTV  46645  opoeALTV  46651  opeoALTV  46652  epee  46673  perfectALTVlem1  46689  fppr2odd  46699  fpprwppr  46707  0nodd  46848  2nodd  46850  nnsgrpnmnd  46856  1neven  46920  altgsumbc  47118  pw2m1lepw2m1  47290  m1modmmod  47296  zofldiv2  47306  nnpw2pmod  47358  blen1b  47363  blennn0em1  47366  dignn0flhalflem1  47390  dignn0flhalflem2  47391  nn0sumshdiglemB  47395  nn0sumshdiglem1  47396  nn0sumshdiglem2  47397  itcovalpclem2  47446  ackval1  47456  ackval2  47457  ackval3  47458  affineid  47479  1subrec1sub  47480  eenglngeehlnmlem1  47512  eenglngeehlnmlem2  47513  rrx2vlinest  47516