Theorem 1cnd 11145

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  1c1 11045

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

This theorem is referenced by:  adddirp1d  11176  1p1times  11321  addcom  11336  addcomd  11352  muladd11r  11363  pncan1  11578  npcan1  11579  muls1d  11614  mulsubfacd  11615  recrec  11855  rec11  11856  rec11r  11857  rereccl  11876  subrecd  11987  nn1m1nn  12183  add1p1  12409  sub1m1  12410  cnm2m1cnm3  12411  xp1d2m1eqxm1d2  12412  div4p1lem1div2  12413  nn0n0n1ge2  12486  zneo  12593  rpnnen1lem5  12916  lincmb01cmp  13432  iccf1o  13433  xov1plusxeqvd  13435  zpnn0elfzo1  13676  ubmelm1fzo  13700  fzosplitpr  13713  fzosplitprm1  13714  fzoshftral  13721  fladdz  13763  2tnp1ge0ge0  13767  ltdifltdiv  13772  dfceil2  13777  negmod  13857  modnegd  13867  addmodlteq  13887  binom2sub1  14162  binom3  14165  zesq  14167  sqoddm1div8  14184  bcm1k  14256  bcp1n  14257  bcp1m1  14261  bcpasc  14262  bcn2m1  14265  hashfz  14368  hashfzo  14370  hashfzp1  14372  hashf1lem2  14397  hashf1  14398  hashdifsnp1  14447  lswccatn0lsw  14532  ccatws1lenp1b  14562  revccat  14707  repswrevw  14728  cshwidxm1  14748  cshwidxn  14750  cshweqrep  14762  cshimadifsn0  14772  swrds2m  14883  swrd2lsw  14894  relexpaddnn  14993  absexpz  15247  reccn2  15539  rlimno1  15596  isercolllem1  15607  isercoll2  15611  iseraltlem2  15625  iseraltlem3  15626  fsump1  15698  hashiun  15764  hash2iun1dif1  15766  binomlem  15771  bcxmas  15777  incexc  15779  incexc2  15780  climcndslem1  15791  arisum  15802  arisum2  15803  trireciplem  15804  pwdif  15810  pwm1geoser  15811  geolim2  15813  georeclim  15814  mertenslem1  15826  prodfrec  15837  ntrivcvg  15839  ntrivcvgtail  15842  prodrblem  15871  prodmolem2a  15876  fprodntriv  15884  prod1  15886  fprodser  15891  fprodcl  15894  fprodm1  15909  fprodp1  15911  fprodclf  15934  risefacval2  15952  fallfacval2  15953  risefacp1  15971  fallfacp1  15972  risefacfac  15977  fallfacfwd  15978  binomfallfaclem2  15982  fallfacval4  15985  bpolydiflem  15996  ef0lem  16020  tanaddlem  16110  tanadd  16111  cos01bnd  16130  oddm1even  16289  oddp1even  16290  oexpneg  16291  ltoddhalfle  16307  halfleoddlt  16308  nn0ob  16330  pwp1fsum  16337  flodddiv4  16361  bitsp1o  16379  bitsf1  16392  sadcp1  16401  qredeu  16604  prmdiv  16731  prmdiveq  16732  vfermltlALT  16749  pc2dvds  16826  4sqlem11  16902  4sqlem12  16903  vdwapun  16921  vdwlem3  16930  vdwlem6  16933  vdwlem9  16936  ramub1lem2  16974  prmop1  16985  prmdvdsprmo  16989  prmgaplem8  17005  cshwshashnsame  17050  gsumsgrpccat  18749  psgnunilem5  19408  psgnunilem2  19409  sylow1lem1  19512  efgredlemc  19659  odadd2  19763  ablsimpgfindlem1  20023  omndmul2  20047  srgbinomlem3  20148  srgbinomlem4  20149  cncrng  21330  cncrngOLD  21331  gzrngunit  21375  zringunit  21408  prmirredlem  21414  pzriprnglem12  21434  freshmansdream  21516  mhppwdeg  22070  psdmul  22086  cayhamlem1  22786  expcn  24796  expcnOLD  24798  iirevcn  24857  iihalf2cn  24862  iihalf2cnOLD  24863  icchmeo  24871  icchmeoOLD  24872  icopnfcnv  24873  icopnfhmeo  24874  evth  24891  pcoass  24957  pjthlem1  25370  ovolunlem1a  25430  ovolunlem1  25431  opnmbllem  25535  mbfi1fseqlem6  25654  bddibl  25774  dvnadd  25864  dvmptid  25894  dvmptdiv  25911  dvcnvlem  25913  dveflem  25916  dvef  25917  dvsincos  25918  dvlipcn  25932  dvivthlem1  25946  lhop2  25953  dvcvx  25958  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem1  25965  dvfsumlem2  25966  dvfsumlem2OLD  25967  itgpowd  25990  ply1divex  26075  fta1glem1  26106  dgrcolem1  26212  dgrcolem2  26213  vieta1lem1  26251  aaliou3lem2  26284  aaliou3lem8  26286  dvtaylp  26311  dvntaylp  26312  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  abelthlem1  26374  abelthlem2  26375  abelthlem6  26379  abelthlem7  26381  logdivlti  26562  advlog  26596  advlogexp  26597  logtayl  26602  cxpmul2  26631  dvcxp1  26682  dvcxp2  26683  dvcncxp1  26685  dvcnsqrt  26686  loglesqrt  26704  relogbdiv  26722  ang180lem4  26755  ang180lem5  26756  isosctrlem2  26762  isosctrlem3  26763  affineequiv  26766  affineequiv2  26767  affineequiv3  26768  angpieqvdlem  26771  chordthmlem2  26776  chordthmlem3  26777  chordthmlem5  26779  dcubic2  26787  dcubic  26789  quart1lem  26798  quart1  26799  quart  26804  asinlem  26811  asinlem3  26814  atansopn  26875  dvatan  26878  leibpi  26885  birthdaylem2  26895  efrlim  26912  efrlimOLD  26913  cxplim  26915  divsqrtsumlem  26923  logdifbnd  26937  emcllem2  26940  emcllem3  26941  emcllem5  26943  zetacvg  26958  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem4  26975  lgamgulmlem5  26976  lgamgulmlem6  26977  lgamgulm2  26979  lgamcvg2  26998  gamcvg  26999  gamcvg2lem  27002  lgam1  27007  gamfac  27010  wilthlem2  27012  wilthimp  27015  ftalem5  27020  basellem3  27026  basellem5  27028  basellem8  27031  basellem9  27032  sqff1o  27125  muinv  27136  logfaclbnd  27166  logfacrlim  27168  logexprlim  27169  perfectlem2  27174  dchr1cl  27195  dchrinvcl  27197  dchrfi  27199  dchr1  27201  dchrsum2  27212  bcmono  27221  bcp1ctr  27223  bclbnd  27224  bposlem9  27236  gausslemma2dlem1a  27309  gausslemma2dlem5  27315  lgseisenlem4  27322  lgsquadlem1  27324  m1lgs  27332  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  2lgslem3d1  27347  2lgsoddprmlem1  27352  2sqlem8  27370  2sq2  27377  addsqn2reu  27385  addsqrexnreu  27386  addsqnreup  27387  addsq2nreurex  27388  chtppilim  27419  rpvmasumlem  27431  dchrisumlem1  27433  dchrisum0re  27457  dchrisum0lem2a  27461  mudivsum  27474  mulogsumlem  27475  mulogsum  27476  2vmadivsumlem  27484  selberg4lem1  27504  pntrsumo1  27509  selberg34r  27515  pntrlog2bndlem2  27522  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntibndlem2  27535  pntlemg  27542  pntlemr  27546  pntlemf  27549  pntlemk  27550  pntlemo  27551  pntlem3  27553  ostth2lem2  27578  ttgcontlem1  28865  cusgrsize2inds  29434  wlklenvclwlk  29634  pthdadjvtx  29708  crctcshwlkn0lem1  29790  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  wlklnwwlkln2lem  29862  wlknwwlksnbij  29868  wwlksnred  29872  wwlksnext  29873  wwlksnextbi  29874  wwlksnredwwlkn  29875  wwlksnextwrd  29877  wwlksnextinj  29879  wwlksnextproplem2  29890  wwlksnextproplem3  29891  clwwlkccatlem  29968  clwlkclwwlklem2a1  29971  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  clwlkclwwlklem2  29979  clwlkclwwlklem3  29980  clwlkclwwlk  29981  clwwisshclwwslemlem  29992  clwwisshclwws  29994  clwwlkel  30025  clwwlkf  30026  clwwlkwwlksb  30033  clwwlkext2edg  30035  wwlksext2clwwlk  30036  clwwlknonex2lem1  30086  clwwlknonex2lem2  30087  eucrct2eupth  30224  numclwwlk1lem2foalem  30330  numclwwlk1lem2fo  30337  numclwlk2lem2f  30356  numclwlk2lem2f1o  30358  numclwwlk6  30369  smcnlem  30676  receqid  32718  fzm1ne1  32761  bcm1n  32768  fzom1ne1  32774  ltesubnnd  32797  sgn0bi  32815  oexpled  32822  wrdt2ind  32925  chnub  32984  chnlt  32985  psgnfzto1stlem  33072  cycpmco2lem3  33100  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cycpmco2lem7  33104  cycpmco2  33105  archirngz  33158  archiabllem1a  33160  archiabllem2c  33164  ccfldextdgrr  33660  constrfin  33729  nn0constr  33744  iconstr  33749  constrrecl  33752  constrimcl  33753  constrreinvcl  33755  constrinvcl  33756  constrresqrtcl  33760  2sqr3minply  33763  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  cos9thpiminplylem3  33767  cos9thpiminply  33771  cos9thpinconstrlem1  33772  1smat1  33787  madjusmdetlem2  33811  madjusmdetlem4  33813  dya2icoseg  34261  iwrdsplit  34371  fibp1  34385  ballotlemfp1  34476  ballotlemfc0  34477  ballotlemfcc  34478  ballotlemic  34491  ballotlem1c  34492  ballotlemsgt1  34495  ballotlemsdom  34496  ballotlemsel1i  34497  ballotlemsi  34499  ballotlemsima  34500  ballotlem1ri  34519  signstfvn  34553  signsvtn0  34554  signstfveq0  34561  signsvfn  34566  signsvtn  34568  signshf  34572  hashreprin  34604  circlemeth  34624  logdivsqrle  34634  revpfxsfxrev  35096  revwlk  35105  swrdwlk  35107  subfacp1lem1  35159  subfacp1lem5  35164  cvxpconn  35222  sinccvglem  35652  divcnvlin  35713  bcm1nt  35717  bcprod  35718  bccolsum  35719  iprodgam  35722  faclimlem1  35723  faclimlem2  35724  faclimlem3  35725  faclim  35726  iprodfac  35727  faclim2  35728  fwddifnp1  36146  dnizphlfeqhlf  36457  dnibndlem3  36461  dnibndlem13  36471  unblimceq0  36488  knoppndvlem6  36498  knoppndvlem9  36501  knoppndvlem14  36506  knoppndvlem15  36507  knoppndvlem16  36508  knoppndvlem17  36509  bj-bary1lem1  37292  irrdiff  37307  poimirlem25  37632  poimirlem26  37633  poimirlem32  37639  opnmbllem0  37643  itg2addnclem2  37659  dvasin  37691  dvacos  37692  areacirclem1  37695  areacirclem4  37698  areacirc  37700  bfp  37811  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  nnadd1com  42248  nnaddcom  42249  nnadddir  42251  nnmul1com  42252  nnmulcom  42253  3rdpwhole  42273  fz1sump1  42291  oddnumth  42292  nicomachus  42293  sumcubes  42294  tan3rdpi  42333  redvmptabs  42341  readvrec  42343  reixi  42404  sn-mullid  42417  sn-0tie0  42432  renegmulnnass  42446  fiabv  42517  fltnltalem  42643  fltnlta  42644  3cubeslem1  42665  3cubeslem2  42666  3cubeslem4  42670  pell1qrge1  42851  rmspecfund  42890  acongeq  42965  jm2.18  42970  jm2.19lem3  42973  jm2.25  42981  jm2.16nn0  42986  jm3.1lem1  42999  jm3.1lem2  43000  areaquad  43198  relexpmulnn  43691  relexpaddss  43700  cvgdvgrat  44295  radcnvrat  44296  hashnzfzclim  44304  ofdivrec  44308  expgrowthi  44315  bccm1k  44324  dvradcnv2  44329  binomcxplemwb  44330  binomcxplemnn0  44331  binomcxplemrat  44332  binomcxplemfrat  44333  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  refsum2cnlem1  45024  fzisoeu  45291  fperiodmullem  45294  fzdifsuc2  45301  xralrple2  45343  nnsplit  45347  infleinflem2  45360  fmul01lt1lem2  45576  fprodcn  45591  clim1fr1  45592  isumneg  45593  climneg  45601  sumnnodd  45621  reclimc  45644  coseq0  45855  coskpi2  45857  cosknegpi  45860  fprodcncf  45891  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnxpaek  45933  dvnmul  45934  dvmptfprod  45936  dvnprodlem3  45939  itgsinexp  45946  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  stoweidlem1  45992  stoweidlem7  45998  stoweidlem10  46001  stoweidlem11  46002  stoweidlem14  46005  stoweidlem17  46008  stoweidlem34  46025  stoweidlem42  46033  wallispilem3  46058  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  wallispi2lem2  46063  wallispi2  46064  stirlinglem1  46065  stirlinglem3  46067  stirlinglem4  46068  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem8  46072  stirlinglem10  46074  stirlinglem11  46075  stirlinglem12  46076  stirlinglem13  46077  stirlinglem15  46079  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkercncflem1  46094  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem11  46109  fourierdlem15  46113  fourierdlem26  46124  fourierdlem36  46134  fourierdlem40  46138  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem56  46153  fourierdlem58  46155  fourierdlem59  46156  fourierdlem62  46159  fourierdlem64  46161  fourierdlem65  46162  fourierdlem78  46175  fourierdlem79  46176  sqwvfoura  46219  fourierswlem  46221  fouriersw  46222  etransclem23  46248  etransclem24  46249  etransclem28  46253  etransclem35  46260  etransclem38  46263  nnfoctbdjlem  46446  smfmullem1  46782  sigaradd  46857  cjnpoly  46883  deccarry  47305  ceilbi  47327  m1modne  47342  m1modmmod  47352  modm1nep2  47362  modm1nem2  47363  fargshiftf1  47435  fargshiftfo  47436  fmtnof1  47529  sqrtpwpw2p  47532  fmtnorec2lem  47536  fmtnorec4  47543  fmtnoprmfac1lem  47558  fmtnoprmfac1  47559  fmtnoprmfac2  47561  2pwp1prm  47583  mod42tp1mod8  47596  sfprmdvdsmersenne  47597  lighneallem3  47601  lighneallem4  47604  onego  47640  zofldiv2ALTV  47656  oexpnegALTV  47671  opoeALTV  47677  opeoALTV  47678  epee  47699  perfectALTVlem1  47715  fppr2odd  47725  fpprwppr  47733  gpg3nbgrvtx0  48060  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  0nodd  48151  2nodd  48153  nnsgrpnmnd  48159  1neven  48219  altgsumbc  48333  pw2m1lepw2m1  48502  zofldiv2  48513  nnpw2pmod  48565  blen1b  48570  blennn0em1  48573  dignn0flhalflem1  48597  dignn0flhalflem2  48598  nn0sumshdiglemB  48602  nn0sumshdiglem1  48603  nn0sumshdiglem2  48604  itcovalpclem2  48653  ackval1  48663  ackval2  48664  ackval3  48665  affineid  48686  1subrec1sub  48687  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  rrx2vlinest  48723