Theorem 1cnd 11107

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11004  1c1 11007

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

This theorem is referenced by:  adddirp1d  11138  1p1times  11284  addcom  11299  addcomd  11315  muladd11r  11326  pncan1  11541  npcan1  11542  muls1d  11577  mulsubfacd  11578  recrec  11818  rec11  11819  rec11r  11820  rereccl  11839  subrecd  11950  nn1m1nn  12146  add1p1  12372  sub1m1  12373  cnm2m1cnm3  12374  xp1d2m1eqxm1d2  12375  div4p1lem1div2  12376  nn0n0n1ge2  12449  zneo  12556  rpnnen1lem5  12879  lincmb01cmp  13395  iccf1o  13396  xov1plusxeqvd  13398  zpnn0elfzo1  13639  ubmelm1fzo  13663  fzosplitpr  13677  fzosplitprm1  13678  fzom1ne1  13685  fzoshftral  13687  fladdz  13729  2tnp1ge0ge0  13733  ltdifltdiv  13738  dfceil2  13743  negmod  13823  modnegd  13833  addmodlteq  13853  binom2sub1  14128  binom3  14131  zesq  14133  sqoddm1div8  14150  bcm1k  14222  bcp1n  14223  bcp1m1  14227  bcpasc  14228  bcn2m1  14231  hashfz  14334  hashfzo  14336  hashfzp1  14338  hashf1lem2  14363  hashf1  14364  hashdifsnp1  14413  lswccatn0lsw  14499  ccatws1lenp1b  14529  revccat  14673  repswrevw  14694  cshwidxm1  14714  cshwidxn  14716  cshweqrep  14728  cshimadifsn0  14737  swrds2m  14848  swrd2lsw  14859  relexpaddnn  14958  absexpz  15212  reccn2  15504  rlimno1  15561  isercolllem1  15572  isercoll2  15576  iseraltlem2  15590  iseraltlem3  15591  fsump1  15663  hashiun  15729  hash2iun1dif1  15731  binomlem  15736  bcxmas  15742  incexc  15744  incexc2  15745  climcndslem1  15756  arisum  15767  arisum2  15768  trireciplem  15769  pwdif  15775  pwm1geoser  15776  geolim2  15778  georeclim  15779  mertenslem1  15791  prodfrec  15802  ntrivcvg  15804  ntrivcvgtail  15807  prodrblem  15836  prodmolem2a  15841  fprodntriv  15849  prod1  15851  fprodser  15856  fprodcl  15859  fprodm1  15874  fprodp1  15876  fprodclf  15899  risefacval2  15917  fallfacval2  15918  risefacp1  15936  fallfacp1  15937  risefacfac  15942  fallfacfwd  15943  binomfallfaclem2  15947  fallfacval4  15950  bpolydiflem  15961  ef0lem  15985  tanaddlem  16075  tanadd  16076  cos01bnd  16095  oddm1even  16254  oddp1even  16255  oexpneg  16256  ltoddhalfle  16272  halfleoddlt  16273  nn0ob  16295  pwp1fsum  16302  flodddiv4  16326  bitsp1o  16344  bitsf1  16357  sadcp1  16366  qredeu  16569  prmdiv  16696  prmdiveq  16697  vfermltlALT  16714  pc2dvds  16791  4sqlem11  16867  4sqlem12  16868  vdwapun  16886  vdwlem3  16895  vdwlem6  16898  vdwlem9  16901  ramub1lem2  16939  prmop1  16950  prmdvdsprmo  16954  prmgaplem8  16970  cshwshashnsame  17015  chnub  18528  chnlt  18529  chnccat  18532  chnrev  18533  gsumsgrpccat  18748  psgnunilem5  19406  psgnunilem2  19407  sylow1lem1  19510  efgredlemc  19657  odadd2  19761  ablsimpgfindlem1  20021  omndmul2  20045  srgbinomlem3  20146  srgbinomlem4  20147  cncrng  21325  cncrngOLD  21326  gzrngunit  21370  zringunit  21403  prmirredlem  21409  pzriprnglem12  21429  freshmansdream  21511  mhppwdeg  22065  psdmul  22081  cayhamlem1  22781  expcn  24790  expcnOLD  24792  iirevcn  24851  iihalf2cn  24856  iihalf2cnOLD  24857  icchmeo  24865  icchmeoOLD  24866  icopnfcnv  24867  icopnfhmeo  24868  evth  24885  pcoass  24951  pjthlem1  25364  ovolunlem1a  25424  ovolunlem1  25425  opnmbllem  25529  mbfi1fseqlem6  25648  bddibl  25768  dvnadd  25858  dvmptid  25888  dvmptdiv  25905  dvcnvlem  25907  dveflem  25910  dvef  25911  dvsincos  25912  dvlipcn  25926  dvivthlem1  25940  lhop2  25947  dvcvx  25952  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  itgpowd  25984  ply1divex  26069  fta1glem1  26100  dgrcolem1  26206  dgrcolem2  26207  vieta1lem1  26245  aaliou3lem2  26278  aaliou3lem8  26280  dvtaylp  26305  dvntaylp  26306  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  abelthlem1  26368  abelthlem2  26369  abelthlem6  26373  abelthlem7  26375  logdivlti  26556  advlog  26590  advlogexp  26591  logtayl  26596  cxpmul2  26625  dvcxp1  26676  dvcxp2  26677  dvcncxp1  26679  dvcnsqrt  26680  loglesqrt  26698  relogbdiv  26716  ang180lem4  26749  ang180lem5  26750  isosctrlem2  26756  isosctrlem3  26757  affineequiv  26760  affineequiv2  26761  affineequiv3  26762  angpieqvdlem  26765  chordthmlem2  26770  chordthmlem3  26771  chordthmlem5  26773  dcubic2  26781  dcubic  26783  quart1lem  26792  quart1  26793  quart  26798  asinlem  26805  asinlem3  26808  atansopn  26869  dvatan  26872  leibpi  26879  birthdaylem2  26889  efrlim  26906  efrlimOLD  26907  cxplim  26909  divsqrtsumlem  26917  logdifbnd  26931  emcllem2  26934  emcllem3  26935  emcllem5  26937  zetacvg  26952  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem4  26969  lgamgulmlem5  26970  lgamgulmlem6  26971  lgamgulm2  26973  lgamcvg2  26992  gamcvg  26993  gamcvg2lem  26996  lgam1  27001  gamfac  27004  wilthlem2  27006  wilthimp  27009  ftalem5  27014  basellem3  27020  basellem5  27022  basellem8  27025  basellem9  27026  sqff1o  27119  muinv  27130  logfaclbnd  27160  logfacrlim  27162  logexprlim  27163  perfectlem2  27168  dchr1cl  27189  dchrinvcl  27191  dchrfi  27193  dchr1  27195  dchrsum2  27206  bcmono  27215  bcp1ctr  27217  bclbnd  27218  bposlem9  27230  gausslemma2dlem1a  27303  gausslemma2dlem5  27309  lgseisenlem4  27316  lgsquadlem1  27318  m1lgs  27326  2lgslem3a  27334  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  2lgslem3d1  27341  2lgsoddprmlem1  27346  2sqlem8  27364  2sq2  27371  addsqn2reu  27379  addsqrexnreu  27380  addsqnreup  27381  addsq2nreurex  27382  chtppilim  27413  rpvmasumlem  27425  dchrisumlem1  27427  dchrisum0re  27451  dchrisum0lem2a  27455  mudivsum  27468  mulogsumlem  27469  mulogsum  27470  2vmadivsumlem  27478  selberg4lem1  27498  pntrsumo1  27503  selberg34r  27509  pntrlog2bndlem2  27516  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntibndlem2  27529  pntlemg  27536  pntlemr  27540  pntlemf  27543  pntlemk  27544  pntlemo  27545  pntlem3  27547  ostth2lem2  27572  ttgcontlem1  28863  cusgrsize2inds  29432  wlklenvclwlk  29632  pthdadjvtx  29706  crctcshwlkn0lem1  29788  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  wlklnwwlkln2lem  29860  wlknwwlksnbij  29866  wwlksnred  29870  wwlksnext  29871  wwlksnextbi  29872  wwlksnredwwlkn  29873  wwlksnextwrd  29875  wwlksnextinj  29877  wwlksnextproplem2  29888  wwlksnextproplem3  29889  clwwlkccatlem  29969  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  clwlkclwwlklem3  29981  clwlkclwwlk  29982  clwwisshclwwslemlem  29993  clwwisshclwws  29995  clwwlkel  30026  clwwlkf  30027  clwwlkwwlksb  30034  clwwlkext2edg  30036  wwlksext2clwwlk  30037  clwwlknonex2lem1  30087  clwwlknonex2lem2  30088  eucrct2eupth  30225  numclwwlk1lem2foalem  30331  numclwwlk1lem2fo  30338  numclwlk2lem2f  30357  numclwlk2lem2f1o  30359  numclwwlk6  30370  smcnlem  30677  receqid  32728  fzm1ne1  32771  bcm1n  32777  ltesubnnd  32805  sgn0bi  32823  oexpled  32830  wrdt2ind  32934  psgnfzto1stlem  33069  cycpmco2lem3  33097  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2lem7  33101  cycpmco2  33102  archirngz  33158  archiabllem1a  33160  archiabllem2c  33164  gsumind  33310  ccfldextdgrr  33685  constrfin  33759  nn0constr  33774  iconstr  33779  constrrecl  33782  constrimcl  33783  constrreinvcl  33785  constrinvcl  33786  constrresqrtcl  33790  2sqr3minply  33793  cos9thpiminplylem1  33795  cos9thpiminplylem2  33796  cos9thpiminplylem3  33797  cos9thpiminply  33801  cos9thpinconstrlem1  33802  1smat1  33817  madjusmdetlem2  33841  madjusmdetlem4  33843  dya2icoseg  34290  iwrdsplit  34400  fibp1  34414  ballotlemfp1  34505  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemic  34520  ballotlem1c  34521  ballotlemsgt1  34524  ballotlemsdom  34525  ballotlemsel1i  34526  ballotlemsi  34528  ballotlemsima  34529  ballotlem1ri  34548  signstfvn  34582  signsvtn0  34583  signstfveq0  34590  signsvfn  34595  signsvtn  34597  signshf  34601  hashreprin  34633  circlemeth  34653  logdivsqrle  34663  revpfxsfxrev  35160  revwlk  35169  swrdwlk  35171  subfacp1lem1  35223  subfacp1lem5  35228  cvxpconn  35286  sinccvglem  35716  divcnvlin  35777  bcm1nt  35781  bcprod  35782  bccolsum  35783  iprodgam  35786  faclimlem1  35787  faclimlem2  35788  faclimlem3  35789  faclim  35790  iprodfac  35791  faclim2  35792  fwddifnp1  36209  dnizphlfeqhlf  36520  dnibndlem3  36524  dnibndlem13  36534  unblimceq0  36551  knoppndvlem6  36561  knoppndvlem9  36564  knoppndvlem14  36569  knoppndvlem15  36570  knoppndvlem16  36571  knoppndvlem17  36572  bj-bary1lem1  37355  irrdiff  37370  poimirlem25  37695  poimirlem26  37696  poimirlem32  37702  opnmbllem0  37706  itg2addnclem2  37722  dvasin  37754  dvacos  37755  areacirclem1  37758  areacirclem4  37761  areacirc  37763  bfp  37874  fzsplitnd  42085  lcmfunnnd  42115  lcmineqlem1  42132  lcmineqlem3  42134  lcmineqlem4  42135  lcmineqlem7  42138  lcmineqlem8  42139  lcmineqlem10  42141  lcmineqlem11  42142  lcmineqlem12  42143  lcmineqlem18  42149  lcmineqlem19  42150  lcmineqlem22  42153  lcmineqlem23  42154  dvrelogpow2b  42171  aks4d1p1p4  42174  aks4d1p1p6  42176  aks4d1p1p7  42177  aks4d1p1p5  42178  aks4d1p1  42179  aks4d1p3  42181  aks4d1p7d1  42185  primrootsunit1  42200  posbezout  42203  primrootscoprbij  42205  primrootspoweq0  42209  aks6d1c1  42219  hashscontpow1  42224  2np3bcnp1  42247  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  sticksstones16  42265  sticksstones22  42271  aks6d1c6lem3  42275  aks6d1c7lem1  42283  unitscyglem5  42302  nnadd1com  42370  nnaddcom  42371  nnadddir  42373  nnmul1com  42374  nnmulcom  42375  3rdpwhole  42395  fz1sump1  42413  oddnumth  42414  nicomachus  42415  sumcubes  42416  tan3rdpi  42455  redvmptabs  42463  readvrec  42465  reixi  42526  sn-mullid  42539  sn-0tie0  42554  renegmulnnass  42568  fiabv  42639  fltnltalem  42765  fltnlta  42766  3cubeslem1  42787  3cubeslem2  42788  3cubeslem4  42792  pell1qrge1  42973  rmspecfund  43012  acongeq  43086  jm2.18  43091  jm2.19lem3  43094  jm2.25  43102  jm2.16nn0  43107  jm3.1lem1  43120  jm3.1lem2  43121  areaquad  43319  relexpmulnn  43812  relexpaddss  43821  cvgdvgrat  44416  radcnvrat  44417  hashnzfzclim  44425  ofdivrec  44429  expgrowthi  44436  bccm1k  44445  dvradcnv2  44450  binomcxplemwb  44451  binomcxplemnn0  44452  binomcxplemrat  44453  binomcxplemfrat  44454  binomcxplemdvbinom  44456  binomcxplemnotnn0  44459  refsum2cnlem1  45144  fzisoeu  45411  fperiodmullem  45414  fzdifsuc2  45421  xralrple2  45463  nnsplit  45467  infleinflem2  45479  fmul01lt1lem2  45695  fprodcn  45710  clim1fr1  45711  isumneg  45712  climneg  45720  sumnnodd  45740  reclimc  45761  coseq0  45972  coskpi2  45974  cosknegpi  45977  fprodcncf  46008  fprodsubrecnncnvlem  46015  fprodaddrecnncnvlem  46017  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnxpaek  46050  dvnmul  46051  dvmptfprod  46053  dvnprodlem3  46056  itgsinexp  46063  itgiccshift  46088  itgperiod  46089  itgsbtaddcnst  46090  stoweidlem1  46109  stoweidlem7  46115  stoweidlem10  46118  stoweidlem11  46119  stoweidlem14  46122  stoweidlem17  46125  stoweidlem34  46142  stoweidlem42  46150  wallispilem3  46175  wallispilem5  46177  wallispi  46178  wallispi2lem1  46179  wallispi2lem2  46180  wallispi2  46181  stirlinglem1  46182  stirlinglem3  46184  stirlinglem4  46185  stirlinglem5  46186  stirlinglem6  46187  stirlinglem7  46188  stirlinglem8  46189  stirlinglem10  46191  stirlinglem11  46192  stirlinglem12  46193  stirlinglem13  46194  stirlinglem15  46196  dirkertrigeqlem2  46207  dirkertrigeqlem3  46208  dirkertrigeq  46209  dirkercncflem1  46211  dirkercncflem2  46212  dirkercncflem4  46214  fourierdlem11  46226  fourierdlem15  46230  fourierdlem26  46241  fourierdlem36  46251  fourierdlem40  46255  fourierdlem41  46256  fourierdlem42  46257  fourierdlem48  46262  fourierdlem49  46263  fourierdlem56  46270  fourierdlem58  46272  fourierdlem59  46273  fourierdlem62  46276  fourierdlem64  46278  fourierdlem65  46279  fourierdlem78  46292  fourierdlem79  46293  sqwvfoura  46336  fourierswlem  46338  fouriersw  46339  etransclem23  46365  etransclem24  46366  etransclem28  46370  etransclem35  46377  etransclem38  46380  nnfoctbdjlem  46563  smfmullem1  46899  sigaradd  46974  chnerlem2  46991  cjnpoly  46999  deccarry  47421  ceilbi  47443  m1modne  47458  m1modmmod  47468  modm1nep2  47478  modm1nem2  47479  fargshiftf1  47551  fargshiftfo  47552  fmtnof1  47645  sqrtpwpw2p  47648  fmtnorec2lem  47652  fmtnorec4  47659  fmtnoprmfac1lem  47674  fmtnoprmfac1  47675  fmtnoprmfac2  47677  2pwp1prm  47699  mod42tp1mod8  47712  sfprmdvdsmersenne  47713  lighneallem3  47717  lighneallem4  47720  onego  47756  zofldiv2ALTV  47772  oexpnegALTV  47787  opoeALTV  47793  opeoALTV  47794  epee  47815  perfectALTVlem1  47831  fppr2odd  47841  fpprwppr  47849  gpg3nbgrvtx0  48186  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  0nodd  48280  2nodd  48282  nnsgrpnmnd  48288  1neven  48348  altgsumbc  48462  pw2m1lepw2m1  48631  zofldiv2  48642  nnpw2pmod  48694  blen1b  48699  blennn0em1  48702  dignn0flhalflem1  48726  dignn0flhalflem2  48727  nn0sumshdiglemB  48731  nn0sumshdiglem1  48732  nn0sumshdiglem2  48733  itcovalpclem2  48782  ackval1  48792  ackval2  48793  ackval3  48794  affineid  48815  1subrec1sub  48816  eenglngeehlnmlem1  48848  eenglngeehlnmlem2  48849  rrx2vlinest  48852