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

Theorem 1z 10069
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 9773 . 2  |-  1  e.  NN
21nnzi 10063 1  |-  1  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   1c1 8754   ZZcz 10040
This theorem is referenced by:  peano2z  10076  peano2zm  10078  peano5uzti  10117  nnuz  10279  eluz2b1  10305  uz2m1nn  10308  nninfm  10314  nnrecq  10355  qbtwnxr  10543  fz1n  10828  fz10  10830  fz01en  10834  fzprval  10860  fztpval  10861  fseq1p1m1  10873  elfzm1b  10876  fzm1  10878  fzoss2  10913  fzofzp1  10932  fzostep1  10938  flge1nn  10965  modnegd  11020  fzennn  11046  fzen2  11047  sermono  11094  seqf1olem2  11102  ser1const  11118  exp1  11125  zexpcl  11134  qexpcl  11135  qexpclz  11140  m1expcl  11142  expp1z  11166  expm1  11167  facnn  11306  fac0  11307  fac1  11308  bcn1  11341  bcp1nk  11345  bcpasc  11349  hashsng  11372  hashfz  11397  fz1isolem  11415  seqcoll  11417  climuni  12042  isercoll  12157  isercoll2  12158  iseraltlem1  12170  sum0  12210  sumsn  12229  fsumtscopo  12276  fsumparts  12280  binomlem  12303  climcndslem1  12324  climcndslem2  12325  climcnds  12326  divcnv  12328  supcvg  12330  arisum  12334  trireciplem  12336  trirecip  12337  expcnv  12338  geo2sum  12345  geo2lim  12347  geoisum1  12351  geoisum1c  12352  mertenslem1  12356  mertenslem2  12357  ege2le3  12387  sin01gt0  12486  rpnnen2lem10  12518  rpnnen2  12520  nthruc  12545  iddvds  12558  1dvds  12559  dvdsle  12590  dvds1  12593  3dvds  12607  divalglem5  12612  divalg  12618  bitsfzolem  12641  bitsfzo  12642  bitscmp  12645  bitsinv1lem  12648  gcdcllem1  12706  gcdcllem3  12708  gcdaddmlem  12723  gcdadd  12725  gcdid  12726  gcd1  12727  1gcd  12732  bezoutlem1  12733  gcdmultiple  12745  isprm3  12783  phicl2  12852  phi1  12857  dfphi2  12858  hashdvds  12859  phiprmpw  12860  eulerthlem2  12866  prmdiv  12869  prmdiveq  12870  odzcllem  12873  odzdvds  12876  odzphi  12877  oddprm  12884  pythagtriplem4  12888  iserodd  12904  pcpre1  12911  pc1  12924  pcrec  12927  pcid  12941  pcmptcl  12955  pcmpt  12956  fldivp1  12961  expnprm  12966  pockthlem  12968  unbenlem  12971  prmreclem2  12980  prmreclem4  12982  prmreclem6  12984  prmrec  12985  igz  12997  4sqlem12  13019  4sqlem13  13020  4sqlem19  13026  vdwapun  13037  vdwlem8  13051  vdwlem13  13056  prmlem0  13123  1259lem4  13148  2503lem2  13152  4001lem1  13155  mulg1  14590  mulgm1  14602  mulgp1  14609  mulgneg2  14610  mulgpropd  14616  cycsubgcl  14659  odinv  14890  sylow1lem1  14925  sylow3lem6  14959  efgs1b  15061  lt6abl  15197  pgpfac1lem2  15326  qsubdrg  16440  zsubrg  16441  gzsubrg  16442  zcyg  16461  mulgrhm  16476  mulgrhm2  16477  chrnzr  16500  znunit  16533  znrrg  16535  frgpcyg  16543  lmcnp  17048  lmmo  17124  1stcelcls  17203  1stccnp  17204  1stckgenlem  17264  1stckgen  17265  zfbas  17607  imasdsf1olem  17953  clmvneg1  18605  clmmulg  18607  lmnn  18705  cmetcaulem  18730  iscmet2  18736  causs  18740  caubl  18749  iscmet3i  18753  bcthlem5  18766  ovolsf  18848  ovolctb  18865  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliun  18880  ovoliun2  18881  ovoliunnul  18882  ovolicc1  18891  ovolicc2lem2  18893  ovolicc2lem3  18894  ovolicc2lem4  18895  voliunlem1  18923  voliunlem2  18924  voliunlem3  18925  volsup  18929  ioombl1lem4  18934  uniioombllem2  18954  uniioombllem3  18956  uniioombllem6  18959  vitalilem4  18982  vitalilem5  18983  itg1climres  19085  mbfi1fseqlem6  19091  mbfi1flimlem  19093  mbfmullem2  19095  itg2monolem1  19121  itg2i1fseq  19126  itg2i1fseq2  19127  itg2addlem  19129  plyeq0lem  19608  dvply1  19680  vieta1lem2  19707  elqaalem2  19716  qaa  19719  iaa  19721  dvtaylp  19765  dvradcnv  19813  pserdvlem2  19820  pserdv2  19822  abelthlem6  19828  abelthlem9  19832  sin2pim  19869  cos2pim  19870  efif1olem2  19921  advlogexp  20018  logtayl  20023  logtaylsum  20024  logtayl2  20025  ang180lem3  20125  1cubrlem  20153  atantayl  20249  leibpilem2  20253  leibpi  20254  birthdaylem2  20263  dfef2  20281  divsqrsumlem  20290  emcllem4  20308  emcllem5  20309  emcllem6  20310  emcllem7  20311  wilthlem1  20322  wilthlem2  20323  wilthlem3  20324  basellem6  20339  basellem7  20340  basellem8  20341  basellem9  20342  muf  20394  ppip1le  20415  ppi1  20418  cht1  20419  chp1  20421  cht2  20426  ppieq0  20430  ppiub  20459  chpeq0  20463  chpchtsum  20474  chpub  20475  logfacbnd3  20478  logexprlim  20480  mersenne  20482  perfectlem1  20484  perfectlem2  20485  bposlem1  20539  bposlem2  20540  bposlem5  20543  bposlem6  20544  lgslem1  20551  lgslem2  20552  lgsfcl2  20557  lgsval2lem  20561  lgsdir2lem1  20578  lgsdir2lem3  20580  lgsdir2lem4  20581  lgsdir2lem5  20582  lgsqrlem1  20596  lgsdchr  20603  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem4  20607  lgsquad2lem1  20613  lgsquad3  20616  m1lgs  20617  2sqlem9  20628  2sqlem10  20629  2sqlem11  20630  2sqblem  20632  2sqb  20633  dchrisumlema  20653  dchrisumlem3  20656  dchrmusum2  20659  dchrvmasumiflem1  20666  dchrvmaeq0  20669  dchrisum0re  20678  dchrisum0lem1b  20680  dchrisum0lem2a  20682  logdivsum  20698  log2sumbnd  20709  pntrlog2bndlem1  20742  pntpbnd2  20752  qabvle  20790  ostth3  20803  ex-fl  20850  gx1  20945  gxm1  20951  nvlmle  21281  ipval2  21296  minvecolem3  21471  minvecolem4b  21473  minvecolem4  21475  h2hcau  21575  h2hlm  21576  hlimadd  21788  hlim0  21831  hhsscms  21872  occllem  21898  nlelchi  22657  opsqrlem2  22737  opsqrlem4  22739  hmopidmchi  22747  fzspl  23046  fzsplit3  23047  ballotlem2  23063  ballotlemfp1  23066  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemimin  23080  ballotlemic  23081  ballotlem1c  23082  ballotlemsdom  23086  ballotlemsel1i  23087  ballotlemsima  23090  ballotlemfrci  23102  ballotlemfrceq  23103  ballotlemfrcn0  23104  iuninc  23174  lmlim  23386  rge0scvg  23388  lmxrge0  23390  lmdvg  23391  gsumpropd2lem  23394  rnlogblem  23416  logblt  23423  esumpcvgval  23461  esumcvg  23469  dya2ub  23590  dstfrvclim1  23693  zetacvg  23704  subfac1  23724  subfacp1lem1  23725  subfacp1lem2a  23726  subfacp1lem5  23730  subfacp1lem6  23731  cvmliftlem10  23840  eupap1  23915  eupath2lem3  23918  sinccvg  24021  circum  24022  elfzp1b  24027  fznatpl1  24108  bcnm1  24111  faclimlem3  24119  faclimlem5  24121  faclim  24126  cprod0  24168  axlowdimlem3  24644  axlowdimlem4  24645  axlowdimlem6  24647  axlowdimlem7  24648  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  bpolydiflem  24861  ovoliunnfl  25001  cntrset  25705  1iskle  26092  clscnc  26113  phckle  26130  psckle  26131  intset  26147  fnckle  26148  fdc  26558  lmclim2  26577  geomcau  26578  heibor1lem  26636  heibor1  26637  bfplem1  26649  bfplem2  26650  rrncmslem  26659  rrncms  26660  mapfzcons  26896  mzpexpmpt  26926  fzsplit1nn0  26936  eldioph2lem1  26942  eldioph3b  26947  fz1eqin  26951  diophin  26955  diophun  26956  0dioph  26961  elnnrabdioph  26991  rabren3dioph  27001  irrapxlem1  27010  irrapxlem3  27012  pellexlem6  27022  rmspecnonsq  27095  rmxyadd  27109  rmxy1  27110  rmxy0  27111  rmxp1  27120  rmyp1  27121  rmxm1  27122  rmym1  27123  jm2.24nn  27149  acongeq  27173  jm2.22  27191  jm2.23  27192  jm2.25  27195  jm2.15nn0  27199  jm2.16nn0  27200  jm2.27c  27203  jm2.27dlem2  27206  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  expdioph  27219  mpaaeu  27458  sumsnd  27800  fmuldfeq  27816  fmul01lt1lem2  27818  fmul01lt1  27819  clim1fr1  27830  stoweidlem3  27855  stoweidlem7  27859  stoweidlem11  27863  stoweidlem14  27866  stoweidlem20  27872  stoweidlem26  27878  stoweidlem34  27886  stoweidlem51  27903  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem1  27926  stirlinglem5  27930  stirlinglem7  27932  stirlinglem8  27933  stirlinglem11  27936  stirlinglem12  27937  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  stirlingr  27942  f1oun2prg  28187  elfznelfzo  28213  injresinj  28215  4fvwrd4  28220  s2f1o  28223  usgraex1elv  28263  usgraexmpldifpr  28266  usgraexmpl  28267  0pth  28356  redwlk  28364  fargshiftlem  28379  usgrcyclnl1  28386  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3lem4  28393  constr3trllem3  28398  constr3trllem5  28400  constr3pthlem1  28401  constr3pthlem2  28402  constr3pthlem3  28403  4cycl4v4e  28412  4cycl4dv4e  28414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830
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 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-riota 6320  df-recs 6404  df-rdg 6439  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-nn 9763  df-z 10041
  Copyright terms: Public domain W3C validator