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

Theorem 1z 10267
Description: One is an integer. (Contributed by NM, 10-May-2004.)
Assertion
Ref Expression
1z  |-  1  e.  ZZ

Proof of Theorem 1z
StepHypRef Expression
1 1nn 9967 . 2  |-  1  e.  NN
21nnzi 10261 1  |-  1  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   1c1 8947   ZZcz 10238
This theorem is referenced by:  peano2z  10274  peano2zm  10276  peano5uzti  10315  nnuz  10477  eluz2b1  10503  uz2m1nn  10506  nninfm  10512  nnrecq  10553  qbtwnxr  10742  fz1n  11029  fz10  11031  fz01en  11035  fzprval  11062  fztpval  11063  4fvwrd4  11076  fseq1p1m1  11077  elfzm1b  11080  fzm1  11082  fzoss2  11118  fzo12sn  11138  fzofzp1  11144  elfznelfzo  11147  fzostep1  11152  injresinj  11155  flge1nn  11181  modnegd  11236  fzennn  11262  fzen2  11263  sermono  11310  seqf1olem2  11318  ser1const  11334  exp1  11342  zexpcl  11351  qexpcl  11352  qexpclz  11357  m1expcl  11359  expp1z  11383  expm1  11384  facnn  11523  fac0  11524  fac1  11525  bcn1  11559  bcp1nk  11563  bcpasc  11567  hashsng  11602  hashfz  11647  fz1isolem  11665  seqcoll  11667  s2f1o  11818  f1oun2prg  11819  climuni  12301  isercoll  12416  isercoll2  12417  iseraltlem1  12430  sum0  12470  sumsn  12489  fsumtscopo  12536  fsumparts  12540  binomlem  12563  climcndslem1  12584  climcndslem2  12585  climcnds  12586  divcnv  12588  supcvg  12590  arisum  12594  trireciplem  12596  trirecip  12597  expcnv  12598  geo2sum  12605  geo2lim  12607  geoisum1  12611  geoisum1c  12612  mertenslem1  12616  mertenslem2  12617  ege2le3  12647  sin01gt0  12746  rpnnen2lem10  12778  rpnnen2  12780  nthruc  12805  iddvds  12818  1dvds  12819  dvdsle  12850  dvds1  12853  3dvds  12867  divalglem5  12872  divalg  12878  bitsfzolem  12901  bitsfzo  12902  bitscmp  12905  gcdcllem1  12966  gcdcllem3  12968  gcdaddmlem  12983  gcdadd  12985  gcdid  12986  gcd1  12987  1gcd  12992  bezoutlem1  12993  gcdmultiple  13005  isprm3  13043  phicl2  13112  phi1  13117  dfphi2  13118  hashdvds  13119  phiprmpw  13120  eulerthlem2  13126  prmdiv  13129  prmdiveq  13130  odzcllem  13133  odzdvds  13136  odzphi  13137  oddprm  13144  pythagtriplem4  13148  iserodd  13164  pcpre1  13171  pc1  13184  pcrec  13187  pcid  13201  pcmptcl  13215  pcmpt  13216  fldivp1  13221  expnprm  13226  pockthlem  13228  unbenlem  13231  prmreclem2  13240  prmreclem4  13242  prmreclem6  13244  prmrec  13245  igz  13257  4sqlem12  13279  4sqlem13  13280  4sqlem19  13286  vdwapun  13297  vdwlem8  13311  vdwlem13  13316  prmlem0  13383  1259lem4  13408  2503lem2  13412  4001lem1  13415  mulg1  14852  mulgm1  14864  mulgp1  14871  mulgneg2  14872  mulgpropd  14878  cycsubgcl  14921  odinv  15152  sylow1lem1  15187  sylow3lem6  15221  efgs1b  15323  lt6abl  15459  pgpfac1lem2  15588  qsubdrg  16706  zsubrg  16707  gzsubrg  16708  zcyg  16727  mulgrhm  16742  mulgrhm2  16743  chrnzr  16766  znunit  16799  znrrg  16801  frgpcyg  16809  lmcnp  17322  lmmo  17398  1stcelcls  17477  1stccnp  17478  1stckgenlem  17538  1stckgen  17539  zfbas  17881  imasdsf1olem  18356  clmvneg1  19069  clmmulg  19071  lmnn  19169  cmetcaulem  19194  iscmet2  19200  causs  19204  caubl  19213  iscmet3i  19217  bcthlem5  19234  ovolsf  19322  ovolctb  19339  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliun  19354  ovoliun2  19355  ovoliunnul  19356  ovolicc1  19365  ovolicc2lem2  19367  ovolicc2lem3  19368  ovolicc2lem4  19369  voliunlem1  19397  voliunlem2  19398  voliunlem3  19399  volsup  19403  ioombl1lem4  19408  uniioombllem2  19428  uniioombllem3  19430  uniioombllem6  19433  vitalilem4  19456  vitalilem5  19457  itg1climres  19559  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfmullem2  19569  itg2monolem1  19595  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  plyeq0lem  20082  dvply1  20154  vieta1lem2  20181  elqaalem2  20190  qaa  20193  iaa  20195  dvtaylp  20239  dvradcnv  20290  pserdvlem2  20297  pserdv2  20299  abelthlem6  20305  abelthlem9  20309  sin2pim  20346  cos2pim  20347  efif1olem2  20398  advlogexp  20499  logtayl  20504  logtaylsum  20505  logtayl2  20506  ang180lem3  20606  1cubrlem  20634  atantayl  20730  leibpilem2  20734  leibpi  20735  birthdaylem2  20744  dfef2  20762  divsqrsumlem  20771  emcllem4  20790  emcllem5  20791  emcllem6  20792  emcllem7  20793  wilthlem1  20804  wilthlem2  20805  wilthlem3  20806  basellem6  20821  basellem7  20822  basellem8  20823  basellem9  20824  muf  20876  ppip1le  20897  ppi1  20900  cht1  20901  chp1  20903  cht2  20908  ppieq0  20912  ppiub  20941  chpeq0  20945  chpchtsum  20956  chpub  20957  logfacbnd3  20960  logexprlim  20962  mersenne  20964  perfectlem1  20966  perfectlem2  20967  bposlem1  21021  bposlem2  21022  bposlem5  21025  bposlem6  21026  lgslem1  21033  lgslem2  21034  lgsfcl2  21039  lgsval2lem  21043  lgsdir2lem1  21060  lgsdir2lem3  21062  lgsdir2lem4  21063  lgsdir2lem5  21064  lgsqrlem1  21078  lgsdchr  21085  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem4  21089  lgsquad2lem1  21095  lgsquad3  21098  m1lgs  21099  2sqlem9  21110  2sqlem10  21111  2sqlem11  21112  2sqblem  21114  2sqb  21115  dchrisumlema  21135  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasumiflem1  21148  dchrvmaeq0  21151  dchrisum0re  21160  dchrisum0lem1b  21162  dchrisum0lem2a  21164  logdivsum  21180  log2sumbnd  21191  pntrlog2bndlem1  21224  pntpbnd2  21234  qabvle  21272  ostth3  21285  usgraexmpldifpr  21372  usgraexmpl  21373  2trllemD  21510  2trllemG  21511  0pth  21523  constr1trl  21541  constr2spthlem1  21547  redwlk  21559  fargshiftlem  21574  usgrcyclnl1  21580  usgrcyclnl2  21581  3v3e3cycl1  21584  constr3lem4  21587  constr3trllem3  21592  constr3trllem5  21594  constr3pthlem1  21595  constr3pthlem2  21596  constr3pthlem3  21597  4cycl4v4e  21606  4cycl4dv4e  21608  eupap1  21651  eupath2lem3  21654  ex-fl  21708  gx1  21803  gxm1  21809  nvlmle  22141  ipval2  22156  minvecolem3  22331  minvecolem4b  22333  minvecolem4  22335  h2hcau  22435  h2hlm  22436  hlimadd  22648  hlim0  22691  hhsscms  22732  occllem  22758  nlelchi  23517  opsqrlem2  23597  opsqrlem4  23599  hmopidmchi  23607  iuninc  23964  fzspl  24102  fzsplit3  24103  gsumpropd2lem  24173  zzsmulg  24218  lmlim  24286  rge0scvg  24288  lmxrge0  24290  lmdvg  24291  qqhval2lem  24318  qqh0  24321  qqh1  24322  rnlogblem  24352  logblt  24359  esumfzf  24412  esumfsup  24413  esumfsupre  24414  esumpcvgval  24421  esumcvg  24429  dya2ub  24573  rrvsum  24665  dstfrvclim1  24688  ballotlem2  24699  ballotlemfp1  24702  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemimin  24716  ballotlemic  24717  ballotlem1c  24718  ballotlemsdom  24722  ballotlemsel1i  24723  ballotlemsima  24726  ballotlemfrceq  24739  ballotlemfrcn0  24740  zetacvg  24752  lgamgulmlem4  24769  lgamgulmlem6  24771  lgamgulm2  24773  lgamcvglem  24777  lgamcvg2  24792  gamcvg  24793  gamcvg2lem  24796  regamcl  24798  relgamcl  24799  lgam1  24801  subfac1  24817  subfacp1lem1  24818  subfacp1lem2a  24819  subfacp1lem5  24823  subfacp1lem6  24824  cvmliftlem10  24934  sinccvg  25063  circum  25064  elfzp1b  25069  fznatpl1  25151  bcnm1  25154  divcnvshft  25164  divcnvlin  25165  prod0  25222  fprodser  25228  fprodzcl  25233  prodsn  25239  iprodgam  25272  risefacval2  25279  fallfacval2  25280  zrisefaccl  25288  zfallfaccl  25289  risefall0lem  25294  binomfallfaclem2  25307  faclimlem1  25310  faclimlem2  25311  faclim  25313  iprodfac  25314  faclim2  25315  axlowdimlem3  25787  axlowdimlem4  25788  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  bpolydiflem  26004  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  fdc  26339  lmclim2  26354  geomcau  26355  heibor1lem  26408  heibor1  26409  bfplem1  26421  bfplem2  26422  rrncmslem  26431  rrncms  26432  mapfzcons  26662  mzpexpmpt  26692  fzsplit1nn0  26702  eldioph2lem1  26708  eldioph3b  26713  fz1eqin  26717  diophin  26721  diophun  26722  0dioph  26727  elnnrabdioph  26757  rabren3dioph  26766  irrapxlem1  26775  irrapxlem3  26777  pellexlem6  26787  rmspecnonsq  26860  rmxyadd  26874  rmxy1  26875  rmxy0  26876  rmxp1  26885  rmyp1  26886  rmxm1  26887  rmym1  26888  jm2.24nn  26914  acongeq  26938  jm2.22  26956  jm2.23  26957  jm2.25  26960  jm2.15nn0  26964  jm2.16nn0  26965  jm2.27c  26968  jm2.27dlem2  26971  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  mpaaeu  27223  sumsnd  27564  fmuldfeq  27580  fmul01lt1lem2  27582  fmul01lt1  27583  clim1fr1  27594  stoweidlem3  27619  stoweidlem7  27623  stoweidlem11  27627  stoweidlem14  27630  stoweidlem20  27636  stoweidlem26  27642  stoweidlem34  27650  stoweidlem51  27667  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem1  27690  stirlinglem5  27694  stirlinglem7  27696  stirlinglem8  27697  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  stirlingr  27706  f13idfv  27963  ubmelm1fzo  27987  fzo1fzo0n0  27988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-z 10239
  Copyright terms: Public domain W3C validator