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

Theorem 1z 10055
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 9759 . 2  |-  1  e.  NN
21nnzi 10049 1  |-  1  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1686   1c1 8740   ZZcz 10026
This theorem is referenced by:  peano2z  10062  peano2zm  10064  peano5uzti  10103  nnuz  10265  eluz2b1  10291  uz2m1nn  10294  nninfm  10300  nnrecq  10341  qbtwnxr  10529  fz1n  10814  fz10  10816  fz01en  10820  fzprval  10846  fztpval  10847  fseq1p1m1  10859  elfzm1b  10862  fzm1  10864  fzoss2  10899  fzofzp1  10918  fzostep1  10924  flge1nn  10951  modnegd  11006  fzennn  11032  fzen2  11033  sermono  11080  seqf1olem2  11088  ser1const  11104  exp1  11111  zexpcl  11120  qexpcl  11121  qexpclz  11126  m1expcl  11128  expp1z  11152  expm1  11153  facnn  11292  fac0  11293  fac1  11294  bcn1  11327  bcp1nk  11331  bcpasc  11335  hashsng  11358  hashfz  11383  fz1isolem  11401  seqcoll  11403  climuni  12028  isercoll  12143  isercoll2  12144  iseraltlem1  12156  sum0  12196  sumsn  12215  fsumtscopo  12262  fsumparts  12266  binomlem  12289  climcndslem1  12310  climcndslem2  12311  climcnds  12312  divcnv  12314  supcvg  12316  arisum  12320  trireciplem  12322  trirecip  12323  expcnv  12324  geo2sum  12331  geo2lim  12333  geoisum1  12337  geoisum1c  12338  mertenslem1  12342  mertenslem2  12343  ege2le3  12373  sin01gt0  12472  rpnnen2lem10  12504  rpnnen2  12506  nthruc  12531  iddvds  12544  1dvds  12545  dvdsle  12576  dvds1  12579  3dvds  12593  divalglem5  12598  divalg  12604  bitsfzolem  12627  bitsfzo  12628  bitscmp  12631  bitsinv1lem  12634  gcdcllem1  12692  gcdcllem3  12694  gcdaddmlem  12709  gcdadd  12711  gcdid  12712  gcd1  12713  1gcd  12718  bezoutlem1  12719  gcdmultiple  12731  isprm3  12769  phicl2  12838  phi1  12843  dfphi2  12844  hashdvds  12845  phiprmpw  12846  eulerthlem2  12852  prmdiv  12855  prmdiveq  12856  odzcllem  12859  odzdvds  12862  odzphi  12863  oddprm  12870  pythagtriplem4  12874  iserodd  12890  pcpre1  12897  pc1  12910  pcrec  12913  pcid  12927  pcmptcl  12941  pcmpt  12942  fldivp1  12947  expnprm  12952  pockthlem  12954  unbenlem  12957  prmreclem2  12966  prmreclem4  12968  prmreclem6  12970  prmrec  12971  igz  12983  4sqlem12  13005  4sqlem13  13006  4sqlem19  13012  vdwapun  13023  vdwlem8  13037  vdwlem13  13042  prmlem0  13109  1259lem4  13134  2503lem2  13138  4001lem1  13141  mulg1  14576  mulgm1  14588  mulgp1  14595  mulgneg2  14596  mulgpropd  14602  cycsubgcl  14645  odinv  14876  sylow1lem1  14911  sylow3lem6  14945  efgs1b  15047  lt6abl  15183  pgpfac1lem2  15312  qsubdrg  16426  zsubrg  16427  gzsubrg  16428  zcyg  16447  mulgrhm  16462  mulgrhm2  16463  chrnzr  16486  znunit  16519  znrrg  16521  frgpcyg  16529  lmcnp  17034  lmmo  17110  1stcelcls  17189  1stccnp  17190  1stckgenlem  17250  1stckgen  17251  zfbas  17593  imasdsf1olem  17939  clmvneg1  18591  clmmulg  18593  lmnn  18691  cmetcaulem  18716  iscmet2  18722  causs  18726  caubl  18735  iscmet3i  18739  bcthlem5  18752  ovolsf  18834  ovolctb  18851  ovolunlem1a  18857  ovolunlem1  18858  ovoliunlem1  18863  ovoliun  18866  ovoliun2  18867  ovoliunnul  18868  ovolicc1  18877  ovolicc2lem2  18879  ovolicc2lem3  18880  ovolicc2lem4  18881  voliunlem1  18909  voliunlem2  18910  voliunlem3  18911  volsup  18915  ioombl1lem4  18920  uniioombllem2  18940  uniioombllem3  18942  uniioombllem6  18945  vitalilem4  18968  vitalilem5  18969  itg1climres  19071  mbfi1fseqlem6  19077  mbfi1flimlem  19079  mbfmullem2  19081  itg2monolem1  19107  itg2i1fseq  19112  itg2i1fseq2  19113  itg2addlem  19115  plyeq0lem  19594  dvply1  19666  vieta1lem2  19693  elqaalem2  19702  qaa  19705  iaa  19707  dvtaylp  19751  dvradcnv  19799  pserdvlem2  19806  pserdv2  19808  abelthlem6  19814  abelthlem9  19818  sin2pim  19855  cos2pim  19856  efif1olem2  19907  advlogexp  20004  logtayl  20009  logtaylsum  20010  logtayl2  20011  ang180lem3  20111  1cubrlem  20139  atantayl  20235  leibpilem2  20239  leibpi  20240  birthdaylem2  20249  dfef2  20267  divsqrsumlem  20276  emcllem4  20294  emcllem5  20295  emcllem6  20296  emcllem7  20297  wilthlem1  20308  wilthlem2  20309  wilthlem3  20310  basellem6  20325  basellem7  20326  basellem8  20327  basellem9  20328  muf  20380  ppip1le  20401  ppi1  20404  cht1  20405  chp1  20407  cht2  20412  ppieq0  20416  ppiub  20445  chpeq0  20449  chpchtsum  20460  chpub  20461  logfacbnd3  20464  logexprlim  20466  mersenne  20468  perfectlem1  20470  perfectlem2  20471  bposlem1  20525  bposlem2  20526  bposlem5  20529  bposlem6  20530  lgslem1  20537  lgslem2  20538  lgsfcl2  20543  lgsval2lem  20547  lgsdir2lem1  20564  lgsdir2lem3  20566  lgsdir2lem4  20567  lgsdir2lem5  20568  lgsqrlem1  20582  lgsdchr  20589  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem4  20593  lgsquad2lem1  20599  lgsquad3  20602  m1lgs  20603  2sqlem9  20614  2sqlem10  20615  2sqlem11  20616  2sqblem  20618  2sqb  20619  dchrisumlema  20639  dchrisumlem3  20642  dchrmusum2  20645  dchrvmasumiflem1  20652  dchrvmaeq0  20655  dchrisum0re  20664  dchrisum0lem1b  20666  dchrisum0lem2a  20668  logdivsum  20684  log2sumbnd  20695  pntrlog2bndlem1  20728  pntpbnd2  20738  qabvle  20776  ostth3  20789  ex-fl  20836  gx1  20931  gxm1  20937  nvlmle  21267  ipval2  21282  minvecolem3  21457  minvecolem4b  21459  minvecolem4  21461  h2hcau  21561  h2hlm  21562  hlimadd  21774  hlim0  21817  hhsscms  21858  occllem  21884  nlelchi  22643  opsqrlem2  22723  opsqrlem4  22725  hmopidmchi  22733  fzspl  23032  fzsplit3  23033  ballotlem2  23049  ballotlemfp1  23052  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemimin  23066  ballotlemic  23067  ballotlem1c  23068  ballotlemsdom  23072  ballotlemsel1i  23073  ballotlemsima  23076  ballotlemfrci  23088  ballotlemfrceq  23089  ballotlemfrcn0  23090  iuninc  23160  lmlim  23373  rge0scvg  23375  lmxrge0  23377  lmdvg  23378  gsumpropd2lem  23381  rnlogblem  23403  logblt  23410  esumpcvgval  23448  esumcvg  23456  dya2ub  23577  dstfrvclim1  23680  zetacvg  23691  subfac1  23711  subfacp1lem1  23712  subfacp1lem2a  23713  subfacp1lem5  23717  subfacp1lem6  23718  cvmliftlem10  23827  eupap1  23902  eupath2lem3  23905  sinccvg  24008  circum  24009  elfzp1b  24014  fznatpl1  24095  bcnm1  24098  axlowdimlem3  24574  axlowdimlem4  24575  axlowdimlem6  24577  axlowdimlem7  24578  axlowdimlem16  24587  axlowdimlem17  24588  axlowdim  24591  bpolydiflem  24791  cntrset  25613  1iskle  26000  clscnc  26021  phckle  26038  psckle  26039  intset  26055  fnckle  26056  fdc  26466  lmclim2  26485  geomcau  26486  heibor1lem  26544  heibor1  26545  bfplem1  26557  bfplem2  26558  rrncmslem  26567  rrncms  26568  mapfzcons  26804  mzpexpmpt  26834  fzsplit1nn0  26844  eldioph2lem1  26850  eldioph3b  26855  fz1eqin  26859  diophin  26863  diophun  26864  0dioph  26869  elnnrabdioph  26899  rabren3dioph  26909  irrapxlem1  26918  irrapxlem3  26920  pellexlem6  26930  rmspecnonsq  27003  rmxyadd  27017  rmxy1  27018  rmxy0  27019  rmxp1  27028  rmyp1  27029  rmxm1  27030  rmym1  27031  jm2.24nn  27057  acongeq  27081  jm2.22  27099  jm2.23  27100  jm2.25  27103  jm2.15nn0  27107  jm2.16nn0  27108  jm2.27c  27111  jm2.27dlem2  27114  rmydioph  27118  rmxdioph  27120  expdiophlem2  27126  expdioph  27127  mpaaeu  27366  sumsnd  27708  fmuldfeq  27724  fmul01lt1lem2  27726  fmul01lt1  27727  clim1fr1  27738  stoweidlem3  27763  stoweidlem7  27767  stoweidlem11  27771  stoweidlem14  27774  stoweidlem20  27780  stoweidlem26  27786  stoweidlem34  27794  stoweidlem51  27811  wallispilem4  27828  wallispilem5  27829  wallispi  27830  wallispi2lem1  27831  wallispi2lem2  27832  stirlinglem1  27834  stirlinglem5  27838  stirlinglem7  27840  stirlinglem8  27841  stirlinglem11  27844  stirlinglem12  27845  stirlinglem13  27846  stirlinglem14  27847  stirlinglem15  27848  stirlingr  27850  f1oun2prg  28087  s2f1o  28102  usgraex1elv  28140  usgraexmpldifpr  28143  usgraexmpl  28144
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-riota 6306  df-recs 6390  df-rdg 6425  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-nn 9749  df-z 10027
  Copyright terms: Public domain W3C validator