MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1cnd Unicode version

Theorem 1cnd 9633
Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1cnd

Proof of Theorem 1cnd
StepHypRef Expression
1 ax-1cn 9571 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511  1c1 9514
This theorem is referenced by:  1p1times  9772  addcom  9787  addcomd  9803  pncan1  10008  npcan1  10009  mulsubfacd  10041  recrec  10266  rec11  10267  rec11r  10268  rereccl  10287  subrec  10398  nn1m1nn  10581  add1p1  10813  sub1m1  10814  cnm2m1cnm3  10815  nn0n0n1ge2  10884  zneo  10970  rpnnen1lem5  11241  lincmb01cmp  11692  iccf1o  11693  xov1plusxeqvd  11695  zpnn0elfzo1  11889  ubmelm1fzo  11908  fzoshftral  11923  fladdz  11958  ltdifltdiv  11966  dfceil2  11968  modvalp1  12014  modnegd  12042  binom3  12287  zesq  12289  bcm1k  12393  bcp1n  12394  bcp1m1  12398  bcpasc  12399  bcn2m1  12402  hashfz  12485  hashfzo  12487  hashf1lem2  12505  hashf1  12506  brfi1indlem  12531  lswccatn0lsw  12607  wrdlenccats1lenm1  12627  ccatw2s1p2  12641  swrdccatwrd  12693  revccat  12740  repswrevw  12758  cshwidxm1  12777  cshwidxn  12779  cshweqrep  12789  swrd2lsw  12890  absexpz  13138  reccn2  13419  rlimno1  13476  isercolllem1  13487  isercoll2  13491  iseraltlem2  13505  iseraltlem3  13506  hashiun  13636  binomlem  13641  bcxmas  13647  incexc  13649  incexc2  13650  climcndslem1  13661  arisum  13671  trireciplem  13673  geolim2  13680  georeclim  13681  mertenslem1  13693  prodfrec  13704  ntrivcvg  13706  ntrivcvgtail  13709  prodrblem  13736  prodmolem2a  13741  fprodntriv  13749  prod1  13751  fprodser  13756  fprodcl  13759  fprodm1  13771  fprodp1  13773  ef0lem  13814  tanaddlem  13901  tanadd  13902  cos01bnd  13921  oddm1even  14047  oddp1even  14048  oexpneg  14049  bitsp1o  14083  bitsf1  14096  sadcp1  14105  qredeu  14248  prmdiv  14315  prmdiveq  14316  pcexp  14383  pc2dvds  14402  4sqlem11  14473  4sqlem12  14474  vdwapun  14492  vdwlem3  14501  vdwlem6  14504  vdwlem9  14507  ramub1lem2  14545  cshwshashnsame  14588  gsumccat  16009  mulgnnass  16170  psgnunilem5  16519  psgnunilem2  16520  sylow1lem1  16618  efgredlemc  16763  odadd2  16855  srgbinomlem3  17193  srgbinomlem4  17194  cncrng  18439  cnfldmulg  18450  gzrngunit  18483  zringunit  18520  zrngunit  18521  prmirredlem  18523  cayhamlem1  19367  expcn  21376  iirevcn  21430  iihalf2cn  21434  icchmeo  21441  icopnfcnv  21442  icopnfhmeo  21443  evth  21459  pjthlem1  21852  ovolunlem1a  21907  ovolunlem1  21908  opnmbllem  22010  mbfi1fseqlem6  22127  bddibl  22246  dvnadd  22332  dvmptid  22360  dvcnvlem  22377  dveflem  22380  dvsincos  22382  dvlipcn  22395  dvivthlem1  22409  lhop2  22416  dvcvx  22421  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem2  22428  ply1divex  22537  fta1glem1  22566  dgrcolem1  22670  dgrcolem2  22671  aaliou3lem2  22739  aaliou3lem8  22741  dvtaylp  22765  dvntaylp  22766  taylthlem1  22768  taylthlem2  22769  abelthlem1  22826  abelthlem2  22827  abelthlem6  22831  abelthlem7  22833  logdivlti  23005  advlog  23035  advlogexp  23036  logtayl  23041  cxpmul2  23070  dvcxp1  23116  dvcxp2  23117  loglesqrt  23132  ang180lem4  23144  ang180lem5  23145  isosctrlem2  23153  isosctrlem3  23154  affineequiv  23157  affineequiv2  23158  angpieqvdlem  23159  chordthmlem2  23164  chordthmlem3  23165  chordthmlem5  23167  dcubic2  23175  dcubic  23177  quart1lem  23186  quart1  23187  quart  23192  asinlem  23199  asinlem3  23202  atansopn  23263  dvatan  23266  leibpi  23273  birthdaylem2  23282  efrlim  23299  cxplim  23301  divsqrtsumlem  23309  logdifbnd  23323  emcllem2  23326  emcllem3  23327  emcllem5  23329  ftalem5  23350  basellem3  23356  basellem5  23358  basellem8  23361  basellem9  23362  sqff1o  23456  muinv  23469  logfaclbnd  23497  logfacrlim  23499  logexprlim  23500  dchr1cl  23526  dchrinvcl  23528  dchrfi  23530  dchr1  23532  dchrsum2  23543  bcmono  23552  bcp1ctr  23554  bclbnd  23555  bposlem1  23559  bposlem9  23567  lgseisenlem4  23627  lgsquadlem1  23629  m1lgs  23637  2sqlem8  23647  chtppilim  23660  rpvmasumlem  23672  dchrisumlem1  23674  dchrisum0re  23698  dchrisum0lem2a  23702  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  2vmadivsumlem  23725  selberg4lem1  23745  pntrsumo1  23750  selberg34r  23756  pntrlog2bndlem2  23763  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntibndlem2  23776  pntlemg  23783  pntlemr  23787  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntlem3  23794  ostth2lem2  23819  ttgcontlem1  24188  cusgrasizeinds  24476  cusgrasize2inds  24477  wlkdvspthlem  24609  fargshiftf1  24637  fargshiftfo  24638  wwlknimp  24687  wlklniswwlkn2  24700  wwlknred  24723  wwlknextbi  24725  wwlknredwwlkn  24726  wwlkextwrd  24728  wwlkextinj  24730  wwlkextproplem2  24742  wwlkextproplem3  24743  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwlkisclwwlklem0  24788  clwlkisclwwlk  24789  clwwlkel  24793  clwwlkf  24794  clwwlkext2edg  24802  clwwisshclwwlem1  24805  clwwisshclww  24807  wlklenvclwlk  24839  nbhashuvtx1  24915  rusgra0edg  24955  eupatrl  24968  frghash2spot  25063  frgregordn0  25070  extwwlkfablem1  25074  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwlk1lem2foa  25091  numclwlk1lem2fo  25095  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  smcnlem  25607  bcm1n  27600  ltesubnnd  27612  omndmul2  27702  archirngz  27733  archiabllem1a  27735  archiabllem2c  27739  dya2icoseg  28248  iwrdsplit  28326  fibp1  28340  ballotlemfp1  28430  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemic  28445  ballotlem1c  28446  ballotlemsgt1  28449  ballotlemsdom  28450  ballotlemsel1i  28451  ballotlemsi  28453  ballotlemsima  28454  ballotlem1ri  28473  sgn0bi  28486  signstfvn  28526  signsvtn0  28527  signstfveq0  28534  signsvfn  28539  signsvtn  28541  signshf  28545  zetacvg  28557  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamgulm2  28578  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  lgam1  28606  gamfac  28609  subfacp1lem1  28623  subfacp1lem5  28628  cvxpcon  28687  sinccvglem  29038  relexpadd  29061  divcnvlin  29118  muls1d  29119  iprodgam  29125  risefacval2  29132  fallfacval2  29133  risefacp1  29151  fallfacp1  29152  risefacfac  29157  fallfacfwd  29158  binomfallfaclem2  29162  fallfacval4  29165  faclimlem1  29168  faclimlem2  29169  faclimlem3  29170  faclim  29171  iprodfac  29172  faclim2  29173  bpolydiflem  29816  opnmbllem0  30050  itg2addnclem2  30067  dvcncxp1  30100  dvcnsqrt  30101  dvasin  30103  dvacos  30104  areacirclem1  30107  areacirclem4  30110  areacirc  30112  bfp  30320  pell1qrge1  30806  rmspecfund  30845  acongeq  30921  jm2.18  30930  jm2.19lem3  30933  jm2.25  30941  jm2.16nn0  30946  jm3.1lem1  30959  jm3.1lem2  30960  itgpowd  31182  areaquad  31184  cvgdvgrat  31194  radcnvrat  31195  hashnzfzclim  31227  ofdivrec  31231  expgrowthi  31238  bccm1k  31247  dvradcnv2  31252  binomcxplemwb  31253  binomcxplemnn0  31254  binomcxplemrat  31255  binomcxplemfrat  31256  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  refsum2cnlem1  31412  adddirp1d  31486  fzisoeu  31500  fperiodmullem  31503  fzdifsuc2  31512  fmul01lt1lem2  31579  m1expeven  31585  clim1fr1  31607  isumneg  31608  climneg  31616  sumnnodd  31636  reclimc  31659  coseq0  31664  coskpi2  31666  cosknegpi  31669  fprodcncf  31704  dvmptdiv  31714  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnxpaek  31739  dvnmul  31740  dvmptfprod  31742  dvnprodlem3  31745  itgsinexp  31753  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem1  31783  stoweidlem7  31789  stoweidlem10  31792  stoweidlem11  31793  stoweidlem14  31796  stoweidlem17  31799  stoweidlem34  31816  stoweidlem42  31824  wallispilem3  31849  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  stirlinglem4  31859  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem8  31863  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem15  31870  dirkertrigeqlem2  31881  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem11  31900  fourierdlem15  31904  fourierdlem26  31915  fourierdlem36  31925  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem48  31937  fourierdlem49  31938  fourierdlem56  31945  fourierdlem58  31947  fourierdlem59  31948  fourierdlem62  31951  fourierdlem64  31953  fourierdlem65  31954  fourierdlem78  31967  fourierdlem79  31968  sqwvfoura  32011  fourierswlem  32013  fouriersw  32014  etransclem23  32040  etransclem24  32041  etransclem28  32045  etransclem35  32052  etransclem38  32055  sigaradd  32083  fzosplitpr  32342  0nodd  32498  2nodd  32500  nnsgrpnmnd  32506  1neven  32738  altgsumbc  32941  bj-bary1lem1  34680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9571
  Copyright terms: Public domain W3C validator